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

a__U11(tt, V1, V2) → a__U12(a__isNat(V1), V2)
a__U12(tt, V2) → a__U13(a__isNat(V2))
a__U13(tt) → tt
a__U21(tt, V1) → a__U22(a__isNat(V1))
a__U22(tt) → tt
a__U31(tt, V1, V2) → a__U32(a__isNat(V1), V2)
a__U32(tt, V2) → a__U33(a__isNat(V2))
a__U33(tt) → tt
a__U41(tt, N) → mark(N)
a__U51(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__U61(tt) → 0
a__U71(tt, M, N) → a__plus(a__x(mark(N), mark(M)), mark(N))
a__and(tt, X) → mark(X)
a__isNat(0) → tt
a__isNat(plus(V1, V2)) → a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)
a__isNat(x(V1, V2)) → a__U31(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__and(a__isNatKind(V1), isNatKind(V2))
a__isNatKind(s(V1)) → a__isNatKind(V1)
a__isNatKind(x(V1, V2)) → a__and(a__isNatKind(V1), isNatKind(V2))
a__plus(N, 0) → a__U41(a__and(a__isNat(N), isNatKind(N)), N)
a__plus(N, s(M)) → a__U51(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
a__x(N, 0) → a__U61(a__and(a__isNat(N), isNatKind(N)))
a__x(N, s(M)) → a__U71(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)
mark(U13(X)) → a__U13(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(U31(X1, X2, X3)) → a__U31(mark(X1), X2, X3)
mark(U32(X1, X2)) → a__U32(mark(X1), X2)
mark(U33(X)) → a__U33(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U51(X1, X2, X3)) → a__U51(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2, X3)) → a__U71(mark(X1), X2, X3)
mark(x(X1, X2)) → a__x(mark(X1), mark(X2))
mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isNatKind(X)) → a__isNatKind(X)
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)
a__U12(X1, X2) → U12(X1, X2)
a__isNat(X) → isNat(X)
a__U13(X) → U13(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__U31(X1, X2, X3) → U31(X1, X2, X3)
a__U32(X1, X2) → U32(X1, X2)
a__U33(X) → U33(X)
a__U41(X1, X2) → U41(X1, X2)
a__U51(X1, X2, X3) → U51(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)
a__U61(X) → U61(X)
a__U71(X1, X2, X3) → U71(X1, X2, X3)
a__x(X1, X2) → x(X1, X2)
a__and(X1, X2) → and(X1, X2)
a__isNatKind(X) → isNatKind(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__U11'(tt', V1, V2) → a__U12'(a__isNat'(V1), V2)
a__U12'(tt', V2) → a__U13'(a__isNat'(V2))
a__U13'(tt') → tt'
a__U21'(tt', V1) → a__U22'(a__isNat'(V1))
a__U22'(tt') → tt'
a__U31'(tt', V1, V2) → a__U32'(a__isNat'(V1), V2)
a__U32'(tt', V2) → a__U33'(a__isNat'(V2))
a__U33'(tt') → tt'
a__U41'(tt', N) → mark'(N)
a__U51'(tt', M, N) → s'(a__plus'(mark'(N), mark'(M)))
a__U61'(tt') → 0'
a__U71'(tt', M, N) → a__plus'(a__x'(mark'(N), mark'(M)), mark'(N))
a__and'(tt', X) → mark'(X)
a__isNat'(0') → tt'
a__isNat'(plus'(V1, V2)) → a__U11'(a__and'(a__isNatKind'(V1), isNatKind'(V2)), V1, V2)
a__isNat'(s'(V1)) → a__U21'(a__isNatKind'(V1), V1)
a__isNat'(x'(V1, V2)) → a__U31'(a__and'(a__isNatKind'(V1), isNatKind'(V2)), V1, V2)
a__isNatKind'(0') → tt'
a__isNatKind'(plus'(V1, V2)) → a__and'(a__isNatKind'(V1), isNatKind'(V2))
a__isNatKind'(s'(V1)) → a__isNatKind'(V1)
a__isNatKind'(x'(V1, V2)) → a__and'(a__isNatKind'(V1), isNatKind'(V2))
a__plus'(N, 0') → a__U41'(a__and'(a__isNat'(N), isNatKind'(N)), N)
a__plus'(N, s'(M)) → a__U51'(a__and'(a__and'(a__isNat'(M), isNatKind'(M)), and'(isNat'(N), isNatKind'(N))), M, N)
a__x'(N, 0') → a__U61'(a__and'(a__isNat'(N), isNatKind'(N)))
a__x'(N, s'(M)) → a__U71'(a__and'(a__and'(a__isNat'(M), isNatKind'(M)), and'(isNat'(N), isNatKind'(N))), M, N)
mark'(U11'(X1, X2, X3)) → a__U11'(mark'(X1), X2, X3)
mark'(U12'(X1, X2)) → a__U12'(mark'(X1), X2)
mark'(isNat'(X)) → a__isNat'(X)
mark'(U13'(X)) → a__U13'(mark'(X))
mark'(U21'(X1, X2)) → a__U21'(mark'(X1), X2)
mark'(U22'(X)) → a__U22'(mark'(X))
mark'(U31'(X1, X2, X3)) → a__U31'(mark'(X1), X2, X3)
mark'(U32'(X1, X2)) → a__U32'(mark'(X1), X2)
mark'(U33'(X)) → a__U33'(mark'(X))
mark'(U41'(X1, X2)) → a__U41'(mark'(X1), X2)
mark'(U51'(X1, X2, X3)) → a__U51'(mark'(X1), X2, X3)
mark'(plus'(X1, X2)) → a__plus'(mark'(X1), mark'(X2))
mark'(U61'(X)) → a__U61'(mark'(X))
mark'(U71'(X1, X2, X3)) → a__U71'(mark'(X1), X2, X3)
mark'(x'(X1, X2)) → a__x'(mark'(X1), mark'(X2))
mark'(and'(X1, X2)) → a__and'(mark'(X1), X2)
mark'(isNatKind'(X)) → a__isNatKind'(X)
mark'(tt') → tt'
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__U11'(X1, X2, X3) → U11'(X1, X2, X3)
a__U12'(X1, X2) → U12'(X1, X2)
a__isNat'(X) → isNat'(X)
a__U13'(X) → U13'(X)
a__U21'(X1, X2) → U21'(X1, X2)
a__U22'(X) → U22'(X)
a__U31'(X1, X2, X3) → U31'(X1, X2, X3)
a__U32'(X1, X2) → U32'(X1, X2)
a__U33'(X) → U33'(X)
a__U41'(X1, X2) → U41'(X1, X2)
a__U51'(X1, X2, X3) → U51'(X1, X2, X3)
a__plus'(X1, X2) → plus'(X1, X2)
a__U61'(X) → U61'(X)
a__U71'(X1, X2, X3) → U71'(X1, X2, X3)
a__x'(X1, X2) → x'(X1, X2)
a__and'(X1, X2) → and'(X1, X2)
a__isNatKind'(X) → isNatKind'(X)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
a__U11'(tt', V1, V2) → a__U12'(a__isNat'(V1), V2)
a__U12'(tt', V2) → a__U13'(a__isNat'(V2))
a__U13'(tt') → tt'
a__U21'(tt', V1) → a__U22'(a__isNat'(V1))
a__U22'(tt') → tt'
a__U31'(tt', V1, V2) → a__U32'(a__isNat'(V1), V2)
a__U32'(tt', V2) → a__U33'(a__isNat'(V2))
a__U33'(tt') → tt'
a__U41'(tt', N) → mark'(N)
a__U51'(tt', M, N) → s'(a__plus'(mark'(N), mark'(M)))
a__U61'(tt') → 0'
a__U71'(tt', M, N) → a__plus'(a__x'(mark'(N), mark'(M)), mark'(N))
a__and'(tt', X) → mark'(X)
a__isNat'(0') → tt'
a__isNat'(plus'(V1, V2)) → a__U11'(a__and'(a__isNatKind'(V1), isNatKind'(V2)), V1, V2)
a__isNat'(s'(V1)) → a__U21'(a__isNatKind'(V1), V1)
a__isNat'(x'(V1, V2)) → a__U31'(a__and'(a__isNatKind'(V1), isNatKind'(V2)), V1, V2)
a__isNatKind'(0') → tt'
a__isNatKind'(plus'(V1, V2)) → a__and'(a__isNatKind'(V1), isNatKind'(V2))
a__isNatKind'(s'(V1)) → a__isNatKind'(V1)
a__isNatKind'(x'(V1, V2)) → a__and'(a__isNatKind'(V1), isNatKind'(V2))
a__plus'(N, 0') → a__U41'(a__and'(a__isNat'(N), isNatKind'(N)), N)
a__plus'(N, s'(M)) → a__U51'(a__and'(a__and'(a__isNat'(M), isNatKind'(M)), and'(isNat'(N), isNatKind'(N))), M, N)
a__x'(N, 0') → a__U61'(a__and'(a__isNat'(N), isNatKind'(N)))
a__x'(N, s'(M)) → a__U71'(a__and'(a__and'(a__isNat'(M), isNatKind'(M)), and'(isNat'(N), isNatKind'(N))), M, N)
mark'(U11'(X1, X2, X3)) → a__U11'(mark'(X1), X2, X3)
mark'(U12'(X1, X2)) → a__U12'(mark'(X1), X2)
mark'(isNat'(X)) → a__isNat'(X)
mark'(U13'(X)) → a__U13'(mark'(X))
mark'(U21'(X1, X2)) → a__U21'(mark'(X1), X2)
mark'(U22'(X)) → a__U22'(mark'(X))
mark'(U31'(X1, X2, X3)) → a__U31'(mark'(X1), X2, X3)
mark'(U32'(X1, X2)) → a__U32'(mark'(X1), X2)
mark'(U33'(X)) → a__U33'(mark'(X))
mark'(U41'(X1, X2)) → a__U41'(mark'(X1), X2)
mark'(U51'(X1, X2, X3)) → a__U51'(mark'(X1), X2, X3)
mark'(plus'(X1, X2)) → a__plus'(mark'(X1), mark'(X2))
mark'(U61'(X)) → a__U61'(mark'(X))
mark'(U71'(X1, X2, X3)) → a__U71'(mark'(X1), X2, X3)
mark'(x'(X1, X2)) → a__x'(mark'(X1), mark'(X2))
mark'(and'(X1, X2)) → a__and'(mark'(X1), X2)
mark'(isNatKind'(X)) → a__isNatKind'(X)
mark'(tt') → tt'
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__U11'(X1, X2, X3) → U11'(X1, X2, X3)
a__U12'(X1, X2) → U12'(X1, X2)
a__isNat'(X) → isNat'(X)
a__U13'(X) → U13'(X)
a__U21'(X1, X2) → U21'(X1, X2)
a__U22'(X) → U22'(X)
a__U31'(X1, X2, X3) → U31'(X1, X2, X3)
a__U32'(X1, X2) → U32'(X1, X2)
a__U33'(X) → U33'(X)
a__U41'(X1, X2) → U41'(X1, X2)
a__U51'(X1, X2, X3) → U51'(X1, X2, X3)
a__plus'(X1, X2) → plus'(X1, X2)
a__U61'(X) → U61'(X)
a__U71'(X1, X2, X3) → U71'(X1, X2, X3)
a__x'(X1, X2) → x'(X1, X2)
a__and'(X1, X2) → and'(X1, X2)
a__isNatKind'(X) → isNatKind'(X)

Types:
a__U11' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
tt' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
a__U12' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
a__isNat' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
a__U13' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
a__U21' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
a__U22' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
a__U31' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
a__U32' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
a__U33' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
a__U41' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
mark' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
a__U51' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
s' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
a__plus' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
a__U61' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
0' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
a__U71' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
a__x' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
a__and' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
plus' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
a__isNatKind' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
isNatKind' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
x' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
and' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
isNat' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
U11' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
U12' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
U13' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
U21' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
U22' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
U31' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
U32' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
U33' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
U41' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
U51' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
U61' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
U71' :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71' → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
_hole_tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'1 :: tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'
_gen_tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'2 :: Nat → tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'

Heuristically decided to analyse the following defined symbols:
a__U11', a__U12', a__isNat', a__U21', a__U31', a__U32', a__U41', mark', a__U51', a__plus', a__U71', a__x', a__and', a__isNatKind'

They will be analysed ascendingly in the following order:
a__U11' = a__U12'
a__U11' = a__isNat'
a__U11' = a__U21'
a__U11' = a__U31'
a__U11' = a__U32'
a__U11' = a__U41'
a__U11' = mark'
a__U11' = a__U51'
a__U11' = a__plus'
a__U11' = a__U71'
a__U11' = a__x'
a__U11' = a__and'
a__U11' = a__isNatKind'
a__U12' = a__isNat'
a__U12' = a__U21'
a__U12' = a__U31'
a__U12' = a__U32'
a__U12' = a__U41'
a__U12' = mark'
a__U12' = a__U51'
a__U12' = a__plus'
a__U12' = a__U71'
a__U12' = a__x'
a__U12' = a__and'
a__U12' = a__isNatKind'
a__isNat' = a__U21'
a__isNat' = a__U31'
a__isNat' = a__U32'
a__isNat' = a__U41'
a__isNat' = mark'
a__isNat' = a__U51'
a__isNat' = a__plus'
a__isNat' = a__U71'
a__isNat' = a__x'
a__isNat' = a__and'
a__isNat' = a__isNatKind'
a__U21' = a__U31'
a__U21' = a__U32'
a__U21' = a__U41'
a__U21' = mark'
a__U21' = a__U51'
a__U21' = a__plus'
a__U21' = a__U71'
a__U21' = a__x'
a__U21' = a__and'
a__U21' = a__isNatKind'
a__U31' = a__U32'
a__U31' = a__U41'
a__U31' = mark'
a__U31' = a__U51'
a__U31' = a__plus'
a__U31' = a__U71'
a__U31' = a__x'
a__U31' = a__and'
a__U31' = a__isNatKind'
a__U32' = a__U41'
a__U32' = mark'
a__U32' = a__U51'
a__U32' = a__plus'
a__U32' = a__U71'
a__U32' = a__x'
a__U32' = a__and'
a__U32' = a__isNatKind'
a__U41' = mark'
a__U41' = a__U51'
a__U41' = a__plus'
a__U41' = a__U71'
a__U41' = a__x'
a__U41' = a__and'
a__U41' = a__isNatKind'
mark' = a__U51'
mark' = a__plus'
mark' = a__U71'
mark' = a__x'
mark' = a__and'
mark' = a__isNatKind'
a__U51' = a__plus'
a__U51' = a__U71'
a__U51' = a__x'
a__U51' = a__and'
a__U51' = a__isNatKind'
a__plus' = a__U71'
a__plus' = a__x'
a__plus' = a__and'
a__plus' = a__isNatKind'
a__U71' = a__x'
a__U71' = a__and'
a__U71' = a__isNatKind'
a__x' = a__and'
a__x' = a__isNatKind'
a__and' = a__isNatKind'

Generator Equations:
_gen_tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'2(0) ⇔ tt'
_gen_tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'2(+(x, 1)) ⇔ s'(_gen_tt':s':0':plus':isNatKind':x':isNat':and':U11':U12':U13':U21':U22':U31':U32':U33':U41':U51':U61':U71'2(x))

The following defined symbols remain to be analysed:
a__U12', a__U11', a__isNat', a__U21', a__U31', a__U32', a__U41', mark', a__U51', a__plus', a__U71', a__x', a__and', a__isNatKind'

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

The following defined symbols remain to be analysed:
a__isNat', a__U11', a__U21', a__U31', a__U32', a__U41', mark', a__U51', a__plus', a__U71', a__x', a__and', a__isNatKind'

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

The following defined symbols remain to be analysed:
a__U11', a__U21', a__U31', a__U32', a__U41', mark', a__U51', a__plus', a__U71', a__x', a__and', a__isNatKind'

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

The following defined symbols remain to be analysed:
a__and', a__U21', a__U31', a__U32', a__U41', mark', a__U51', a__plus', a__U71', a__x', a__isNatKind'