; @origtpdbfilename rybalchenko-nonloop-popl08.trs
; @xtcfilename "./TRS_Standard/EEG_IJCAR_12/rybalchenko-nonloop-popl08.xml"
(format TRS)
(fun notZero 1)
(fun pos 1)
(fun s 1)
(fun true 0)
(fun neg 1)
(fun |0| 0)
(fun false 0)
(fun greaterZero 1)
(fun and 2)
(fun minusT 2)
(fun plusNat 2)
(fun negate 1)
(fun minus 2)
(fun while 3)
(rule (notZero (pos (s x))) true)
(rule (notZero (neg (s x))) true)
(rule (notZero (neg |0|)) false)
(rule (notZero (pos |0|)) false)
(rule (greaterZero (pos (s x))) true)
(rule (greaterZero (pos |0|)) false)
(rule (greaterZero (neg x)) false)
(rule (and false false) false)
(rule (and false true) false)
(rule (and true false) false)
(rule (and true true) true)
(rule (minusT |0| y) (neg y))
(rule (minusT x |0|) (pos x))
(rule (minusT (s x) (s y)) (minusT x y))
(rule (plusNat |0| y) y)
(rule (plusNat (s x) y) (plusNat x (s y)))
(rule (negate (pos x)) (neg x))
(rule (negate (neg x)) (pos x))
(rule (minus (pos x) (pos y)) (minusT x y))
(rule (minus (neg x) (neg y)) (negate (minusT x y)))
(rule (minus (pos x) (neg y)) (pos (plusNat x y)))
(rule (minus (neg x) (pos y)) (neg (plusNat x y)))
(rule (while true i y) (while (and (notZero y) (greaterZero i)) (minus i y) y))