/home/nowonder/forschung/aprove/TPDB05/TRS/Zantema/z25.trs

The program

(VAR x )
(RULES
f(a,f(b,x)) -> f(b,f(a,x)) 
f(b,f(c,x)) -> f(c,f(b,x)) 
f(c,f(a,x)) -> f(a,f(c,x)) 
)
(COMMENT: curried version of simply terminating SRS ab -> ba, bc -> cb, ca -> ac )

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend