; @origtpdbfilename ./TRS/TRCSR/Ex1_GM03_iGM.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/Ex1_GM03_iGM.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)
(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 (mark (p X)) (active (p (mark X))))
(rule (mark |0|) (active |0|))
(rule (mark (s X)) (active (s (mark X))))
(rule (mark (leq X1 X2)) (active (leq (mark X1) (mark X2))))
(rule (mark true) (active true))
(rule (mark false) (active false))
(rule (mark (if X1 X2 X3)) (active (if (mark X1) X2 X3)))
(rule (mark (diff X1 X2)) (active (diff (mark X1) (mark X2))))
(rule (p (mark X)) (p X))
(rule (p (active X)) (p X))
(rule (s (mark X)) (s X))
(rule (s (active X)) (s X))
(rule (leq (mark X1) X2) (leq X1 X2))
(rule (leq X1 (mark X2)) (leq X1 X2))
(rule (leq (active X1) X2) (leq X1 X2))
(rule (leq X1 (active X2)) (leq X1 X2))
(rule (if (mark X1) X2 X3) (if X1 X2 X3))
(rule (if X1 (mark X2) X3) (if X1 X2 X3))
(rule (if X1 X2 (mark X3)) (if X1 X2 X3))
(rule (if (active X1) X2 X3) (if X1 X2 X3))
(rule (if X1 (active X2) X3) (if X1 X2 X3))
(rule (if X1 X2 (active X3)) (if X1 X2 X3))
(rule (diff (mark X1) X2) (diff X1 X2))
(rule (diff X1 (mark X2)) (diff X1 X2))
(rule (diff (active X1) X2) (diff X1 X2))
(rule (diff X1 (active X2)) (diff X1 X2))