; @origtpdbfilename ./TRS/AProVE/IJCAR_18.trs
; @xtcfilename "./TRS_Standard/AProVE_04/IJCAR_18.xml"
(format TRS)
(fun plus 2)
(fun |0| 0)
(fun s 1)
(fun times 2)
(fun div 2)
(fun quot 3)
(fun eq 2)
(fun true 0)
(fun false 0)
(fun divides 2)
(fun prime 1)
(fun pr 2)
(fun if 3)
(rule (plus x |0|) x)
(rule (plus |0| y) y)
(rule (plus (s x) y) (s (plus x y)))
(rule (times |0| y) |0|)
(rule (times (s |0|) y) y)
(rule (times (s x) y) (plus y (times x y)))
(rule (div |0| y) |0|)
(rule (div x y) (quot x y y))
(rule (quot |0| (s y) z) |0|)
(rule (quot (s x) (s y) z) (quot x y z))
(rule (quot x |0| (s z)) (s (div x (s z))))
(rule (div (div x y) z) (div x (times y z)))
(rule (eq |0| |0|) true)
(rule (eq (s x) |0|) false)
(rule (eq |0| (s y)) false)
(rule (eq (s x) (s y)) (eq x y))
(rule (divides y x) (eq x (times (div x y) y)))
(rule (prime (s (s x))) (pr (s (s x)) (s x)))
(rule (pr x (s |0|)) true)
(rule (pr x (s (s y))) (if (divides (s (s y)) x) x (s y)))
(rule (if true x y) false)
(rule (if false x y) (pr x y))