/home/nowonder/forschung/aprove/TPDB05/TRS/AG01/#3.36.trs

The program

(from AG01 3.36)
(VAR x y)
(RULES
minus(x,0) -> x
minus(s(x),s(y)) -> minus(x,y)
f(0) -> s(0)
f(s(x)) -> minus(s(x),g(f(x)))
g(0) -> 0
g(s(x)) -> minus(s(x),f(g(x)))
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend