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

The program

(from AG01 3.18)
(VAR x y z)
(RULES
minus(x,0) -> x
minus(s(x),s(y)) -> minus(x,y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0,y) -> y
plus(s(x),y) -> s(plus(x,y))
plus(s(x),y) -> plus(x,s(y))
plus(s(x),y) -> s(plus(minus(x,y),double(y)))
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend