/home/nowonder/forschung/aprove/TPDB05/TRS/D33/30.trs

The program

(VAR x y z u)
(RULES
:(:(:(:(C,x),y),z),u) -> :(:(x,z),:(:(:(x,y),z),u))
)
(COMMENT Example 30 in \cite{D33})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend