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

The program

(VAR x y z)
(RULES
flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x,y)) -> ++(flatten(x),flatten(y))
flatten(++(unit(x),y)) -> ++(flatten(x),flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x,y)) -> ++(rev(y),rev(x))
rev(rev(x)) -> x
++(x,nil) -> x
++(nil,y) -> y
++(++(x,y),z) -> ++(x,++(y,z))
)
(COMMENT Example 2.42 (Flattening and Reverse Operation) in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend