; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann29.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann29.xml"
(format TRS)
(fun le 2)
(fun s 1)
(fun |0| 0)
(fun false 0)
(fun true 0)
(fun plus 2)
(fun times 2)
(fun log 2)
(fun baseError 0)
(fun logZeroError 0)
(fun loop 4)
(fun if 5)
(rule (le (s x) |0|) false)
(rule (le |0| y) true)
(rule (le (s x) (s y)) (le x y))
(rule (plus |0| y) y)
(rule (plus (s x) y) (s (plus x y)))
(rule (times |0| y) |0|)
(rule (times (s x) y) (plus y (times x y)))
(rule (log x |0|) baseError)
(rule (log x (s |0|)) baseError)
(rule (log |0| (s (s b))) logZeroError)
(rule (log (s x) (s (s b))) (loop (s x) (s (s b)) (s |0|) |0|))
(rule (loop x (s (s b)) (s y) z) (if (le x (s y)) x (s (s b)) (s y) z))
(rule (if true x b y z) z)
(rule (if false x b y z) (loop x b (times b y) (s z)))