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

The program

(VAR x y z u)
(RULES
+(x,+(y,z)) -> +(+(x,y),z)
+(*(x,y),+(x,z)) -> *(x,+(y,z))
+(*(x,y),+(*(x,z),u)) -> +(*(x,+(y,z)),u)
)
(COMMENT Example 2.6 in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend