; @origtpdbfilename ./TRS/SK90/2.29.trs
; @xtcfilename "./TRS_Standard/SK90/2.29.xml"
(format TRS)
(fun prime 1)
(fun |0| 0)
(fun false 0)
(fun s 1)
(fun prime1 2)
(fun true 0)
(fun and 2)
(fun not 1)
(fun divp 2)
(fun = 2)
(fun rem 2)
(rule (prime |0|) false)
(rule (prime (s |0|)) false)
(rule (prime (s (s x))) (prime1 (s (s x)) (s x)))
(rule (prime1 x |0|) false)
(rule (prime1 x (s |0|)) true)
(rule (prime1 x (s (s y))) (and (not (divp (s (s y)) x)) (prime1 x (s y))))
(rule (divp x y) (= (rem x y) |0|))