; @origtpdbfilename ./TRS/secret07/aprove/aprove04.trs
; @xtcfilename "./TRS_Standard/Secret_07_TRS/aprove04.xml"
(format TRS)
(fun lcm 2)
(fun lcmIter 4)
(fun |0| 0)
(fun times 2)
(fun if 5)
(fun or 2)
(fun ge 2)
(fun true 0)
(fun false 0)
(fun if2 5)
(fun divisible 2)
(fun plus 2)
(fun s 1)
(fun ifTimes 3)
(fun p 1)
(fun div 3)
(fun a 0)
(fun b 0)
(fun c 0)
(rule (lcm x y) (lcmIter x y |0| (times x y)))
(rule (lcmIter x y z u) (if (or (ge |0| x) (ge z u)) x y z u))
(rule (if true x y z u) z)
(rule (if false x y z u) (if2 (divisible z y) x y z u))
(rule (if2 true x y z u) z)
(rule (if2 false x y z u) (lcmIter x y (plus x z) u))
(rule (plus |0| y) y)
(rule (plus (s x) y) (s (plus x y)))
(rule (times x y) (ifTimes (ge |0| x) x y))
(rule (ifTimes true x y) |0|)
(rule (ifTimes false x y) (plus y (times y (p x))))
(rule (p (s x)) x)
(rule (p |0|) (s (s |0|)))
(rule (ge x |0|) true)
(rule (ge |0| (s y)) false)
(rule (ge (s x) (s y)) (ge x y))
(rule (or true y) true)
(rule (or false y) y)
(rule (divisible |0| (s y)) true)
(rule (divisible (s x) (s y)) (div (s x) (s y) (s y)))
(rule (div x y |0|) (divisible x y))
(rule (div |0| y (s z)) false)
(rule (div (s x) y (s z)) (div x y z))
(rule a b)
(rule a c)