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

The program

(VAR x y z)
(RULES
*(x,+(y,z)) -> +(*(x,y),*(x,z))
)
(COMMENT Example 18 in \cite{D33})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend