/home/nowonder/forschung/aprove/TPDB05/TRS/HM/t013.trs

The program

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

(COMMENT
Example 8 in \cite{G96}.
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend