; @origtpdbfilename ./TRS/TRCSR/Ex1_GM03_GM.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/Ex1_GM03_GM.xml"
(format TRS)
(fun a__p 1)
(fun |0| 0)
(fun s 1)
(fun mark 1)
(fun a__leq 2)
(fun true 0)
(fun false 0)
(fun a__if 3)
(fun a__diff 2)
(fun diff 2)
(fun p 1)
(fun leq 2)
(fun if 3)
(rule (a__p |0|) |0|)
(rule (a__p (s X)) (mark X))
(rule (a__leq |0| Y) true)
(rule (a__leq (s X) |0|) false)
(rule (a__leq (s X) (s Y)) (a__leq (mark X) (mark Y)))
(rule (a__if true X Y) (mark X))
(rule (a__if false X Y) (mark Y))
(rule (a__diff X Y) (a__if (a__leq (mark X) (mark Y)) |0| (s (diff (p X) Y))))
(rule (mark (p X)) (a__p (mark X)))
(rule (mark (leq X1 X2)) (a__leq (mark X1) (mark X2)))
(rule (mark (if X1 X2 X3)) (a__if (mark X1) X2 X3))
(rule (mark (diff X1 X2)) (a__diff (mark X1) (mark X2)))
(rule (mark |0|) |0|)
(rule (mark (s X)) (s (mark X)))
(rule (mark true) true)
(rule (mark false) false)
(rule (a__p X) (p X))
(rule (a__leq X1 X2) (leq X1 X2))
(rule (a__if X1 X2 X3) (if X1 X2 X3))
(rule (a__diff X1 X2) (diff X1 X2))