Runtime Complexity TRS:
The TRS R consists of the following rules:

a__U101(tt, M, N) → a__U102(a__isNatKind(M), M, N)
a__U102(tt, M, N) → a__U103(a__isNat(N), M, N)
a__U103(tt, M, N) → a__U104(a__isNatKind(N), M, N)
a__U104(tt, M, N) → a__plus(a__x(mark(N), mark(M)), mark(N))
a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)
a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)
a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))
a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)
a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tt
a__U31(tt, V1, V2) → a__U32(a__isNatKind(V1), V1, V2)
a__U32(tt, V1, V2) → a__U33(a__isNatKind(V2), V1, V2)
a__U33(tt, V1, V2) → a__U34(a__isNatKind(V2), V1, V2)
a__U34(tt, V1, V2) → a__U35(a__isNat(V1), V2)
a__U35(tt, V2) → a__U36(a__isNat(V2))
a__U36(tt) → tt
a__U41(tt, V2) → a__U42(a__isNatKind(V2))
a__U42(tt) → tt
a__U51(tt) → tt
a__U61(tt, V2) → a__U62(a__isNatKind(V2))
a__U62(tt) → tt
a__U71(tt, N) → a__U72(a__isNatKind(N), N)
a__U72(tt, N) → mark(N)
a__U81(tt, M, N) → a__U82(a__isNatKind(M), M, N)
a__U82(tt, M, N) → a__U83(a__isNat(N), M, N)
a__U83(tt, M, N) → a__U84(a__isNatKind(N), M, N)
a__U84(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__U91(tt, N) → a__U92(a__isNatKind(N))
a__U92(tt) → 0
a__isNat(0) → tt
a__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)
a__isNat(x(V1, V2)) → a__U31(a__isNatKind(V1), V1, V2)
a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U41(a__isNatKind(V1), V2)
a__isNatKind(s(V1)) → a__U51(a__isNatKind(V1))
a__isNatKind(x(V1, V2)) → a__U61(a__isNatKind(V1), V2)
a__plus(N, 0) → a__U71(a__isNat(N), N)
a__plus(N, s(M)) → a__U81(a__isNat(M), M, N)
a__x(N, 0) → a__U91(a__isNat(N), N)
a__x(N, s(M)) → a__U101(a__isNat(M), M, N)
mark(U101(X1, X2, X3)) → a__U101(mark(X1), X2, X3)
mark(U102(X1, X2, X3)) → a__U102(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)
mark(U103(X1, X2, X3)) → a__U103(mark(X1), X2, X3)
mark(isNat(X)) → a__isNat(X)
mark(U104(X1, X2, X3)) → a__U104(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))
mark(x(X1, X2)) → a__x(mark(X1), mark(X2))
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)
mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)
mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))
mark(U31(X1, X2, X3)) → a__U31(mark(X1), X2, X3)
mark(U32(X1, X2, X3)) → a__U32(mark(X1), X2, X3)
mark(U33(X1, X2, X3)) → a__U33(mark(X1), X2, X3)
mark(U34(X1, X2, X3)) → a__U34(mark(X1), X2, X3)
mark(U35(X1, X2)) → a__U35(mark(X1), X2)
mark(U36(X)) → a__U36(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(U51(X)) → a__U51(mark(X))
mark(U61(X1, X2)) → a__U61(mark(X1), X2)
mark(U62(X)) → a__U62(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X1, X2)) → a__U72(mark(X1), X2)
mark(U81(X1, X2, X3)) → a__U81(mark(X1), X2, X3)
mark(U82(X1, X2, X3)) → a__U82(mark(X1), X2, X3)
mark(U83(X1, X2, X3)) → a__U83(mark(X1), X2, X3)
mark(U84(X1, X2, X3)) → a__U84(mark(X1), X2, X3)
mark(U91(X1, X2)) → a__U91(mark(X1), X2)
mark(U92(X)) → a__U92(mark(X))
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(0) → 0
a__U101(X1, X2, X3) → U101(X1, X2, X3)
a__U102(X1, X2, X3) → U102(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)
a__U103(X1, X2, X3) → U103(X1, X2, X3)
a__isNat(X) → isNat(X)
a__U104(X1, X2, X3) → U104(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)
a__x(X1, X2) → x(X1, X2)
a__U11(X1, X2, X3) → U11(X1, X2, X3)
a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)
a__U15(X1, X2) → U15(X1, X2)
a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)
a__U31(X1, X2, X3) → U31(X1, X2, X3)
a__U32(X1, X2, X3) → U32(X1, X2, X3)
a__U33(X1, X2, X3) → U33(X1, X2, X3)
a__U34(X1, X2, X3) → U34(X1, X2, X3)
a__U35(X1, X2) → U35(X1, X2)
a__U36(X) → U36(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__U51(X) → U51(X)
a__U61(X1, X2) → U61(X1, X2)
a__U62(X) → U62(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X1, X2) → U72(X1, X2)
a__U81(X1, X2, X3) → U81(X1, X2, X3)
a__U82(X1, X2, X3) → U82(X1, X2, X3)
a__U83(X1, X2, X3) → U83(X1, X2, X3)
a__U84(X1, X2, X3) → U84(X1, X2, X3)
a__U91(X1, X2) → U91(X1, X2)
a__U92(X) → U92(X)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:

a__U101'(tt', M, N) → a__U102'(a__isNatKind'(M), M, N)
a__U102'(tt', M, N) → a__U103'(a__isNat'(N), M, N)
a__U103'(tt', M, N) → a__U104'(a__isNatKind'(N), M, N)
a__U104'(tt', M, N) → a__plus'(a__x'(mark'(N), mark'(M)), mark'(N))
a__U11'(tt', V1, V2) → a__U12'(a__isNatKind'(V1), V1, V2)
a__U12'(tt', V1, V2) → a__U13'(a__isNatKind'(V2), V1, V2)
a__U13'(tt', V1, V2) → a__U14'(a__isNatKind'(V2), V1, V2)
a__U14'(tt', V1, V2) → a__U15'(a__isNat'(V1), V2)
a__U15'(tt', V2) → a__U16'(a__isNat'(V2))
a__U16'(tt') → tt'
a__U21'(tt', V1) → a__U22'(a__isNatKind'(V1), V1)
a__U22'(tt', V1) → a__U23'(a__isNat'(V1))
a__U23'(tt') → tt'
a__U31'(tt', V1, V2) → a__U32'(a__isNatKind'(V1), V1, V2)
a__U32'(tt', V1, V2) → a__U33'(a__isNatKind'(V2), V1, V2)
a__U33'(tt', V1, V2) → a__U34'(a__isNatKind'(V2), V1, V2)
a__U34'(tt', V1, V2) → a__U35'(a__isNat'(V1), V2)
a__U35'(tt', V2) → a__U36'(a__isNat'(V2))
a__U36'(tt') → tt'
a__U41'(tt', V2) → a__U42'(a__isNatKind'(V2))
a__U42'(tt') → tt'
a__U51'(tt') → tt'
a__U61'(tt', V2) → a__U62'(a__isNatKind'(V2))
a__U62'(tt') → tt'
a__U71'(tt', N) → a__U72'(a__isNatKind'(N), N)
a__U72'(tt', N) → mark'(N)
a__U81'(tt', M, N) → a__U82'(a__isNatKind'(M), M, N)
a__U82'(tt', M, N) → a__U83'(a__isNat'(N), M, N)
a__U83'(tt', M, N) → a__U84'(a__isNatKind'(N), M, N)
a__U84'(tt', M, N) → s'(a__plus'(mark'(N), mark'(M)))
a__U91'(tt', N) → a__U92'(a__isNatKind'(N))
a__U92'(tt') → 0'
a__isNat'(0') → tt'
a__isNat'(plus'(V1, V2)) → a__U11'(a__isNatKind'(V1), V1, V2)
a__isNat'(s'(V1)) → a__U21'(a__isNatKind'(V1), V1)
a__isNat'(x'(V1, V2)) → a__U31'(a__isNatKind'(V1), V1, V2)
a__isNatKind'(0') → tt'
a__isNatKind'(plus'(V1, V2)) → a__U41'(a__isNatKind'(V1), V2)
a__isNatKind'(s'(V1)) → a__U51'(a__isNatKind'(V1))
a__isNatKind'(x'(V1, V2)) → a__U61'(a__isNatKind'(V1), V2)
a__plus'(N, 0') → a__U71'(a__isNat'(N), N)
a__plus'(N, s'(M)) → a__U81'(a__isNat'(M), M, N)
a__x'(N, 0') → a__U91'(a__isNat'(N), N)
a__x'(N, s'(M)) → a__U101'(a__isNat'(M), M, N)
mark'(U101'(X1, X2, X3)) → a__U101'(mark'(X1), X2, X3)
mark'(U102'(X1, X2, X3)) → a__U102'(mark'(X1), X2, X3)
mark'(isNatKind'(X)) → a__isNatKind'(X)
mark'(U103'(X1, X2, X3)) → a__U103'(mark'(X1), X2, X3)
mark'(isNat'(X)) → a__isNat'(X)
mark'(U104'(X1, X2, X3)) → a__U104'(mark'(X1), X2, X3)
mark'(plus'(X1, X2)) → a__plus'(mark'(X1), mark'(X2))
mark'(x'(X1, X2)) → a__x'(mark'(X1), mark'(X2))
mark'(U11'(X1, X2, X3)) → a__U11'(mark'(X1), X2, X3)
mark'(U12'(X1, X2, X3)) → a__U12'(mark'(X1), X2, X3)
mark'(U13'(X1, X2, X3)) → a__U13'(mark'(X1), X2, X3)
mark'(U14'(X1, X2, X3)) → a__U14'(mark'(X1), X2, X3)
mark'(U15'(X1, X2)) → a__U15'(mark'(X1), X2)
mark'(U16'(X)) → a__U16'(mark'(X))
mark'(U21'(X1, X2)) → a__U21'(mark'(X1), X2)
mark'(U22'(X1, X2)) → a__U22'(mark'(X1), X2)
mark'(U23'(X)) → a__U23'(mark'(X))
mark'(U31'(X1, X2, X3)) → a__U31'(mark'(X1), X2, X3)
mark'(U32'(X1, X2, X3)) → a__U32'(mark'(X1), X2, X3)
mark'(U33'(X1, X2, X3)) → a__U33'(mark'(X1), X2, X3)
mark'(U34'(X1, X2, X3)) → a__U34'(mark'(X1), X2, X3)
mark'(U35'(X1, X2)) → a__U35'(mark'(X1), X2)
mark'(U36'(X)) → a__U36'(mark'(X))
mark'(U41'(X1, X2)) → a__U41'(mark'(X1), X2)
mark'(U42'(X)) → a__U42'(mark'(X))
mark'(U51'(X)) → a__U51'(mark'(X))
mark'(U61'(X1, X2)) → a__U61'(mark'(X1), X2)
mark'(U62'(X)) → a__U62'(mark'(X))
mark'(U71'(X1, X2)) → a__U71'(mark'(X1), X2)
mark'(U72'(X1, X2)) → a__U72'(mark'(X1), X2)
mark'(U81'(X1, X2, X3)) → a__U81'(mark'(X1), X2, X3)
mark'(U82'(X1, X2, X3)) → a__U82'(mark'(X1), X2, X3)
mark'(U83'(X1, X2, X3)) → a__U83'(mark'(X1), X2, X3)
mark'(U84'(X1, X2, X3)) → a__U84'(mark'(X1), X2, X3)
mark'(U91'(X1, X2)) → a__U91'(mark'(X1), X2)
mark'(U92'(X)) → a__U92'(mark'(X))
mark'(tt') → tt'
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__U101'(X1, X2, X3) → U101'(X1, X2, X3)
a__U102'(X1, X2, X3) → U102'(X1, X2, X3)
a__isNatKind'(X) → isNatKind'(X)
a__U103'(X1, X2, X3) → U103'(X1, X2, X3)
a__isNat'(X) → isNat'(X)
a__U104'(X1, X2, X3) → U104'(X1, X2, X3)
a__plus'(X1, X2) → plus'(X1, X2)
a__x'(X1, X2) → x'(X1, X2)
a__U11'(X1, X2, X3) → U11'(X1, X2, X3)
a__U12'(X1, X2, X3) → U12'(X1, X2, X3)
a__U13'(X1, X2, X3) → U13'(X1, X2, X3)
a__U14'(X1, X2, X3) → U14'(X1, X2, X3)
a__U15'(X1, X2) → U15'(X1, X2)
a__U16'(X) → U16'(X)
a__U21'(X1, X2) → U21'(X1, X2)
a__U22'(X1, X2) → U22'(X1, X2)
a__U23'(X) → U23'(X)
a__U31'(X1, X2, X3) → U31'(X1, X2, X3)
a__U32'(X1, X2, X3) → U32'(X1, X2, X3)
a__U33'(X1, X2, X3) → U33'(X1, X2, X3)
a__U34'(X1, X2, X3) → U34'(X1, X2, X3)
a__U35'(X1, X2) → U35'(X1, X2)
a__U36'(X) → U36'(X)
a__U41'(X1, X2) → U41'(X1, X2)
a__U42'(X) → U42'(X)
a__U51'(X) → U51'(X)
a__U61'(X1, X2) → U61'(X1, X2)
a__U62'(X) → U62'(X)
a__U71'(X1, X2) → U71'(X1, X2)
a__U72'(X1, X2) → U72'(X1, X2)
a__U81'(X1, X2, X3) → U81'(X1, X2, X3)
a__U82'(X1, X2, X3) → U82'(X1, X2, X3)
a__U83'(X1, X2, X3) → U83'(X1, X2, X3)
a__U84'(X1, X2, X3) → U84'(X1, X2, X3)
a__U91'(X1, X2) → U91'(X1, X2)
a__U92'(X) → U92'(X)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
a__U101'(tt', M, N) → a__U102'(a__isNatKind'(M), M, N)
a__U102'(tt', M, N) → a__U103'(a__isNat'(N), M, N)
a__U103'(tt', M, N) → a__U104'(a__isNatKind'(N), M, N)
a__U104'(tt', M, N) → a__plus'(a__x'(mark'(N), mark'(M)), mark'(N))
a__U11'(tt', V1, V2) → a__U12'(a__isNatKind'(V1), V1, V2)
a__U12'(tt', V1, V2) → a__U13'(a__isNatKind'(V2), V1, V2)
a__U13'(tt', V1, V2) → a__U14'(a__isNatKind'(V2), V1, V2)
a__U14'(tt', V1, V2) → a__U15'(a__isNat'(V1), V2)
a__U15'(tt', V2) → a__U16'(a__isNat'(V2))
a__U16'(tt') → tt'
a__U21'(tt', V1) → a__U22'(a__isNatKind'(V1), V1)
a__U22'(tt', V1) → a__U23'(a__isNat'(V1))
a__U23'(tt') → tt'
a__U31'(tt', V1, V2) → a__U32'(a__isNatKind'(V1), V1, V2)
a__U32'(tt', V1, V2) → a__U33'(a__isNatKind'(V2), V1, V2)
a__U33'(tt', V1, V2) → a__U34'(a__isNatKind'(V2), V1, V2)
a__U34'(tt', V1, V2) → a__U35'(a__isNat'(V1), V2)
a__U35'(tt', V2) → a__U36'(a__isNat'(V2))
a__U36'(tt') → tt'
a__U41'(tt', V2) → a__U42'(a__isNatKind'(V2))
a__U42'(tt') → tt'
a__U51'(tt') → tt'
a__U61'(tt', V2) → a__U62'(a__isNatKind'(V2))
a__U62'(tt') → tt'
a__U71'(tt', N) → a__U72'(a__isNatKind'(N), N)
a__U72'(tt', N) → mark'(N)
a__U81'(tt', M, N) → a__U82'(a__isNatKind'(M), M, N)
a__U82'(tt', M, N) → a__U83'(a__isNat'(N), M, N)
a__U83'(tt', M, N) → a__U84'(a__isNatKind'(N), M, N)
a__U84'(tt', M, N) → s'(a__plus'(mark'(N), mark'(M)))
a__U91'(tt', N) → a__U92'(a__isNatKind'(N))
a__U92'(tt') → 0'
a__isNat'(0') → tt'
a__isNat'(plus'(V1, V2)) → a__U11'(a__isNatKind'(V1), V1, V2)
a__isNat'(s'(V1)) → a__U21'(a__isNatKind'(V1), V1)
a__isNat'(x'(V1, V2)) → a__U31'(a__isNatKind'(V1), V1, V2)
a__isNatKind'(0') → tt'
a__isNatKind'(plus'(V1, V2)) → a__U41'(a__isNatKind'(V1), V2)
a__isNatKind'(s'(V1)) → a__U51'(a__isNatKind'(V1))
a__isNatKind'(x'(V1, V2)) → a__U61'(a__isNatKind'(V1), V2)
a__plus'(N, 0') → a__U71'(a__isNat'(N), N)
a__plus'(N, s'(M)) → a__U81'(a__isNat'(M), M, N)
a__x'(N, 0') → a__U91'(a__isNat'(N), N)
a__x'(N, s'(M)) → a__U101'(a__isNat'(M), M, N)
mark'(U101'(X1, X2, X3)) → a__U101'(mark'(X1), X2, X3)
mark'(U102'(X1, X2, X3)) → a__U102'(mark'(X1), X2, X3)
mark'(isNatKind'(X)) → a__isNatKind'(X)
mark'(U103'(X1, X2, X3)) → a__U103'(mark'(X1), X2, X3)
mark'(isNat'(X)) → a__isNat'(X)
mark'(U104'(X1, X2, X3)) → a__U104'(mark'(X1), X2, X3)
mark'(plus'(X1, X2)) → a__plus'(mark'(X1), mark'(X2))
mark'(x'(X1, X2)) → a__x'(mark'(X1), mark'(X2))
mark'(U11'(X1, X2, X3)) → a__U11'(mark'(X1), X2, X3)
mark'(U12'(X1, X2, X3)) → a__U12'(mark'(X1), X2, X3)
mark'(U13'(X1, X2, X3)) → a__U13'(mark'(X1), X2, X3)
mark'(U14'(X1, X2, X3)) → a__U14'(mark'(X1), X2, X3)
mark'(U15'(X1, X2)) → a__U15'(mark'(X1), X2)
mark'(U16'(X)) → a__U16'(mark'(X))
mark'(U21'(X1, X2)) → a__U21'(mark'(X1), X2)
mark'(U22'(X1, X2)) → a__U22'(mark'(X1), X2)
mark'(U23'(X)) → a__U23'(mark'(X))
mark'(U31'(X1, X2, X3)) → a__U31'(mark'(X1), X2, X3)
mark'(U32'(X1, X2, X3)) → a__U32'(mark'(X1), X2, X3)
mark'(U33'(X1, X2, X3)) → a__U33'(mark'(X1), X2, X3)
mark'(U34'(X1, X2, X3)) → a__U34'(mark'(X1), X2, X3)
mark'(U35'(X1, X2)) → a__U35'(mark'(X1), X2)
mark'(U36'(X)) → a__U36'(mark'(X))
mark'(U41'(X1, X2)) → a__U41'(mark'(X1), X2)
mark'(U42'(X)) → a__U42'(mark'(X))
mark'(U51'(X)) → a__U51'(mark'(X))
mark'(U61'(X1, X2)) → a__U61'(mark'(X1), X2)
mark'(U62'(X)) → a__U62'(mark'(X))
mark'(U71'(X1, X2)) → a__U71'(mark'(X1), X2)
mark'(U72'(X1, X2)) → a__U72'(mark'(X1), X2)
mark'(U81'(X1, X2, X3)) → a__U81'(mark'(X1), X2, X3)
mark'(U82'(X1, X2, X3)) → a__U82'(mark'(X1), X2, X3)
mark'(U83'(X1, X2, X3)) → a__U83'(mark'(X1), X2, X3)
mark'(U84'(X1, X2, X3)) → a__U84'(mark'(X1), X2, X3)
mark'(U91'(X1, X2)) → a__U91'(mark'(X1), X2)
mark'(U92'(X)) → a__U92'(mark'(X))
mark'(tt') → tt'
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__U101'(X1, X2, X3) → U101'(X1, X2, X3)
a__U102'(X1, X2, X3) → U102'(X1, X2, X3)
a__isNatKind'(X) → isNatKind'(X)
a__U103'(X1, X2, X3) → U103'(X1, X2, X3)
a__isNat'(X) → isNat'(X)
a__U104'(X1, X2, X3) → U104'(X1, X2, X3)
a__plus'(X1, X2) → plus'(X1, X2)
a__x'(X1, X2) → x'(X1, X2)
a__U11'(X1, X2, X3) → U11'(X1, X2, X3)
a__U12'(X1, X2, X3) → U12'(X1, X2, X3)
a__U13'(X1, X2, X3) → U13'(X1, X2, X3)
a__U14'(X1, X2, X3) → U14'(X1, X2, X3)
a__U15'(X1, X2) → U15'(X1, X2)
a__U16'(X) → U16'(X)
a__U21'(X1, X2) → U21'(X1, X2)
a__U22'(X1, X2) → U22'(X1, X2)
a__U23'(X) → U23'(X)
a__U31'(X1, X2, X3) → U31'(X1, X2, X3)
a__U32'(X1, X2, X3) → U32'(X1, X2, X3)
a__U33'(X1, X2, X3) → U33'(X1, X2, X3)
a__U34'(X1, X2, X3) → U34'(X1, X2, X3)
a__U35'(X1, X2) → U35'(X1, X2)
a__U36'(X) → U36'(X)
a__U41'(X1, X2) → U41'(X1, X2)
a__U42'(X) → U42'(X)
a__U51'(X) → U51'(X)
a__U61'(X1, X2) → U61'(X1, X2)
a__U62'(X) → U62'(X)
a__U71'(X1, X2) → U71'(X1, X2)
a__U72'(X1, X2) → U72'(X1, X2)
a__U81'(X1, X2, X3) → U81'(X1, X2, X3)
a__U82'(X1, X2, X3) → U82'(X1, X2, X3)
a__U83'(X1, X2, X3) → U83'(X1, X2, X3)
a__U84'(X1, X2, X3) → U84'(X1, X2, X3)
a__U91'(X1, X2) → U91'(X1, X2)
a__U92'(X) → U92'(X)

Types:
a__U101' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
tt' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U102' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__isNatKind' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U103' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__isNat' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U104' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__plus' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__x' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
mark' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U11' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U12' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U13' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U14' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U15' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U16' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U21' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U22' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U23' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U31' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U32' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U33' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U34' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U35' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U36' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U41' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U42' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U51' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U61' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U62' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U71' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U72' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U81' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U82' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U83' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U84' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
s' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U91' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
a__U92' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
0' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
plus' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
x' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U101' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U102' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
isNatKind' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U103' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
isNat' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U104' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U11' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U12' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U13' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U14' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U15' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U16' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U21' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U22' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U23' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U31' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U32' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U33' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U34' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U35' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U36' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U41' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U42' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U51' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U61' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U62' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U71' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U72' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U81' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U82' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U83' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U84' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U91' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
U92' :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92' → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
_hole_tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'1 :: tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'
_gen_tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'2 :: Nat → tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'

Heuristically decided to analyse the following defined symbols:
a__U101', a__U102', a__isNatKind', a__U103', a__isNat', a__U104', a__plus', a__x', mark', a__U11', a__U12', a__U13', a__U14', a__U15', a__U21', a__U22', a__U31', a__U32', a__U33', a__U34', a__U35', a__U41', a__U61', a__U71', a__U72', a__U81', a__U82', a__U83', a__U84'

They will be analysed ascendingly in the following order:
a__U101' = a__U102'
a__isNatKind' < a__U101'
a__U101' = a__U103'
a__U101' = a__U104'
a__U101' = a__plus'
a__U101' = a__x'
a__U101' = mark'
a__U101' = a__U71'
a__U101' = a__U72'
a__U101' = a__U81'
a__U101' = a__U82'
a__U101' = a__U83'
a__U101' = a__U84'
a__U102' = a__U103'
a__isNat' < a__U102'
a__U102' = a__U104'
a__U102' = a__plus'
a__U102' = a__x'
a__U102' = mark'
a__U102' = a__U71'
a__U102' = a__U72'
a__U102' = a__U81'
a__U102' = a__U82'
a__U102' = a__U83'
a__U102' = a__U84'
a__isNatKind' < a__U103'
a__isNatKind' < a__isNat'
a__isNatKind' < mark'
a__isNatKind' < a__U11'
a__isNatKind' < a__U12'
a__isNatKind' < a__U13'
a__isNatKind' < a__U21'
a__isNatKind' < a__U31'
a__isNatKind' < a__U32'
a__isNatKind' < a__U33'
a__isNatKind' = a__U41'
a__isNatKind' = a__U61'
a__isNatKind' < a__U71'
a__isNatKind' < a__U81'
a__isNatKind' < a__U83'
a__U103' = a__U104'
a__U103' = a__plus'
a__U103' = a__x'
a__U103' = mark'
a__U103' = a__U71'
a__U103' = a__U72'
a__U103' = a__U81'
a__U103' = a__U82'
a__U103' = a__U83'
a__U103' = a__U84'
a__isNat' < a__plus'
a__isNat' < a__x'
a__isNat' < mark'
a__isNat' = a__U11'
a__isNat' = a__U12'
a__isNat' = a__U13'
a__isNat' = a__U14'
a__isNat' = a__U15'
a__isNat' = a__U21'
a__isNat' = a__U22'
a__isNat' = a__U31'
a__isNat' = a__U32'
a__isNat' = a__U33'
a__isNat' = a__U34'
a__isNat' = a__U35'
a__isNat' < a__U82'
a__U104' = a__plus'
a__U104' = a__x'
a__U104' = mark'
a__U104' = a__U71'
a__U104' = a__U72'
a__U104' = a__U81'
a__U104' = a__U82'
a__U104' = a__U83'
a__U104' = a__U84'
a__plus' = a__x'
a__plus' = mark'
a__plus' = a__U71'
a__plus' = a__U72'
a__plus' = a__U81'
a__plus' = a__U82'
a__plus' = a__U83'
a__plus' = a__U84'
a__x' = mark'
a__x' = a__U71'
a__x' = a__U72'
a__x' = a__U81'
a__x' = a__U82'
a__x' = a__U83'
a__x' = a__U84'
a__U11' < mark'
a__U12' < mark'
a__U13' < mark'
a__U14' < mark'
a__U15' < mark'
a__U21' < mark'
a__U22' < mark'
a__U31' < mark'
a__U32' < mark'
a__U33' < mark'
a__U34' < mark'
a__U35' < mark'
a__U41' < mark'
a__U61' < mark'
mark' = a__U71'
mark' = a__U72'
mark' = a__U81'
mark' = a__U82'
mark' = a__U83'
mark' = a__U84'
a__U11' = a__U12'
a__U11' = a__U13'
a__U11' = a__U14'
a__U11' = a__U15'
a__U11' = a__U21'
a__U11' = a__U22'
a__U11' = a__U31'
a__U11' = a__U32'
a__U11' = a__U33'
a__U11' = a__U34'
a__U11' = a__U35'
a__U12' = a__U13'
a__U12' = a__U14'
a__U12' = a__U15'
a__U12' = a__U21'
a__U12' = a__U22'
a__U12' = a__U31'
a__U12' = a__U32'
a__U12' = a__U33'
a__U12' = a__U34'
a__U12' = a__U35'
a__U13' = a__U14'
a__U13' = a__U15'
a__U13' = a__U21'
a__U13' = a__U22'
a__U13' = a__U31'
a__U13' = a__U32'
a__U13' = a__U33'
a__U13' = a__U34'
a__U13' = a__U35'
a__U14' = a__U15'
a__U14' = a__U21'
a__U14' = a__U22'
a__U14' = a__U31'
a__U14' = a__U32'
a__U14' = a__U33'
a__U14' = a__U34'
a__U14' = a__U35'
a__U15' = a__U21'
a__U15' = a__U22'
a__U15' = a__U31'
a__U15' = a__U32'
a__U15' = a__U33'
a__U15' = a__U34'
a__U15' = a__U35'
a__U21' = a__U22'
a__U21' = a__U31'
a__U21' = a__U32'
a__U21' = a__U33'
a__U21' = a__U34'
a__U21' = a__U35'
a__U22' = a__U31'
a__U22' = a__U32'
a__U22' = a__U33'
a__U22' = a__U34'
a__U22' = a__U35'
a__U31' = a__U32'
a__U31' = a__U33'
a__U31' = a__U34'
a__U31' = a__U35'
a__U32' = a__U33'
a__U32' = a__U34'
a__U32' = a__U35'
a__U33' = a__U34'
a__U33' = a__U35'
a__U34' = a__U35'
a__U41' = a__U61'
a__U71' = a__U72'
a__U71' = a__U81'
a__U71' = a__U82'
a__U71' = a__U83'
a__U71' = a__U84'
a__U72' = a__U81'
a__U72' = a__U82'
a__U72' = a__U83'
a__U72' = a__U84'
a__U81' = a__U82'
a__U81' = a__U83'
a__U81' = a__U84'
a__U82' = a__U83'
a__U82' = a__U84'
a__U83' = a__U84'

Generator Equations:
_gen_tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'2(0) ⇔ tt'
_gen_tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'2(+(x, 1)) ⇔ s'(_gen_tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'2(x))

The following defined symbols remain to be analysed:
a__U41', a__U101', a__U102', a__isNatKind', a__U103', a__isNat', a__U104', a__plus', a__x', mark', a__U11', a__U12', a__U13', a__U14', a__U15', a__U21', a__U22', a__U31', a__U32', a__U33', a__U34', a__U35', a__U61', a__U71', a__U72', a__U81', a__U82', a__U83', a__U84'

Could not prove a rewrite lemma for the defined symbol a__U41'.

The following defined symbols remain to be analysed:
a__isNatKind', a__U101', a__U102', a__U103', a__isNat', a__U104', a__plus', a__x', mark', a__U11', a__U12', a__U13', a__U14', a__U15', a__U21', a__U22', a__U31', a__U32', a__U33', a__U34', a__U35', a__U61', a__U71', a__U72', a__U81', a__U82', a__U83', a__U84'

Proved the following rewrite lemma:
a__isNatKind'(_gen_tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'2(+(1, _n5316))) → _*3, rt ∈ Ω(_n5316)

Induction Base:
a__isNatKind'(_gen_tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'2(+(1, 0)))

Induction Step:
a__isNatKind'(_gen_tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'2(+(1, +(_$n5317, 1)))) →_R^Ω(1)
a__U51'(a__isNatKind'(_gen_tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'2(+(1, _$n5317)))) →_IH
a__U51'(_*3)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Lemmas:
a__isNatKind'(_gen_tt':s':0':plus':x':U101':U102':isNatKind':U103':isNat':U104':U11':U12':U13':U14':U15':U16':U21':U22':U23':U31':U32':U33':U34':U35':U36':U41':U42':U51':U61':U62':U71':U72':U81':U82':U83':U84':U91':U92'2(+(1, _n5316))) → _*3, rt ∈ Ω(_n5316)

The following defined symbols remain to be analysed:
a__U61', a__U101', a__U102', a__U103', a__isNat', a__U104', a__plus', a__x', mark', a__U11', a__U12', a__U13', a__U14', a__U15', a__U21', a__U22', a__U31', a__U32', a__U33', a__U34', a__U35', a__U41', a__U71', a__U72', a__U81', a__U82', a__U83', a__U84'

Could not prove a rewrite lemma for the defined symbol a__U61'.

The following defined symbols remain to be analysed:
a__U41', a__U101', a__U102', a__U103', a__isNat', a__U104', a__plus', a__x', mark', a__U11', a__U12', a__U13', a__U14', a__U15', a__U21', a__U22', a__U31', a__U32', a__U33', a__U34', a__U35', a__U71', a__U72', a__U81', a__U82', a__U83', a__U84'

Could not prove a rewrite lemma for the defined symbol a__U41'.

The following defined symbols remain to be analysed:
a__U11', a__U101', a__U102', a__U103', a__isNat', a__U104', a__plus', a__x', mark', a__U12', a__U13', a__U14', a__U15', a__U21', a__U22', a__U31', a__U32', a__U33', a__U34', a__U35', a__U71', a__U72', a__U81', a__U82', a__U83', a__U84'

They will be analysed ascendingly in the following order:
a__U101' = a__U102'
a__U101' = a__U103'
a__U101' = a__U104'
a__U101' = a__plus'
a__U101' = a__x'
a__U101' = mark'
a__U101' = a__U71'
a__U101' = a__U72'
a__U101' = a__U81'
a__U101' = a__U82'
a__U101' = a__U83'
a__U101' = a__U84'
a__U102' = a__U103'
a__isNat' < a__U102'
a__U102' = a__U104'
a__U102' = a__plus'
a__U102' = a__x'
a__U102' = mark'
a__U102' = a__U71'
a__U102' = a__U72'
a__U102' = a__U81'
a__U102' = a__U82'
a__U102' = a__U83'
a__U102' = a__U84'
a__U103' = a__U104'
a__U103' = a__plus'
a__U103' = a__x'
a__U103' = mark'
a__U103' = a__U71'
a__U103' = a__U72'
a__U103' = a__U81'
a__U103' = a__U82'
a__U103' = a__U83'
a__U103' = a__U84'
a__isNat' < a__plus'
a__isNat' < a__x'
a__isNat' < mark'
a__isNat' = a__U11'
a__isNat' = a__U12'
a__isNat' = a__U13'
a__isNat' = a__U14'
a__isNat' = a__U15'
a__isNat' = a__U21'
a__isNat' = a__U22'
a__isNat' = a__U31'
a__isNat' = a__U32'
a__isNat' = a__U33'
a__isNat' = a__U34'
a__isNat' = a__U35'
a__isNat' < a__U82'
a__U104' = a__plus'
a__U104' = a__x'
a__U104' = mark'
a__U104' = a__U71'
a__U104' = a__U72'
a__U104' = a__U81'
a__U104' = a__U82'
a__U104' = a__U83'
a__U104' = a__U84'
a__plus' = a__x'
a__plus' = mark'
a__plus' = a__U71'
a__plus' = a__U72'
a__plus' = a__U81'
a__plus' = a__U82'
a__plus' = a__U83'
a__plus' = a__U84'
a__x' = mark'
a__x' = a__U71'
a__x' = a__U72'
a__x' = a__U81'
a__x' = a__U82'
a__x' = a__U83'
a__x' = a__U84'
a__U11' < mark'
a__U12' < mark'
a__U13' < mark'
a__U14' < mark'
a__U15' < mark'
a__U21' < mark'
a__U22' < mark'
a__U31' < mark'
a__U32' < mark'
a__U33' < mark'
a__U34' < mark'
a__U35' < mark'
mark' = a__U71'
mark' = a__U72'
mark' = a__U81'
mark' = a__U82'
mark' = a__U83'
mark' = a__U84'
a__U11' = a__U12'
a__U11' = a__U13'
a__U11' = a__U14'
a__U11' = a__U15'
a__U11' = a__U21'
a__U11' = a__U22'
a__U11' = a__U31'
a__U11' = a__U32'
a__U11' = a__U33'
a__U11' = a__U34'
a__U11' = a__U35'
a__U12' = a__U13'
a__U12' = a__U14'
a__U12' = a__U15'
a__U12' = a__U21'
a__U12' = a__U22'
a__U12' = a__U31'
a__U12' = a__U32'
a__U12' = a__U33'
a__U12' = a__U34'
a__U12' = a__U35'
a__U13' = a__U14'
a__U13' = a__U15'
a__U13' = a__U21'
a__U13' = a__U22'
a__U13' = a__U31'
a__U13' = a__U32'
a__U13' = a__U33'
a__U13' = a__U34'
a__U13' = a__U35'
a__U14' = a__U15'
a__U14' = a__U21'
a__U14' = a__U22'
a__U14' = a__U31'
a__U14' = a__U32'
a__U14' = a__U33'
a__U14' = a__U34'
a__U14' = a__U35'
a__U15' = a__U21'
a__U15' = a__U22'
a__U15' = a__U31'
a__U15' = a__U32'
a__U15' = a__U33'
a__U15' = a__U34'
a__U15' = a__U35'
a__U21' = a__U22'
a__U21' = a__U31'
a__U21' = a__U32'
a__U21' = a__U33'
a__U21' = a__U34'
a__U21' = a__U35'
a__U22' = a__U31'
a__U22' = a__U32'
a__U22' = a__U33'
a__U22' = a__U34'
a__U22' = a__U35'
a__U31' = a__U32'
a__U31' = a__U33'
a__U31' = a__U34'
a__U31' = a__U35'
a__U32' = a__U33'
a__U32' = a__U34'
a__U32' = a__U35'
a__U33' = a__U34'
a__U33' = a__U35'
a__U34' = a__U35'
a__U71' = a__U72'
a__U71' = a__U81'
a__U71' = a__U82'
a__U71' = a__U83'
a__U71' = a__U84'
a__U72' = a__U81'
a__U72' = a__U82'
a__U72' = a__U83'
a__U72' = a__U84'
a__U81' = a__U82'
a__U81' = a__U83'
a__U81' = a__U84'
a__U82' = a__U83'
a__U82' = a__U84'
a__U83' = a__U84'

Could not prove a rewrite lemma for the defined symbol a__U11'.

The following defined symbols remain to be analysed:
a__U12', a__U101', a__U102', a__U103', a__isNat', a__U104', a__plus', a__x', mark', a__U13', a__U14', a__U15', a__U21', a__U22', a__U31', a__U32', a__U33', a__U34', a__U35', a__U71', a__U72', a__U81', a__U82', a__U83', a__U84'

Could not prove a rewrite lemma for the defined symbol a__U12'.

The following defined symbols remain to be analysed:
a__U13', a__U101', a__U102', a__U103', a__isNat', a__U104', a__plus', a__x', mark', a__U14', a__U15', a__U21', a__U22', a__U31', a__U32', a__U33', a__U34', a__U35', a__U71', a__U72', a__U81', a__U82', a__U83', a__U84'

Could not prove a rewrite lemma for the defined symbol a__U13'.

The following defined symbols remain to be analysed:
a__U14', a__U101', a__U102', a__U103', a__isNat', a__U104', a__plus', a__x', mark', a__U15', a__U21', a__U22', a__U31', a__U32', a__U33', a__U34', a__U35', a__U71', a__U72', a__U81', a__U82', a__U83', a__U84'

Could not prove a rewrite lemma for the defined symbol a__U14'.