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

The program

(VAR x y z)
(RULES
*(*(x,y),z) -> *(x,*(y,z))
*(+(x,y),z) -> +(*(x,z),*(y,z))
*(x,+(y,f(z))) -> *(g(x,z),+(y,y))
)

(COMMENT Example 4.6 (Associativity and Distributivity) in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend