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

The program

(VAR x y z)
(RULES
f(f(f(a,x),y),z) -> f(f(x,z),f(y,z))
f(f(b,x),y) -> x
f(c,y) -> y
)
(COMMENT Example 4.40 (Combinatory Logic) in \cite{SK90}) 
(COMMENT This TRS is not terminating!)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend