; @origtpdbfilename ./TRS/SchneiderKamp/trs/otto12.trs
; @xtcfilename "./TRS_Standard/AProVE_07/otto12.xml"
(format TRS)
(fun plus 2)
(fun |0| 0)
(fun s 1)
(fun times 2)
(fun exp 2)
(fun ge 2)
(fun true 0)
(fun false 0)
(fun tower 2)
(fun towerIter 4)
(fun help 5)
(rule (plus |0| x) x)
(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 (exp x |0|) (s |0|))
(rule (exp x (s y)) (times x (exp x y)))
(rule (ge x |0|) true)
(rule (ge |0| (s x)) false)
(rule (ge (s x) (s y)) (ge x y))
(rule (tower x y) (towerIter |0| x y (s |0|)))
(rule (towerIter c x y z) (help (ge c x) c x y z))
(rule (help true c x y z) z)
(rule (help false c x y z) (towerIter (s c) x y (exp y z)))