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

The program

(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})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend