; @origtpdbfilename ./TRS/secret07/aprove/aprove09.trs
; @xtcfilename "./TRS_Standard/Secret_07_TRS/aprove09.xml"
(format TRS)
(fun div 2)
(fun div2 3)
(fun |0| 0)
(fun if1 6)
(fun le 2)
(fun plus 2)
(fun inc 1)
(fun true 0)
(fun divZeroError 0)
(fun false 0)
(fun if2 5)
(fun minus 2)
(fun s 1)
(fun plusIter 3)
(fun ifPlus 4)
(fun a 0)
(fun c 0)
(fun d 0)
(rule (div x y) (div2 x y |0|))
(rule (div2 x y i) (if1 (le y |0|) (le y x) x y (plus i |0|) (inc i)))
(rule (if1 true b x y i j) divZeroError)
(rule (if1 false b x y i j) (if2 b x y i j))
(rule (if2 true x y i j) (div2 (minus x y) y j))
(rule (if2 false x y i j) i)
(rule (inc |0|) |0|)
(rule (inc (s i)) (s (inc i)))
(rule (le (s x) |0|) false)
(rule (le |0| y) true)
(rule (le (s x) (s y)) (le x y))
(rule (minus x |0|) x)
(rule (minus |0| y) |0|)
(rule (minus (s x) (s y)) (minus x y))
(rule (plus x y) (plusIter x y |0|))
(rule (plusIter x y z) (ifPlus (le x z) x y z))
(rule (ifPlus true x y z) y)
(rule (ifPlus false x y z) (plusIter x (s y) (s z)))
(rule a c)
(rule a d)