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

The program

(VAR x y z)
(RULES
*(x,*(y,z)) -> *(otimes(x,y),z)
*(1,y) -> y
*(+(x,y),z) -> oplus(*(x,z),*(y,z))
*(x,oplus(y,z)) -> oplus(*(x,y),*(x,z))
)
(COMMENT Example 4.10 (A-Modules) in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend