; @origtpdbfilename ./TRS/Thiemann/mapHard.trs
; @xtcfilename "./TRS_Standard/AProVE_06/mapHard.xml"
(format TRS)
(fun ap 2)
(fun map 0)
(fun if 0)
(fun isEmpty 0)
(fun true 0)
(fun nil 0)
(fun false 0)
(fun cons 0)
(fun last 0)
(fun dropLast 0)
(rule (ap (ap map f) xs) (ap (ap (ap if (ap isEmpty xs)) f) xs))
(rule (ap (ap (ap if true) f) xs) nil)
(rule (ap (ap (ap if false) f) xs) (ap (ap cons (ap f (ap last xs))) (ap (ap map f) (ap dropLast xs))))
(rule (ap isEmpty nil) true)
(rule (ap isEmpty (ap (ap cons x) xs)) false)
(rule (ap last (ap (ap cons x) nil)) x)
(rule (ap last (ap (ap cons x) (ap (ap cons y) ys))) (ap last (ap (ap cons y) ys)))
(rule (ap dropLast nil) nil)
(rule (ap dropLast (ap (ap cons x) nil)) nil)
(rule (ap dropLast (ap (ap cons x) (ap (ap cons y) ys))) (ap (ap cons x) (ap dropLast (ap (ap cons y) ys))))