/home/nowonder/forschung/aprove/TPDB05/TRS/Rubio/test4.trs

The program

(VAR X)
(RULES

f(a,a) -> f(a,b)
f(a,b) -> f(s(a),c)
f(s(X),c) -> f(X,c)
f(c,c) -> f(a,a)

)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend