; @origtpdbfilename ./TRS/SchneiderKamp/trs/wiehe11.trs
; @xtcfilename "./TRS_Standard/AProVE_07/wiehe11.xml"
(format TRS)
(fun minus 2)
(fun |0| 0)
(fun s 1)
(fun quot 2)
(fun plus 2)
(fun app 2)
(fun nil 0)
(fun cons 2)
(fun sum 1)
(fun if 3)
(fun gt 2)
(fun not 1)
(fun id 1)
(fun zero 0)
(fun true 0)
(fun false 0)
(rule (minus x |0|) x)
(rule (minus (s x) (s y)) (minus x y))
(rule (quot |0| (s y)) |0|)
(rule (quot (s x) (s y)) (s (quot (minus x y) (s y))))
(rule (plus |0| y) y)
(rule (plus (s x) y) (s (plus x y)))
(rule (minus (minus x y) z) (minus x (plus y z)))
(rule (app nil k) k)
(rule (app l nil) l)
(rule (app (cons x l) k) (cons x (app l k)))
(rule (sum (cons x nil)) (cons x nil))
(rule (sum (cons x (cons y l))) (sum (cons (plus x y) l)))
(rule (sum (app l (cons x (cons y k)))) (sum (app l (sum (cons x (cons y k))))))
(rule (plus (s x) (s y)) (s (s (plus (if (gt x y) x y) (if (not (gt x y)) (id x) (id y))))))
(rule (plus (s x) x) (plus (if (gt x x) (id x) (id x)) (s x)))
(rule (plus zero y) y)
(rule (plus (id x) (s y)) (s (plus x (if (gt (s y) y) y (s y)))))
(rule (id x) x)
(rule (if true x y) x)
(rule (if false x y) y)
(rule (not x) (if x false true))
(rule (gt (s x) zero) true)
(rule (gt zero y) false)
(rule (gt (s x) (s y)) (gt x y))