/home/nowonder/forschung/aprove/TPDB05/TRS/various/23.trs

The program

(VAR x y z)
(RULES
g(0,f(x,x)) -> x
g(x,s(y)) -> g(f(x,y),0)
g(s(x),y) -> g(f(x,y),0)
g(f(x,y),0) -> f(g(x,0),g(y,0))
)
(COMMENT Example 4.2.30 in \cite{K00})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend