/home/nowonder/forschung/aprove/TPDB05/TRS/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)
)
(STRATEGY INNERMOST)
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend