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

The program

(VAR x y z)
(RULES
++(nil,y) -> y
++(x,nil) -> x
++(.(x,y),z) -> .(x,++(y,z))
++(++(x,y),z) -> ++(x,++(y,z))
)

(COMMENT Example 2.38 (Functional List Append) in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend