; @origtpdbfilename ./TRS/secret07/aprove/aprove01.trs
; @xtcfilename "./TRS_Standard/Secret_07_TRS/aprove01.xml"
(format TRS)
(fun times 2)
(fun sum 1)
(fun generate 2)
(fun gen 3)
(fun |0| 0)
(fun if 4)
(fun ge 2)
(fun true 0)
(fun nil 0)
(fun false 0)
(fun cons 2)
(fun s 1)
(fun sum2 2)
(fun ifsum 4)
(fun isNil 1)
(fun isZero 1)
(fun head 1)
(fun ifsum2 3)
(fun tail 1)
(fun p 1)
(fun error 0)
(fun a 0)
(fun c 0)
(fun d 0)
(rule (times x y) (sum (generate x y)))
(rule (generate x y) (gen x y |0|))
(rule (gen x y z) (if (ge z x) x y z))
(rule (if true x y z) nil)
(rule (if false x y z) (cons y (gen x y (s z))))
(rule (sum xs) (sum2 xs |0|))
(rule (sum2 xs y) (ifsum (isNil xs) (isZero (head xs)) xs y))
(rule (ifsum true b xs y) y)
(rule (ifsum false b xs y) (ifsum2 b xs y))
(rule (ifsum2 true xs y) (sum2 (tail xs) y))
(rule (ifsum2 false xs y) (sum2 (cons (p (head xs)) (tail xs)) (s y)))
(rule (isNil nil) true)
(rule (isNil (cons x xs)) false)
(rule (tail nil) nil)
(rule (tail (cons x xs)) xs)
(rule (head (cons x xs)) x)
(rule (head nil) error)
(rule (isZero |0|) true)
(rule (isZero (s |0|)) false)
(rule (isZero (s (s x))) (isZero (s x)))
(rule (p |0|) (s (s |0|)))
(rule (p (s |0|)) |0|)
(rule (p (s (s x))) (s (p (s x))))
(rule (ge x |0|) true)
(rule (ge |0| (s y)) false)
(rule (ge (s x) (s y)) (ge x y))
(rule a c)
(rule a d)