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

The program

(VAR x y z)
(RULES
f(0,1,x) -> f(g(x),g(x),x)
f(g(x),y,z) -> g(f(x,y,z))
f(x,g(y),z) -> g(f(x,y,z))
f(x,y,g(z)) -> g(f(x,y,z))
)


Submit to AProVE Web Frontend

Edit in AProVE Web Frontend