; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann06.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann06.xml"
(format TRS)
(fun p 1)
(fun s 1)
(fun |0| 0)
(fun le 2)
(fun true 0)
(fun false 0)
(fun average 2)
(fun if 6)
(fun if2 5)
(fun if3 4)
(fun if4 3)
(rule (p (s x)) x)
(rule (p |0|) |0|)
(rule (le |0| y) true)
(rule (le (s x) |0|) false)
(rule (le (s x) (s y)) (le x y))
(rule (average x y) (if (le x |0|) (le y |0|) (le y (s |0|)) (le y (s (s |0|))) x y))
(rule (if true b1 b2 b3 x y) (if2 b1 b2 b3 x y))
(rule (if false b1 b2 b3 x y) (average (p x) (s y)))
(rule (if2 true b2 b3 x y) |0|)
(rule (if2 false b2 b3 x y) (if3 b2 b3 x y))
(rule (if3 true b3 x y) |0|)
(rule (if3 false b3 x y) (if4 b3 x y))
(rule (if4 true x y) (s |0|))
(rule (if4 false x y) (average (s x) (p (p y))))