; @origtpdbfilename ./TRS/TRCSR/MYNAT_complete_iGM.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/MYNAT_complete_iGM.xml"
(format TRS)
(fun active 1)
(fun U11 3)
(fun tt 0)
(fun mark 1)
(fun U12 2)
(fun isNat 1)
(fun U13 1)
(fun U21 2)
(fun U22 1)
(fun U31 3)
(fun U32 2)
(fun U33 1)
(fun U41 2)
(fun U51 3)
(fun s 1)
(fun plus 2)
(fun U61 1)
(fun |0| 0)
(fun U71 3)
(fun x 2)
(fun and 2)
(fun isNatKind 1)
(rule (active (U11 tt V1 V2)) (mark (U12 (isNat V1) V2)))
(rule (active (U12 tt V2)) (mark (U13 (isNat V2))))
(rule (active (U13 tt)) (mark tt))
(rule (active (U21 tt V1)) (mark (U22 (isNat V1))))
(rule (active (U22 tt)) (mark tt))
(rule (active (U31 tt V1 V2)) (mark (U32 (isNat V1) V2)))
(rule (active (U32 tt V2)) (mark (U33 (isNat V2))))
(rule (active (U33 tt)) (mark tt))
(rule (active (U41 tt N)) (mark N))
(rule (active (U51 tt M N)) (mark (s (plus N M))))
(rule (active (U61 tt)) (mark |0|))
(rule (active (U71 tt M N)) (mark (plus (x N M) N)))
(rule (active (and tt X)) (mark X))
(rule (active (isNat |0|)) (mark tt))
(rule (active (isNat (plus V1 V2))) (mark (U11 (and (isNatKind V1) (isNatKind V2)) V1 V2)))
(rule (active (isNat (s V1))) (mark (U21 (isNatKind V1) V1)))
(rule (active (isNat (x V1 V2))) (mark (U31 (and (isNatKind V1) (isNatKind V2)) V1 V2)))
(rule (active (isNatKind |0|)) (mark tt))
(rule (active (isNatKind (plus V1 V2))) (mark (and (isNatKind V1) (isNatKind V2))))
(rule (active (isNatKind (s V1))) (mark (isNatKind V1)))
(rule (active (isNatKind (x V1 V2))) (mark (and (isNatKind V1) (isNatKind V2))))
(rule (active (plus N |0|)) (mark (U41 (and (isNat N) (isNatKind N)) N)))
(rule (active (plus N (s M))) (mark (U51 (and (and (isNat M) (isNatKind M)) (and (isNat N) (isNatKind N))) M N)))
(rule (active (x N |0|)) (mark (U61 (and (isNat N) (isNatKind N)))))
(rule (active (x N (s M))) (mark (U71 (and (and (isNat M) (isNatKind M)) (and (isNat N) (isNatKind N))) M N)))
(rule (mark (U11 X1 X2 X3)) (active (U11 (mark X1) X2 X3)))
(rule (mark tt) (active tt))
(rule (mark (U12 X1 X2)) (active (U12 (mark X1) X2)))
(rule (mark (isNat X)) (active (isNat X)))
(rule (mark (U13 X)) (active (U13 (mark X))))
(rule (mark (U21 X1 X2)) (active (U21 (mark X1) X2)))
(rule (mark (U22 X)) (active (U22 (mark X))))
(rule (mark (U31 X1 X2 X3)) (active (U31 (mark X1) X2 X3)))
(rule (mark (U32 X1 X2)) (active (U32 (mark X1) X2)))
(rule (mark (U33 X)) (active (U33 (mark X))))
(rule (mark (U41 X1 X2)) (active (U41 (mark X1) X2)))
(rule (mark (U51 X1 X2 X3)) (active (U51 (mark X1) X2 X3)))
(rule (mark (s X)) (active (s (mark X))))
(rule (mark (plus X1 X2)) (active (plus (mark X1) (mark X2))))
(rule (mark (U61 X)) (active (U61 (mark X))))
(rule (mark |0|) (active |0|))
(rule (mark (U71 X1 X2 X3)) (active (U71 (mark X1) X2 X3)))
(rule (mark (x X1 X2)) (active (x (mark X1) (mark X2))))
(rule (mark (and X1 X2)) (active (and (mark X1) X2)))
(rule (mark (isNatKind X)) (active (isNatKind X)))
(rule (U11 (mark X1) X2 X3) (U11 X1 X2 X3))
(rule (U11 X1 (mark X2) X3) (U11 X1 X2 X3))
(rule (U11 X1 X2 (mark X3)) (U11 X1 X2 X3))
(rule (U11 (active X1) X2 X3) (U11 X1 X2 X3))
(rule (U11 X1 (active X2) X3) (U11 X1 X2 X3))
(rule (U11 X1 X2 (active X3)) (U11 X1 X2 X3))
(rule (U12 (mark X1) X2) (U12 X1 X2))
(rule (U12 X1 (mark X2)) (U12 X1 X2))
(rule (U12 (active X1) X2) (U12 X1 X2))
(rule (U12 X1 (active X2)) (U12 X1 X2))
(rule (isNat (mark X)) (isNat X))
(rule (isNat (active X)) (isNat X))
(rule (U13 (mark X)) (U13 X))
(rule (U13 (active X)) (U13 X))
(rule (U21 (mark X1) X2) (U21 X1 X2))
(rule (U21 X1 (mark X2)) (U21 X1 X2))
(rule (U21 (active X1) X2) (U21 X1 X2))
(rule (U21 X1 (active X2)) (U21 X1 X2))
(rule (U22 (mark X)) (U22 X))
(rule (U22 (active X)) (U22 X))
(rule (U31 (mark X1) X2 X3) (U31 X1 X2 X3))
(rule (U31 X1 (mark X2) X3) (U31 X1 X2 X3))
(rule (U31 X1 X2 (mark X3)) (U31 X1 X2 X3))
(rule (U31 (active X1) X2 X3) (U31 X1 X2 X3))
(rule (U31 X1 (active X2) X3) (U31 X1 X2 X3))
(rule (U31 X1 X2 (active X3)) (U31 X1 X2 X3))
(rule (U32 (mark X1) X2) (U32 X1 X2))
(rule (U32 X1 (mark X2)) (U32 X1 X2))
(rule (U32 (active X1) X2) (U32 X1 X2))
(rule (U32 X1 (active X2)) (U32 X1 X2))
(rule (U33 (mark X)) (U33 X))
(rule (U33 (active X)) (U33 X))
(rule (U41 (mark X1) X2) (U41 X1 X2))
(rule (U41 X1 (mark X2)) (U41 X1 X2))
(rule (U41 (active X1) X2) (U41 X1 X2))
(rule (U41 X1 (active X2)) (U41 X1 X2))
(rule (U51 (mark X1) X2 X3) (U51 X1 X2 X3))
(rule (U51 X1 (mark X2) X3) (U51 X1 X2 X3))
(rule (U51 X1 X2 (mark X3)) (U51 X1 X2 X3))
(rule (U51 (active X1) X2 X3) (U51 X1 X2 X3))
(rule (U51 X1 (active X2) X3) (U51 X1 X2 X3))
(rule (U51 X1 X2 (active X3)) (U51 X1 X2 X3))
(rule (s (mark X)) (s X))
(rule (s (active X)) (s X))
(rule (plus (mark X1) X2) (plus X1 X2))
(rule (plus X1 (mark X2)) (plus X1 X2))
(rule (plus (active X1) X2) (plus X1 X2))
(rule (plus X1 (active X2)) (plus X1 X2))
(rule (U61 (mark X)) (U61 X))
(rule (U61 (active X)) (U61 X))
(rule (U71 (mark X1) X2 X3) (U71 X1 X2 X3))
(rule (U71 X1 (mark X2) X3) (U71 X1 X2 X3))
(rule (U71 X1 X2 (mark X3)) (U71 X1 X2 X3))
(rule (U71 (active X1) X2 X3) (U71 X1 X2 X3))
(rule (U71 X1 (active X2) X3) (U71 X1 X2 X3))
(rule (U71 X1 X2 (active X3)) (U71 X1 X2 X3))
(rule (x (mark X1) X2) (x X1 X2))
(rule (x X1 (mark X2)) (x X1 X2))
(rule (x (active X1) X2) (x X1 X2))
(rule (x X1 (active X2)) (x X1 X2))
(rule (and (mark X1) X2) (and X1 X2))
(rule (and X1 (mark X2)) (and X1 X2))
(rule (and (active X1) X2) (and X1 X2))
(rule (and X1 (active X2)) (and X1 X2))
(rule (isNatKind (mark X)) (isNatKind X))
(rule (isNatKind (active X)) (isNatKind X))