; @origtpdbfilename ./TRS/secret06/aprove/addList.trs
; @xtcfilename "./TRS_Standard/Secret_06_TRS/addList.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 append 2)
(fun p 1)
(fun inc 1)
(fun addLists 3)
(fun if 9)
(fun differentLengthError 0)
(fun addList 2)
(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 (append nil x) (cons x nil))
(rule (append (cons y ys) x) (cons y (append ys x)))
(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 (addLists xs ys zs) (if (isEmpty xs) (isEmpty ys) (isZero (head xs)) (tail xs) (tail ys) (cons (p (head xs)) (tail xs)) (cons (inc (head ys)) (tail ys)) zs (append zs (head ys))))
(rule (if true true b xs ys xs2 ys2 zs zs2) zs)
(rule (if true false b xs ys xs2 ys2 zs zs2) differentLengthError)
(rule (if false true b xs ys xs2 ys2 zs zs2) differentLengthError)
(rule (if false false false xs ys xs2 ys2 zs zs2) (addLists xs2 ys2 zs))
(rule (if false false true xs ys xs2 ys2 zs zs2) (addLists xs ys zs2))
(rule (addList xs ys) (addLists xs ys nil))