; @origtpdbfilename ./TRS/TRCSR/MYNAT_complete_noand_iGM.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/MYNAT_complete_noand_iGM.xml"
(format TRS)
(fun active 1)
(fun U101 3)
(fun tt 0)
(fun mark 1)
(fun U102 3)
(fun isNatKind 1)
(fun U103 3)
(fun isNat 1)
(fun U104 3)
(fun plus 2)
(fun x 2)
(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 s 1)
(fun U91 2)
(fun U92 1)
(fun |0| 0)
(rule (active (U101 tt M N)) (mark (U102 (isNatKind M) M N)))
(rule (active (U102 tt M N)) (mark (U103 (isNat N) M N)))
(rule (active (U103 tt M N)) (mark (U104 (isNatKind N) M N)))
(rule (active (U104 tt M N)) (mark (plus (x N M) N)))
(rule (active (U11 tt V1 V2)) (mark (U12 (isNatKind V1) V1 V2)))
(rule (active (U12 tt V1 V2)) (mark (U13 (isNatKind V2) V1 V2)))
(rule (active (U13 tt V1 V2)) (mark (U14 (isNatKind V2) V1 V2)))
(rule (active (U14 tt V1 V2)) (mark (U15 (isNat V1) V2)))
(rule (active (U15 tt V2)) (mark (U16 (isNat V2))))
(rule (active (U16 tt)) (mark tt))
(rule (active (U21 tt V1)) (mark (U22 (isNatKind V1) V1)))
(rule (active (U22 tt V1)) (mark (U23 (isNat V1))))
(rule (active (U23 tt)) (mark tt))
(rule (active (U31 tt V1 V2)) (mark (U32 (isNatKind V1) V1 V2)))
(rule (active (U32 tt V1 V2)) (mark (U33 (isNatKind V2) V1 V2)))
(rule (active (U33 tt V1 V2)) (mark (U34 (isNatKind V2) V1 V2)))
(rule (active (U34 tt V1 V2)) (mark (U35 (isNat V1) V2)))
(rule (active (U35 tt V2)) (mark (U36 (isNat V2))))
(rule (active (U36 tt)) (mark tt))
(rule (active (U41 tt V2)) (mark (U42 (isNatKind V2))))
(rule (active (U42 tt)) (mark tt))
(rule (active (U51 tt)) (mark tt))
(rule (active (U61 tt V2)) (mark (U62 (isNatKind V2))))
(rule (active (U62 tt)) (mark tt))
(rule (active (U71 tt N)) (mark (U72 (isNatKind N) N)))
(rule (active (U72 tt N)) (mark N))
(rule (active (U81 tt M N)) (mark (U82 (isNatKind M) M N)))
(rule (active (U82 tt M N)) (mark (U83 (isNat N) M N)))
(rule (active (U83 tt M N)) (mark (U84 (isNatKind N) M N)))
(rule (active (U84 tt M N)) (mark (s (plus N M))))
(rule (active (U91 tt N)) (mark (U92 (isNatKind N))))
(rule (active (U92 tt)) (mark |0|))
(rule (active (isNat |0|)) (mark tt))
(rule (active (isNat (plus V1 V2))) (mark (U11 (isNatKind V1) V1 V2)))
(rule (active (isNat (s V1))) (mark (U21 (isNatKind V1) V1)))
(rule (active (isNat (x V1 V2))) (mark (U31 (isNatKind V1) V1 V2)))
(rule (active (isNatKind |0|)) (mark tt))
(rule (active (isNatKind (plus V1 V2))) (mark (U41 (isNatKind V1) V2)))
(rule (active (isNatKind (s V1))) (mark (U51 (isNatKind V1))))
(rule (active (isNatKind (x V1 V2))) (mark (U61 (isNatKind V1) V2)))
(rule (active (plus N |0|)) (mark (U71 (isNat N) N)))
(rule (active (plus N (s M))) (mark (U81 (isNat M) M N)))
(rule (active (x N |0|)) (mark (U91 (isNat N) N)))
(rule (active (x N (s M))) (mark (U101 (isNat M) M N)))
(rule (mark (U101 X1 X2 X3)) (active (U101 (mark X1) X2 X3)))
(rule (mark tt) (active tt))
(rule (mark (U102 X1 X2 X3)) (active (U102 (mark X1) X2 X3)))
(rule (mark (isNatKind X)) (active (isNatKind X)))
(rule (mark (U103 X1 X2 X3)) (active (U103 (mark X1) X2 X3)))
(rule (mark (isNat X)) (active (isNat X)))
(rule (mark (U104 X1 X2 X3)) (active (U104 (mark X1) X2 X3)))
(rule (mark (plus X1 X2)) (active (plus (mark X1) (mark X2))))
(rule (mark (x X1 X2)) (active (x (mark X1) (mark X2))))
(rule (mark (U11 X1 X2 X3)) (active (U11 (mark X1) X2 X3)))
(rule (mark (U12 X1 X2 X3)) (active (U12 (mark X1) X2 X3)))
(rule (mark (U13 X1 X2 X3)) (active (U13 (mark X1) X2 X3)))
(rule (mark (U14 X1 X2 X3)) (active (U14 (mark X1) X2 X3)))
(rule (mark (U15 X1 X2)) (active (U15 (mark X1) X2)))
(rule (mark (U16 X)) (active (U16 (mark X))))
(rule (mark (U21 X1 X2)) (active (U21 (mark X1) X2)))
(rule (mark (U22 X1 X2)) (active (U22 (mark X1) X2)))
(rule (mark (U23 X)) (active (U23 (mark X))))
(rule (mark (U31 X1 X2 X3)) (active (U31 (mark X1) X2 X3)))
(rule (mark (U32 X1 X2 X3)) (active (U32 (mark X1) X2 X3)))
(rule (mark (U33 X1 X2 X3)) (active (U33 (mark X1) X2 X3)))
(rule (mark (U34 X1 X2 X3)) (active (U34 (mark X1) X2 X3)))
(rule (mark (U35 X1 X2)) (active (U35 (mark X1) X2)))
(rule (mark (U36 X)) (active (U36 (mark X))))
(rule (mark (U41 X1 X2)) (active (U41 (mark X1) X2)))
(rule (mark (U42 X)) (active (U42 (mark X))))
(rule (mark (U51 X)) (active (U51 (mark X))))
(rule (mark (U61 X1 X2)) (active (U61 (mark X1) X2)))
(rule (mark (U62 X)) (active (U62 (mark X))))
(rule (mark (U71 X1 X2)) (active (U71 (mark X1) X2)))
(rule (mark (U72 X1 X2)) (active (U72 (mark X1) X2)))
(rule (mark (U81 X1 X2 X3)) (active (U81 (mark X1) X2 X3)))
(rule (mark (U82 X1 X2 X3)) (active (U82 (mark X1) X2 X3)))
(rule (mark (U83 X1 X2 X3)) (active (U83 (mark X1) X2 X3)))
(rule (mark (U84 X1 X2 X3)) (active (U84 (mark X1) X2 X3)))
(rule (mark (s X)) (active (s (mark X))))
(rule (mark (U91 X1 X2)) (active (U91 (mark X1) X2)))
(rule (mark (U92 X)) (active (U92 (mark X))))
(rule (mark |0|) (active |0|))
(rule (U101 (mark X1) X2 X3) (U101 X1 X2 X3))
(rule (U101 X1 (mark X2) X3) (U101 X1 X2 X3))
(rule (U101 X1 X2 (mark X3)) (U101 X1 X2 X3))
(rule (U101 (active X1) X2 X3) (U101 X1 X2 X3))
(rule (U101 X1 (active X2) X3) (U101 X1 X2 X3))
(rule (U101 X1 X2 (active X3)) (U101 X1 X2 X3))
(rule (U102 (mark X1) X2 X3) (U102 X1 X2 X3))
(rule (U102 X1 (mark X2) X3) (U102 X1 X2 X3))
(rule (U102 X1 X2 (mark X3)) (U102 X1 X2 X3))
(rule (U102 (active X1) X2 X3) (U102 X1 X2 X3))
(rule (U102 X1 (active X2) X3) (U102 X1 X2 X3))
(rule (U102 X1 X2 (active X3)) (U102 X1 X2 X3))
(rule (isNatKind (mark X)) (isNatKind X))
(rule (isNatKind (active X)) (isNatKind X))
(rule (U103 (mark X1) X2 X3) (U103 X1 X2 X3))
(rule (U103 X1 (mark X2) X3) (U103 X1 X2 X3))
(rule (U103 X1 X2 (mark X3)) (U103 X1 X2 X3))
(rule (U103 (active X1) X2 X3) (U103 X1 X2 X3))
(rule (U103 X1 (active X2) X3) (U103 X1 X2 X3))
(rule (U103 X1 X2 (active X3)) (U103 X1 X2 X3))
(rule (isNat (mark X)) (isNat X))
(rule (isNat (active X)) (isNat X))
(rule (U104 (mark X1) X2 X3) (U104 X1 X2 X3))
(rule (U104 X1 (mark X2) X3) (U104 X1 X2 X3))
(rule (U104 X1 X2 (mark X3)) (U104 X1 X2 X3))
(rule (U104 (active X1) X2 X3) (U104 X1 X2 X3))
(rule (U104 X1 (active X2) X3) (U104 X1 X2 X3))
(rule (U104 X1 X2 (active X3)) (U104 X1 X2 X3))
(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 (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 (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 X3) (U12 X1 X2 X3))
(rule (U12 X1 (mark X2) X3) (U12 X1 X2 X3))
(rule (U12 X1 X2 (mark X3)) (U12 X1 X2 X3))
(rule (U12 (active X1) X2 X3) (U12 X1 X2 X3))
(rule (U12 X1 (active X2) X3) (U12 X1 X2 X3))
(rule (U12 X1 X2 (active X3)) (U12 X1 X2 X3))
(rule (U13 (mark X1) X2 X3) (U13 X1 X2 X3))
(rule (U13 X1 (mark X2) X3) (U13 X1 X2 X3))
(rule (U13 X1 X2 (mark X3)) (U13 X1 X2 X3))
(rule (U13 (active X1) X2 X3) (U13 X1 X2 X3))
(rule (U13 X1 (active X2) X3) (U13 X1 X2 X3))
(rule (U13 X1 X2 (active X3)) (U13 X1 X2 X3))
(rule (U14 (mark X1) X2 X3) (U14 X1 X2 X3))
(rule (U14 X1 (mark X2) X3) (U14 X1 X2 X3))
(rule (U14 X1 X2 (mark X3)) (U14 X1 X2 X3))
(rule (U14 (active X1) X2 X3) (U14 X1 X2 X3))
(rule (U14 X1 (active X2) X3) (U14 X1 X2 X3))
(rule (U14 X1 X2 (active X3)) (U14 X1 X2 X3))
(rule (U15 (mark X1) X2) (U15 X1 X2))
(rule (U15 X1 (mark X2)) (U15 X1 X2))
(rule (U15 (active X1) X2) (U15 X1 X2))
(rule (U15 X1 (active X2)) (U15 X1 X2))
(rule (U16 (mark X)) (U16 X))
(rule (U16 (active X)) (U16 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 X1) X2) (U22 X1 X2))
(rule (U22 X1 (mark X2)) (U22 X1 X2))
(rule (U22 (active X1) X2) (U22 X1 X2))
(rule (U22 X1 (active X2)) (U22 X1 X2))
(rule (U23 (mark X)) (U23 X))
(rule (U23 (active X)) (U23 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 X3) (U32 X1 X2 X3))
(rule (U32 X1 (mark X2) X3) (U32 X1 X2 X3))
(rule (U32 X1 X2 (mark X3)) (U32 X1 X2 X3))
(rule (U32 (active X1) X2 X3) (U32 X1 X2 X3))
(rule (U32 X1 (active X2) X3) (U32 X1 X2 X3))
(rule (U32 X1 X2 (active X3)) (U32 X1 X2 X3))
(rule (U33 (mark X1) X2 X3) (U33 X1 X2 X3))
(rule (U33 X1 (mark X2) X3) (U33 X1 X2 X3))
(rule (U33 X1 X2 (mark X3)) (U33 X1 X2 X3))
(rule (U33 (active X1) X2 X3) (U33 X1 X2 X3))
(rule (U33 X1 (active X2) X3) (U33 X1 X2 X3))
(rule (U33 X1 X2 (active X3)) (U33 X1 X2 X3))
(rule (U34 (mark X1) X2 X3) (U34 X1 X2 X3))
(rule (U34 X1 (mark X2) X3) (U34 X1 X2 X3))
(rule (U34 X1 X2 (mark X3)) (U34 X1 X2 X3))
(rule (U34 (active X1) X2 X3) (U34 X1 X2 X3))
(rule (U34 X1 (active X2) X3) (U34 X1 X2 X3))
(rule (U34 X1 X2 (active X3)) (U34 X1 X2 X3))
(rule (U35 (mark X1) X2) (U35 X1 X2))
(rule (U35 X1 (mark X2)) (U35 X1 X2))
(rule (U35 (active X1) X2) (U35 X1 X2))
(rule (U35 X1 (active X2)) (U35 X1 X2))
(rule (U36 (mark X)) (U36 X))
(rule (U36 (active X)) (U36 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 (U42 (mark X)) (U42 X))
(rule (U42 (active X)) (U42 X))
(rule (U51 (mark X)) (U51 X))
(rule (U51 (active X)) (U51 X))
(rule (U61 (mark X1) X2) (U61 X1 X2))
(rule (U61 X1 (mark X2)) (U61 X1 X2))
(rule (U61 (active X1) X2) (U61 X1 X2))
(rule (U61 X1 (active X2)) (U61 X1 X2))
(rule (U62 (mark X)) (U62 X))
(rule (U62 (active X)) (U62 X))
(rule (U71 (mark X1) X2) (U71 X1 X2))
(rule (U71 X1 (mark X2)) (U71 X1 X2))
(rule (U71 (active X1) X2) (U71 X1 X2))
(rule (U71 X1 (active X2)) (U71 X1 X2))
(rule (U72 (mark X1) X2) (U72 X1 X2))
(rule (U72 X1 (mark X2)) (U72 X1 X2))
(rule (U72 (active X1) X2) (U72 X1 X2))
(rule (U72 X1 (active X2)) (U72 X1 X2))
(rule (U81 (mark X1) X2 X3) (U81 X1 X2 X3))
(rule (U81 X1 (mark X2) X3) (U81 X1 X2 X3))
(rule (U81 X1 X2 (mark X3)) (U81 X1 X2 X3))
(rule (U81 (active X1) X2 X3) (U81 X1 X2 X3))
(rule (U81 X1 (active X2) X3) (U81 X1 X2 X3))
(rule (U81 X1 X2 (active X3)) (U81 X1 X2 X3))
(rule (U82 (mark X1) X2 X3) (U82 X1 X2 X3))
(rule (U82 X1 (mark X2) X3) (U82 X1 X2 X3))
(rule (U82 X1 X2 (mark X3)) (U82 X1 X2 X3))
(rule (U82 (active X1) X2 X3) (U82 X1 X2 X3))
(rule (U82 X1 (active X2) X3) (U82 X1 X2 X3))
(rule (U82 X1 X2 (active X3)) (U82 X1 X2 X3))
(rule (U83 (mark X1) X2 X3) (U83 X1 X2 X3))
(rule (U83 X1 (mark X2) X3) (U83 X1 X2 X3))
(rule (U83 X1 X2 (mark X3)) (U83 X1 X2 X3))
(rule (U83 (active X1) X2 X3) (U83 X1 X2 X3))
(rule (U83 X1 (active X2) X3) (U83 X1 X2 X3))
(rule (U83 X1 X2 (active X3)) (U83 X1 X2 X3))
(rule (U84 (mark X1) X2 X3) (U84 X1 X2 X3))
(rule (U84 X1 (mark X2) X3) (U84 X1 X2 X3))
(rule (U84 X1 X2 (mark X3)) (U84 X1 X2 X3))
(rule (U84 (active X1) X2 X3) (U84 X1 X2 X3))
(rule (U84 X1 (active X2) X3) (U84 X1 X2 X3))
(rule (U84 X1 X2 (active X3)) (U84 X1 X2 X3))
(rule (s (mark X)) (s X))
(rule (s (active X)) (s X))
(rule (U91 (mark X1) X2) (U91 X1 X2))
(rule (U91 X1 (mark X2)) (U91 X1 X2))
(rule (U91 (active X1) X2) (U91 X1 X2))
(rule (U91 X1 (active X2)) (U91 X1 X2))
(rule (U92 (mark X)) (U92 X))
(rule (U92 (active X)) (U92 X))