; @origtpdbfilename ./TRS/secret06/aprove/sumList.trs
; @xtcfilename "./TRS_Standard/Secret_06_TRS/sumList.xml"
(format TRS)
(fun isEmpty 1)
(fun cons 2)
(fun false 0)
(fun nil 0)
(fun true 0)
(fun isZero 1)
(fun |0| 0)
(fun s 1)
(fun head 1)
(fun tail 1)
(fun p 1)
(fun inc 1)
(fun sumList 2)
(fun if 6)
(fun sum 1)
(rule (isEmpty (cons x xs)) false)
(rule (isEmpty nil) true)
(rule (isZero |0|) true)
(rule (isZero (s x)) false)
(rule (head (cons x xs)) x)
(rule (tail (cons x xs)) xs)
(rule (tail nil) nil)
(rule (p (s (s x))) (s (p (s x))))
(rule (p (s |0|)) |0|)
(rule (p |0|) |0|)
(rule (inc (s x)) (s (inc x)))
(rule (inc |0|) (s |0|))
(rule (sumList xs y) (if (isEmpty xs) (isZero (head xs)) y (tail xs) (cons (p (head xs)) (tail xs)) (inc y)))
(rule (if true b y xs ys x) y)
(rule (if false true y xs ys x) (sumList xs y))
(rule (if false false y xs ys x) (sumList ys x))
(rule (sum xs) (sumList xs |0|))