; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann20.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann20.xml"
(format TRS)
(fun gt 2)
(fun |0| 0)
(fun false 0)
(fun s 1)
(fun true 0)
(fun plus 2)
(fun double 1)
(fun average 2)
(fun aver 2)
(fun if 3)
(rule (gt |0| y) false)
(rule (gt (s x) |0|) true)
(rule (gt (s x) (s y)) (gt x y))
(rule (plus |0| y) y)
(rule (plus (s x) y) (s (plus x y)))
(rule (double |0|) |0|)
(rule (double (s x)) (s (s (double x))))
(rule (average x y) (aver (plus x y) |0|))
(rule (aver sum z) (if (gt sum (double z)) sum z))
(rule (if true sum z) (aver sum (s z)))
(rule (if false sum z) z)