; @origtpdbfilename ./TRS/secret07/aprove/aprove07.trs
; @xtcfilename "./TRS_Standard/Secret_07_TRS/aprove07.xml"
(format TRS)
(fun plus 2)
(fun plusIter 3)
(fun |0| 0)
(fun ifPlus 4)
(fun le 2)
(fun true 0)
(fun false 0)
(fun s 1)
(fun sum 1)
(fun sumIter 2)
(fun ifSum 4)
(fun isempty 1)
(fun head 1)
(fun tail 1)
(fun nil 0)
(fun cons 2)
(fun error 0)
(fun a 0)
(fun b 0)
(fun c 0)
(rule (plus x y) (plusIter x y |0|))
(rule (plusIter x y z) (ifPlus (le x z) x y z))
(rule (ifPlus true x y z) y)
(rule (ifPlus false x y z) (plusIter x (s y) (s z)))
(rule (le (s x) |0|) false)
(rule (le |0| y) true)
(rule (le (s x) (s y)) (le x y))
(rule (sum xs) (sumIter xs |0|))
(rule (sumIter xs x) (ifSum (isempty xs) xs x (plus x (head xs))))
(rule (ifSum true xs x y) x)
(rule (ifSum false xs x y) (sumIter (tail xs) y))
(rule (isempty nil) true)
(rule (isempty (cons x xs)) false)
(rule (head nil) error)
(rule (head (cons x xs)) x)
(rule (tail nil) nil)
(rule (tail (cons x xs)) xs)
(rule a b)
(rule a c)