; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann41.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann41.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)
(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 nil) |0|)
(rule (sum (cons |0| xs)) (sum xs))
(rule (sum (cons (s x) xs)) (s (sum (cons x xs))))
(rule (ge x |0|) true)
(rule (ge |0| (s y)) false)
(rule (ge (s x) (s y)) (ge x y))