/home/nowonder/forschung/aprove/TPDB05/TRS/HofWald/2.trs

The program

(Comment with f(a,z) = A(z), f(f(a,a),z) = B(z),
         this is AB(z) -> BAA(z)
         this is not RFC-match-bounded (but its reverse is)
)
(VAR x)
(RULES f (a, f (f (a, a), x)) -> f (f (a, a), f (a, f (a, x))))

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend