; @origtpdbfilename ./TRS/TRCSR/Ex49_GM04_C.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/Ex49_GM04_C.xml"
(format TRS)
(fun active 1)
(fun minus 2)
(fun |0| 0)
(fun mark 1)
(fun s 1)
(fun geq 2)
(fun true 0)
(fun false 0)
(fun div 2)
(fun if 3)
(fun proper 1)
(fun ok 1)
(fun top 1)
(rule (active (minus |0| Y)) (mark |0|))
(rule (active (minus (s X) (s Y))) (mark (minus X Y)))
(rule (active (geq X |0|)) (mark true))
(rule (active (geq |0| (s Y))) (mark false))
(rule (active (geq (s X) (s Y))) (mark (geq X Y)))
(rule (active (div |0| (s Y))) (mark |0|))
(rule (active (div (s X) (s Y))) (mark (if (geq X Y) (s (div (minus X Y) (s Y))) |0|)))
(rule (active (if true X Y)) (mark X))
(rule (active (if false X Y)) (mark Y))
(rule (active (s X)) (s (active X)))
(rule (active (div X1 X2)) (div (active X1) X2))
(rule (active (if X1 X2 X3)) (if (active X1) X2 X3))
(rule (s (mark X)) (mark (s X)))
(rule (div (mark X1) X2) (mark (div X1 X2)))
(rule (if (mark X1) X2 X3) (mark (if X1 X2 X3)))
(rule (proper (minus X1 X2)) (minus (proper X1) (proper X2)))
(rule (proper |0|) (ok |0|))
(rule (proper (s X)) (s (proper X)))
(rule (proper (geq X1 X2)) (geq (proper X1) (proper X2)))
(rule (proper true) (ok true))
(rule (proper false) (ok false))
(rule (proper (div X1 X2)) (div (proper X1) (proper X2)))
(rule (proper (if X1 X2 X3)) (if (proper X1) (proper X2) (proper X3)))
(rule (minus (ok X1) (ok X2)) (ok (minus X1 X2)))
(rule (s (ok X)) (ok (s X)))
(rule (geq (ok X1) (ok X2)) (ok (geq X1 X2)))
(rule (div (ok X1) (ok X2)) (ok (div X1 X2)))
(rule (if (ok X1) (ok X2) (ok X3)) (ok (if X1 X2 X3)))
(rule (top (mark X)) (top (proper X)))
(rule (top (ok X)) (top (active X)))