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