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

The program

(VAR x y z)
(RULES
f(nil) -> nil
f(.(nil,y)) -> .(nil,f(y))
f(.(.(x,y),z)) -> f(.(x,.(y,z)))
g(nil) -> nil
g(.(x,nil)) -> .(g(x),nil)
g(.(x,.(y,z))) -> g(.(.(x,y),z))
)
(COMMENT Example 4.30 (Binary Trees) in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend