; @origtpdbfilename ./TRS/TRCSR/MYNAT_complete_noand_GM.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/MYNAT_complete_noand_GM.xml"
(format TRS)
(fun a__U101 3)
(fun tt 0)
(fun a__U102 3)
(fun a__isNatKind 1)
(fun a__U103 3)
(fun a__isNat 1)
(fun a__U104 3)
(fun a__plus 2)
(fun a__x 2)
(fun mark 1)
(fun a__U11 3)
(fun a__U12 3)
(fun a__U13 3)
(fun a__U14 3)
(fun a__U15 2)
(fun a__U16 1)
(fun a__U21 2)
(fun a__U22 2)
(fun a__U23 1)
(fun a__U31 3)
(fun a__U32 3)
(fun a__U33 3)
(fun a__U34 3)
(fun a__U35 2)
(fun a__U36 1)
(fun a__U41 2)
(fun a__U42 1)
(fun a__U51 1)
(fun a__U61 2)
(fun a__U62 1)
(fun a__U71 2)
(fun a__U72 2)
(fun a__U81 3)
(fun a__U82 3)
(fun a__U83 3)
(fun a__U84 3)
(fun s 1)
(fun a__U91 2)
(fun a__U92 1)
(fun |0| 0)
(fun plus 2)
(fun x 2)
(fun U101 3)
(fun U102 3)
(fun isNatKind 1)
(fun U103 3)
(fun isNat 1)
(fun U104 3)
(fun U11 3)
(fun U12 3)
(fun U13 3)
(fun U14 3)
(fun U15 2)
(fun U16 1)
(fun U21 2)
(fun U22 2)
(fun U23 1)
(fun U31 3)
(fun U32 3)
(fun U33 3)
(fun U34 3)
(fun U35 2)
(fun U36 1)
(fun U41 2)
(fun U42 1)
(fun U51 1)
(fun U61 2)
(fun U62 1)
(fun U71 2)
(fun U72 2)
(fun U81 3)
(fun U82 3)
(fun U83 3)
(fun U84 3)
(fun U91 2)
(fun U92 1)
(rule (a__U101 tt M N) (a__U102 (a__isNatKind M) M N))
(rule (a__U102 tt M N) (a__U103 (a__isNat N) M N))
(rule (a__U103 tt M N) (a__U104 (a__isNatKind N) M N))
(rule (a__U104 tt M N) (a__plus (a__x (mark N) (mark M)) (mark N)))
(rule (a__U11 tt V1 V2) (a__U12 (a__isNatKind V1) V1 V2))
(rule (a__U12 tt V1 V2) (a__U13 (a__isNatKind V2) V1 V2))
(rule (a__U13 tt V1 V2) (a__U14 (a__isNatKind V2) V1 V2))
(rule (a__U14 tt V1 V2) (a__U15 (a__isNat V1) V2))
(rule (a__U15 tt V2) (a__U16 (a__isNat V2)))
(rule (a__U16 tt) tt)
(rule (a__U21 tt V1) (a__U22 (a__isNatKind V1) V1))
(rule (a__U22 tt V1) (a__U23 (a__isNat V1)))
(rule (a__U23 tt) tt)
(rule (a__U31 tt V1 V2) (a__U32 (a__isNatKind V1) V1 V2))
(rule (a__U32 tt V1 V2) (a__U33 (a__isNatKind V2) V1 V2))
(rule (a__U33 tt V1 V2) (a__U34 (a__isNatKind V2) V1 V2))
(rule (a__U34 tt V1 V2) (a__U35 (a__isNat V1) V2))
(rule (a__U35 tt V2) (a__U36 (a__isNat V2)))
(rule (a__U36 tt) tt)
(rule (a__U41 tt V2) (a__U42 (a__isNatKind V2)))
(rule (a__U42 tt) tt)
(rule (a__U51 tt) tt)
(rule (a__U61 tt V2) (a__U62 (a__isNatKind V2)))
(rule (a__U62 tt) tt)
(rule (a__U71 tt N) (a__U72 (a__isNatKind N) N))
(rule (a__U72 tt N) (mark N))
(rule (a__U81 tt M N) (a__U82 (a__isNatKind M) M N))
(rule (a__U82 tt M N) (a__U83 (a__isNat N) M N))
(rule (a__U83 tt M N) (a__U84 (a__isNatKind N) M N))
(rule (a__U84 tt M N) (s (a__plus (mark N) (mark M))))
(rule (a__U91 tt N) (a__U92 (a__isNatKind N)))
(rule (a__U92 tt) |0|)
(rule (a__isNat |0|) tt)
(rule (a__isNat (plus V1 V2)) (a__U11 (a__isNatKind V1) V1 V2))
(rule (a__isNat (s V1)) (a__U21 (a__isNatKind V1) V1))
(rule (a__isNat (x V1 V2)) (a__U31 (a__isNatKind V1) V1 V2))
(rule (a__isNatKind |0|) tt)
(rule (a__isNatKind (plus V1 V2)) (a__U41 (a__isNatKind V1) V2))
(rule (a__isNatKind (s V1)) (a__U51 (a__isNatKind V1)))
(rule (a__isNatKind (x V1 V2)) (a__U61 (a__isNatKind V1) V2))
(rule (a__plus N |0|) (a__U71 (a__isNat N) N))
(rule (a__plus N (s M)) (a__U81 (a__isNat M) M N))
(rule (a__x N |0|) (a__U91 (a__isNat N) N))
(rule (a__x N (s M)) (a__U101 (a__isNat M) M N))
(rule (mark (U101 X1 X2 X3)) (a__U101 (mark X1) X2 X3))
(rule (mark (U102 X1 X2 X3)) (a__U102 (mark X1) X2 X3))
(rule (mark (isNatKind X)) (a__isNatKind X))
(rule (mark (U103 X1 X2 X3)) (a__U103 (mark X1) X2 X3))
(rule (mark (isNat X)) (a__isNat X))
(rule (mark (U104 X1 X2 X3)) (a__U104 (mark X1) X2 X3))
(rule (mark (plus X1 X2)) (a__plus (mark X1) (mark X2)))
(rule (mark (x X1 X2)) (a__x (mark X1) (mark X2)))
(rule (mark (U11 X1 X2 X3)) (a__U11 (mark X1) X2 X3))
(rule (mark (U12 X1 X2 X3)) (a__U12 (mark X1) X2 X3))
(rule (mark (U13 X1 X2 X3)) (a__U13 (mark X1) X2 X3))
(rule (mark (U14 X1 X2 X3)) (a__U14 (mark X1) X2 X3))
(rule (mark (U15 X1 X2)) (a__U15 (mark X1) X2))
(rule (mark (U16 X)) (a__U16 (mark X)))
(rule (mark (U21 X1 X2)) (a__U21 (mark X1) X2))
(rule (mark (U22 X1 X2)) (a__U22 (mark X1) X2))
(rule (mark (U23 X)) (a__U23 (mark X)))
(rule (mark (U31 X1 X2 X3)) (a__U31 (mark X1) X2 X3))
(rule (mark (U32 X1 X2 X3)) (a__U32 (mark X1) X2 X3))
(rule (mark (U33 X1 X2 X3)) (a__U33 (mark X1) X2 X3))
(rule (mark (U34 X1 X2 X3)) (a__U34 (mark X1) X2 X3))
(rule (mark (U35 X1 X2)) (a__U35 (mark X1) X2))
(rule (mark (U36 X)) (a__U36 (mark X)))
(rule (mark (U41 X1 X2)) (a__U41 (mark X1) X2))
(rule (mark (U42 X)) (a__U42 (mark X)))
(rule (mark (U51 X)) (a__U51 (mark X)))
(rule (mark (U61 X1 X2)) (a__U61 (mark X1) X2))
(rule (mark (U62 X)) (a__U62 (mark X)))
(rule (mark (U71 X1 X2)) (a__U71 (mark X1) X2))
(rule (mark (U72 X1 X2)) (a__U72 (mark X1) X2))
(rule (mark (U81 X1 X2 X3)) (a__U81 (mark X1) X2 X3))
(rule (mark (U82 X1 X2 X3)) (a__U82 (mark X1) X2 X3))
(rule (mark (U83 X1 X2 X3)) (a__U83 (mark X1) X2 X3))
(rule (mark (U84 X1 X2 X3)) (a__U84 (mark X1) X2 X3))
(rule (mark (U91 X1 X2)) (a__U91 (mark X1) X2))
(rule (mark (U92 X)) (a__U92 (mark X)))
(rule (mark tt) tt)
(rule (mark (s X)) (s (mark X)))
(rule (mark |0|) |0|)
(rule (a__U101 X1 X2 X3) (U101 X1 X2 X3))
(rule (a__U102 X1 X2 X3) (U102 X1 X2 X3))
(rule (a__isNatKind X) (isNatKind X))
(rule (a__U103 X1 X2 X3) (U103 X1 X2 X3))
(rule (a__isNat X) (isNat X))
(rule (a__U104 X1 X2 X3) (U104 X1 X2 X3))
(rule (a__plus X1 X2) (plus X1 X2))
(rule (a__x X1 X2) (x X1 X2))
(rule (a__U11 X1 X2 X3) (U11 X1 X2 X3))
(rule (a__U12 X1 X2 X3) (U12 X1 X2 X3))
(rule (a__U13 X1 X2 X3) (U13 X1 X2 X3))
(rule (a__U14 X1 X2 X3) (U14 X1 X2 X3))
(rule (a__U15 X1 X2) (U15 X1 X2))
(rule (a__U16 X) (U16 X))
(rule (a__U21 X1 X2) (U21 X1 X2))
(rule (a__U22 X1 X2) (U22 X1 X2))
(rule (a__U23 X) (U23 X))
(rule (a__U31 X1 X2 X3) (U31 X1 X2 X3))
(rule (a__U32 X1 X2 X3) (U32 X1 X2 X3))
(rule (a__U33 X1 X2 X3) (U33 X1 X2 X3))
(rule (a__U34 X1 X2 X3) (U34 X1 X2 X3))
(rule (a__U35 X1 X2) (U35 X1 X2))
(rule (a__U36 X) (U36 X))
(rule (a__U41 X1 X2) (U41 X1 X2))
(rule (a__U42 X) (U42 X))
(rule (a__U51 X) (U51 X))
(rule (a__U61 X1 X2) (U61 X1 X2))
(rule (a__U62 X) (U62 X))
(rule (a__U71 X1 X2) (U71 X1 X2))
(rule (a__U72 X1 X2) (U72 X1 X2))
(rule (a__U81 X1 X2 X3) (U81 X1 X2 X3))
(rule (a__U82 X1 X2 X3) (U82 X1 X2 X3))
(rule (a__U83 X1 X2 X3) (U83 X1 X2 X3))
(rule (a__U84 X1 X2 X3) (U84 X1 X2 X3))
(rule (a__U91 X1 X2) (U91 X1 X2))
(rule (a__U92 X) (U92 X))