; @origtpdbfilename ./TRS/secret07/aprove/aprove02.trs
; @xtcfilename "./TRS_Standard/Secret_07_TRS/aprove02.xml"
(format TRS)
(fun plus 2)
(fun ifPlus 3)
(fun isZero 1)
(fun inc 1)
(fun true 0)
(fun p 1)
(fun false 0)
(fun times 2)
(fun timesIter 4)
(fun |0| 0)
(fun ifTimes 5)
(fun ge 2)
(fun s 1)
(fun f0 3)
(fun f1 3)
(fun f2 3)
(fun |1| 0)
(fun d 0)
(fun c 0)
(rule (plus x y) (ifPlus (isZero x) x (inc y)))
(rule (ifPlus true x y) (p y))
(rule (ifPlus false x y) (plus (p x) y))
(rule (times x y) (timesIter |0| x y |0|))
(rule (timesIter i x y z) (ifTimes (ge i x) i x y z))
(rule (ifTimes true i x y z) z)
(rule (ifTimes false i x y z) (timesIter (inc i) x y (plus z y)))
(rule (isZero |0|) true)
(rule (isZero (s |0|)) false)
(rule (isZero (s (s x))) (isZero (s x)))
(rule (inc |0|) (s |0|))
(rule (inc (s x)) (s (inc x)))
(rule (inc x) (s x))
(rule (p |0|) |0|)
(rule (p (s x)) x)
(rule (p (s (s x))) (s (p (s x))))
(rule (ge x |0|) true)
(rule (ge |0| (s y)) false)
(rule (ge (s x) (s y)) (ge x y))
(rule (f0 |0| y x) (f1 x y x))
(rule (f1 x y z) (f2 x y z))
(rule (f2 x |1| z) (f0 x z z))
(rule (f0 x y z) d)
(rule (f1 x y z) c)