; @origtpdbfilename ./TRS/secret07/aprove/aprove05.trs
; @xtcfilename "./TRS_Standard/Secret_07_TRS/aprove05.xml"
(format TRS)
(fun prod 1)
(fun prodIter 2)
(fun s 1)
(fun |0| 0)
(fun ifProd 3)
(fun isempty 1)
(fun true 0)
(fun false 0)
(fun tail 1)
(fun times 2)
(fun head 1)
(fun plus 2)
(fun timesIter 4)
(fun ifTimes 5)
(fun ge 2)
(fun nil 0)
(fun cons 2)
(fun error 0)
(fun a 0)
(fun b 0)
(fun c 0)
(rule (prod xs) (prodIter xs (s |0|)))
(rule (prodIter xs x) (ifProd (isempty xs) xs x))
(rule (ifProd true xs x) x)
(rule (ifProd false xs x) (prodIter (tail xs) (times x (head xs))))
(rule (plus |0| y) y)
(rule (plus (s x) y) (s (plus x y)))
(rule (times x y) (timesIter x y |0| |0|))
(rule (timesIter x y z u) (ifTimes (ge u x) x y z u))
(rule (ifTimes true x y z u) z)
(rule (ifTimes false x y z u) (timesIter x y (plus y z) (s u)))
(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 (ge x |0|) true)
(rule (ge |0| (s y)) false)
(rule (ge (s x) (s y)) (ge x y))
(rule a b)
(rule a c)