/home/nowonder/forschung/aprove/TPDB05/TRS/TRCSR/Ex4_7_15_Bor03_GM.trs

The program

(VAR X1 X2 X)
(RULES 
a__f(0) -> cons(0,f(s(0)))
a__f(s(0)) -> a__f(a__p(s(0)))
a__p(s(0)) -> 0
mark(f(X)) -> a__f(mark(X))
mark(p(X)) -> a__p(mark(X))
mark(0) -> 0
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(s(X)) -> s(mark(X))
a__f(X) -> f(X)
a__p(X) -> p(X)
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend