/home/nowonder/forschung/aprove/TPDB05/TRS/SK90/4.49.trs

The program

(VAR x y z u v)
(RULES
f(x,y,f(z,u,v)) -> f(f(x,y,z),u,f(x,y,v))
)
(COMMENT Example 4.49 in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend