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

The program

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

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend