/home/nowonder/forschung/aprove/TPDB05/TRS/secret2005/tpa3.trs

The program

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

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend