; @origtpdbfilename ./TRS/secret06/aprove/reverse.trs
; @xtcfilename "./TRS_Standard/Secret_06_TRS/reverse.xml"
(format TRS)
(fun isEmpty 1)
(fun nil 0)
(fun true 0)
(fun cons 2)
(fun false 0)
(fun last 1)
(fun dropLast 1)
(fun append 2)
(fun reverse 1)
(fun rev 2)
(fun if 4)
(rule (isEmpty nil) true)
(rule (isEmpty (cons x xs)) false)
(rule (last (cons x nil)) x)
(rule (last (cons x (cons y ys))) (last (cons y ys)))
(rule (dropLast nil) nil)
(rule (dropLast (cons x nil)) nil)
(rule (dropLast (cons x (cons y ys))) (cons x (dropLast (cons y ys))))
(rule (append nil ys) ys)
(rule (append (cons x xs) ys) (cons x (append xs ys)))
(rule (reverse xs) (rev xs nil))
(rule (rev xs ys) (if (isEmpty xs) (dropLast xs) (append ys (last xs)) ys))
(rule (if true xs ys zs) zs)
(rule (if false xs ys zs) (rev xs ys))