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