/home/nowonder/forschung/aprove/TPDB05/TRS/uncurried/AG01/#4.8.trs

The program

(from AG01 4.8)
(VAR x y)
(RULES
plus(x,0) -> x
plus(x,s(y)) -> s(plus(x,y))
f(0,s(0),x) -> f(x,plus(x,x),x)
g(x,y) -> x
g(x,y) -> y
)
(STRATEGY INNERMOST)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend