; @origtpdbfilename ./TRS/secret07/aprove/aprove06.trs
; @xtcfilename "./TRS_Standard/Secret_07_TRS/aprove06.xml"
(format TRS)
(fun le 2)
(fun s 1)
(fun |0| 0)
(fun false 0)
(fun true 0)
(fun double 1)
(fun log 1)
(fun logError 0)
(fun loop 3)
(fun if 4)
(fun maplog 1)
(fun mapIter 2)
(fun nil 0)
(fun ifmap 3)
(fun isempty 1)
(fun droplast 1)
(fun cons 2)
(fun last 1)
(fun error 0)
(fun a 0)
(fun b 0)
(fun c 0)
(rule (le (s x) |0|) false)
(rule (le |0| y) true)
(rule (le (s x) (s y)) (le x y))
(rule (double |0|) |0|)
(rule (double (s x)) (s (s (double x))))
(rule (log |0|) logError)
(rule (log (s x)) (loop (s x) (s |0|) |0|))
(rule (loop x (s y) z) (if (le x (s y)) x (s y) z))
(rule (if true x y z) z)
(rule (if false x y z) (loop x (double y) (s z)))
(rule (maplog xs) (mapIter xs nil))
(rule (mapIter xs ys) (ifmap (isempty xs) xs ys))
(rule (ifmap true xs ys) ys)
(rule (ifmap false xs ys) (mapIter (droplast xs) (cons (log (last xs)) ys)))
(rule (isempty nil) true)
(rule (isempty (cons x xs)) false)
(rule (last nil) error)
(rule (last (cons x nil)) x)
(rule (last (cons x (cons y xs))) (last (cons y xs)))
(rule (droplast nil) nil)
(rule (droplast (cons x nil)) nil)
(rule (droplast (cons x (cons y xs))) (cons x (droplast (cons y xs))))
(rule a b)
(rule a c)