; @origtpdbfilename ./TRS/secret05/aprove1.trs
; @xtcfilename "./TRS_Standard/Secret_05_TRS/aprove1.xml"
(format TRS)
(fun ap 2)
(fun map 0)
(fun if 0)
(fun isEmpty 0)
(fun true 0)
(fun null 0)
(fun cons 0)
(fun last 0)
(fun if2 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) null)
(rule (ap (ap (ap if null) f) xs) (ap (ap cons (ap f (ap last xs))) (ap (ap if2 f) xs)))
(rule (ap (ap if2 f) xs) (ap (ap map f) (ap dropLast xs)))
(rule (ap isEmpty null) true)
(rule (ap isEmpty (ap (ap cons x) xs)) null)
(rule (ap last (ap (ap cons x) null)) x)
(rule (ap last (ap (ap cons x) (ap (ap cons y) ys))) (ap last (ap (ap cons y) ys)))
(rule (ap dropLast (ap (ap cons x) null)) null)
(rule (ap dropLast (ap (ap cons x) (ap (ap cons y) ys))) (ap (ap cons x) (ap dropLast (ap (ap cons y) ys))))