; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann08.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann08.xml"
(format TRS)
(fun empty 1)
(fun nil 0)
(fun true 0)
(fun cons 2)
(fun false 0)
(fun head 1)
(fun tail 1)
(fun rev 1)
(fun rev1 2)
(fun rev2 2)
(fun last 2)
(fun if 3)
(rule (empty nil) true)
(rule (empty (cons x l)) false)
(rule (head (cons x l)) x)
(rule (tail nil) nil)
(rule (tail (cons x l)) l)
(rule (rev nil) nil)
(rule (rev (cons x l)) (cons (rev1 x l) (rev2 x l)))
(rule (last x l) (if (empty l) x l))
(rule (if true x l) x)
(rule (if false x l) (last (head l) (tail l)))
(rule (rev2 x nil) nil)
(rule (rev2 x (cons y l)) (rev (cons x (rev2 y l))))