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

The program

(VAR X Y Z)
(RULES

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

)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend