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

The program

(VAR x y z)
(RULES
rev(nil) -> nil
rev(.(x,y)) -> ++(rev(y),.(x,nil))
car(.(x,y)) -> x
cdr(.(x,y)) -> y
null(nil) -> true
null(.(x,y)) -> false
++(nil,y) -> y
++(.(x,y),z) -> .(x,++(y,z))
)

(COMMENT Example 2.39 (List) in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend