/home/nowonder/forschung/aprove/TPDB05/TRS/nontermin/Rubio-inn/test830.trs

The program

(VAR X Y)
(RULES

f(s(X))  -> f(X)
g(cons(0,Y))  -> g(Y)
g(cons(s(X),Y))  -> s(X)
h(cons(X,Y))  -> h(g(cons(X,Y)))
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend