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

The program

(VAR x y z u v)
(RULES
f(f(x,y,z),u,f(x,y,v)) -> f(x,y,f(z,u,v))
f(x,y,y) -> y
f(x,y,g(y)) -> x
f(x,x,y) -> x
f(g(x),x,y) -> y
)
(COMMENT Example 4.48 (Ternary Boolean Algebra) in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend