/home/nowonder/forschung/aprove/TPDB05/TRS/nontermin/cariboo/tricky1.trs

The program

(from
O. Fissore. Terminaison de la reecriture sous strategies.
PhD Thesis, Universite Henri Poincare - Nancy I, 2003.
)

(VAR x y)

(RULES
f(g(x),g(y)) -> f(p(f(g(x),s(y))), g(s(p(x))))
p(0) -> g(0)
g(s(p(x))) -> p(x)
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend