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

The program

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

(COMMENT Example 4.38 (Associative Ring) in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend