; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann36.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann36.xml"
(format TRS)
(fun le 2)
(fun |0| 0)
(fun true 0)
(fun s 1)
(fun false 0)
(fun quot 2)
(fun quotZeroErro 0)
(fun quotIter 5)
(fun if 6)
(fun if2 6)
(rule (le |0| y) true)
(rule (le (s x) |0|) false)
(rule (le (s x) (s y)) (le x y))
(rule (quot x |0|) quotZeroErro)
(rule (quot x (s y)) (quotIter x (s y) |0| |0| |0|))
(rule (quotIter x (s y) z u v) (if (le x z) x (s y) z u v))
(rule (if true x y z u v) v)
(rule (if false x y z u v) (if2 (le y (s u)) x y (s z) (s u) v))
(rule (if2 false x y z u v) (quotIter x y z u v))
(rule (if2 true x y z u v) (quotIter x y z |0| (s v)))