; @origtpdbfilename velroyen-nonloop-ConvLower_c.trs
; @xtcfilename "./TRS_Standard/EEG_IJCAR_12/velroyen-nonloop-ConvLower_c.xml"
(format TRS)
(fun while 2)
(fun true 0)
(fun s 1)
(fun gt 2)
(fun |0| 0)
(fun f 1)
(fun if 2)
(fun neq 2)
(fun false 0)
(fun plus 2)
(rule (while true (s (s (s i)))) (while (gt (s (s (s i))) (s |0|)) (f (s (s (s i))))))
(rule (f i) (if (neq i (s (s |0|))) i))
(rule (gt (s x) (s y)) (gt x y))
(rule (gt (s x) |0|) true)
(rule (gt |0| |0|) false)
(rule (gt |0| (s y)) false)
(rule (if true i) (plus i (s |0|)))
(rule (if false i) i)
(rule (neq (s x) (s y)) (neq x y))
(rule (neq |0| |0|) false)
(rule (neq |0| (s y)) true)
(rule (neq (s x) |0|) true)
(rule (plus (s x) y) (plus x (s y)))
(rule (plus |0| y) y)