; @origtpdbfilename ./TRS/Cime/fact-hard.trs
; @xtcfilename "./TRS_Standard/CiME_04/fact-hard.xml"
(format TRS)
(fun + 2)
(fun |0| 0)
(fun s 1)
(fun * 2)
(fun ge 2)
(fun true 0)
(fun false 0)
(fun - 2)
(fun fact 1)
(fun iffact 2)
(rule (+ x |0|) x)
(rule (+ x (s y)) (s (+ x y)))
(rule (* x |0|) |0|)
(rule (* x (s y)) (+ (* x y) x))
(rule (ge x |0|) true)
(rule (ge |0| (s y)) false)
(rule (ge (s x) (s y)) (ge x y))
(rule (- x |0|) x)
(rule (- (s x) (s y)) (- x y))
(rule (fact x) (iffact x (ge x (s (s |0|)))))
(rule (iffact x true) (* x (fact (- x (s |0|)))))
(rule (iffact x false) (s |0|))