(VAR x y z) (RULES del(.(x,.(y,z))) -> f(=(x,y),x,y,z) f(true,x,y,z) -> del(.(y,z)) f(false,x,y,z) -> .(x,del(.(y,z))) =(nil,nil) -> true =(.(x,y),nil) -> false =(nil,.(y,z)) -> false =(.(x,y),.(u,v)) -> and(=(x,u),=(y,v)) ) (COMMENT Example 2.44 in \cite{SK90})