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

a__U11(tt, N) → mark(N)
a__U21(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__and(tt, X) → mark(X)
a__isNat(0) → tt
a__isNat(plus(V1, V2)) → a__and(a__isNat(V1), isNat(V2))
a__isNat(s(V1)) → a__isNat(V1)
a__plus(N, 0) → a__U11(a__isNat(N), N)
a__plus(N, s(M)) → a__U21(a__and(a__isNat(M), isNat(N)), M, N)
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U21(X1, X2, X3)) → a__U21(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))
mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(0) → 0
a__U11(X1, X2) → U11(X1, X2)
a__U21(X1, X2, X3) → U21(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)
a__and(X1, X2) → and(X1, X2)
a__isNat(X) → isNat(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', N) → mark'(N)
a__U21'(tt', M, N) → s'(a__plus'(mark'(N), mark'(M)))
a__and'(tt', X) → mark'(X)
a__isNat'(0') → tt'
a__isNat'(plus'(V1, V2)) → a__and'(a__isNat'(V1), isNat'(V2))
a__isNat'(s'(V1)) → a__isNat'(V1)
a__plus'(N, 0') → a__U11'(a__isNat'(N), N)
a__plus'(N, s'(M)) → a__U21'(a__and'(a__isNat'(M), isNat'(N)), M, N)
mark'(U11'(X1, X2)) → a__U11'(mark'(X1), X2)
mark'(U21'(X1, X2, X3)) → a__U21'(mark'(X1), X2, X3)
mark'(plus'(X1, X2)) → a__plus'(mark'(X1), mark'(X2))
mark'(and'(X1, X2)) → a__and'(mark'(X1), X2)
mark'(isNat'(X)) → a__isNat'(X)
mark'(tt') → tt'
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__U11'(X1, X2) → U11'(X1, X2)
a__U21'(X1, X2, X3) → U21'(X1, X2, X3)
a__plus'(X1, X2) → plus'(X1, X2)
a__and'(X1, X2) → and'(X1, X2)
a__isNat'(X) → isNat'(X)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
a__U11'(tt', N) → mark'(N)
a__U21'(tt', M, N) → s'(a__plus'(mark'(N), mark'(M)))
a__and'(tt', X) → mark'(X)
a__isNat'(0') → tt'
a__isNat'(plus'(V1, V2)) → a__and'(a__isNat'(V1), isNat'(V2))
a__isNat'(s'(V1)) → a__isNat'(V1)
a__plus'(N, 0') → a__U11'(a__isNat'(N), N)
a__plus'(N, s'(M)) → a__U21'(a__and'(a__isNat'(M), isNat'(N)), M, N)
mark'(U11'(X1, X2)) → a__U11'(mark'(X1), X2)
mark'(U21'(X1, X2, X3)) → a__U21'(mark'(X1), X2, X3)
mark'(plus'(X1, X2)) → a__plus'(mark'(X1), mark'(X2))
mark'(and'(X1, X2)) → a__and'(mark'(X1), X2)
mark'(isNat'(X)) → a__isNat'(X)
mark'(tt') → tt'
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__U11'(X1, X2) → U11'(X1, X2)
a__U21'(X1, X2, X3) → U21'(X1, X2, X3)
a__plus'(X1, X2) → plus'(X1, X2)
a__and'(X1, X2) → and'(X1, X2)
a__isNat'(X) → isNat'(X)

Types:
a__U11' :: tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and'
tt' :: tt':s':0':plus':isNat':U11':U21':and'
mark' :: tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and'
a__U21' :: tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and'
s' :: tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and'
a__plus' :: tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and'
a__and' :: tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and'
a__isNat' :: tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and'
0' :: tt':s':0':plus':isNat':U11':U21':and'
plus' :: tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and'
isNat' :: tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and'
U11' :: tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and'
U21' :: tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and'
and' :: tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and' → tt':s':0':plus':isNat':U11':U21':and'
_hole_tt':s':0':plus':isNat':U11':U21':and'1 :: tt':s':0':plus':isNat':U11':U21':and'
_gen_tt':s':0':plus':isNat':U11':U21':and'2 :: Nat → tt':s':0':plus':isNat':U11':U21':and'

Heuristically decided to analyse the following defined symbols:
a__U11', mark', a__U21', a__plus', a__and', a__isNat'

They will be analysed ascendingly in the following order:
a__U11' = mark'
a__U11' = a__U21'
a__U11' = a__plus'
a__U11' = a__and'
a__U11' = a__isNat'
mark' = a__U21'
mark' = a__plus'
mark' = a__and'
mark' = a__isNat'
a__U21' = a__plus'
a__U21' = a__and'
a__U21' = a__isNat'
a__plus' = a__and'
a__plus' = a__isNat'
a__and' = a__isNat'

Generator Equations:
_gen_tt':s':0':plus':isNat':U11':U21':and'2(0) ⇔ tt'
_gen_tt':s':0':plus':isNat':U11':U21':and'2(+(x, 1)) ⇔ s'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(x))

The following defined symbols remain to be analysed:
mark', a__U11', a__U21', a__plus', a__and', a__isNat'

Proved the following rewrite lemma:
mark'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(_n4)) → _gen_tt':s':0':plus':isNat':U11':U21':and'2(_n4), rt ∈ Ω(1 + _n4)

Induction Base:
mark'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(0)) →_R^Ω(1)
tt'

Induction Step:
mark'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(+(_$n5, 1))) →_R^Ω(1)
s'(mark'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(_$n5))) →_IH
s'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(_$n5))

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

Lemmas:
mark'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(_n4)) → _gen_tt':s':0':plus':isNat':U11':U21':and'2(_n4), rt ∈ Ω(1 + _n4)

Generator Equations:
_gen_tt':s':0':plus':isNat':U11':U21':and'2(0) ⇔ tt'
_gen_tt':s':0':plus':isNat':U11':U21':and'2(+(x, 1)) ⇔ s'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(x))

The following defined symbols remain to be analysed:
a__U11', a__U21', a__plus', a__and', a__isNat'

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

Lemmas:
mark'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(_n4)) → _gen_tt':s':0':plus':isNat':U11':U21':and'2(_n4), rt ∈ Ω(1 + _n4)

Generator Equations:
_gen_tt':s':0':plus':isNat':U11':U21':and'2(0) ⇔ tt'
_gen_tt':s':0':plus':isNat':U11':U21':and'2(+(x, 1)) ⇔ s'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(x))

The following defined symbols remain to be analysed:
a__U21', a__plus', a__and', a__isNat'

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

Lemmas:
mark'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(_n4)) → _gen_tt':s':0':plus':isNat':U11':U21':and'2(_n4), rt ∈ Ω(1 + _n4)

Generator Equations:
_gen_tt':s':0':plus':isNat':U11':U21':and'2(0) ⇔ tt'
_gen_tt':s':0':plus':isNat':U11':U21':and'2(+(x, 1)) ⇔ s'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(x))

The following defined symbols remain to be analysed:
a__plus', a__and', a__isNat'

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

Lemmas:
mark'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(_n4)) → _gen_tt':s':0':plus':isNat':U11':U21':and'2(_n4), rt ∈ Ω(1 + _n4)

Generator Equations:
_gen_tt':s':0':plus':isNat':U11':U21':and'2(0) ⇔ tt'
_gen_tt':s':0':plus':isNat':U11':U21':and'2(+(x, 1)) ⇔ s'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(x))

The following defined symbols remain to be analysed:
a__isNat', a__and'

Proved the following rewrite lemma:
a__isNat'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(+(1, _n5599))) → _*3, rt ∈ Ω(_n5599)

Induction Base:
a__isNat'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(+(1, 0)))

Induction Step:
a__isNat'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(+(1, +(_$n5600, 1)))) →_R^Ω(1)
a__isNat'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(+(1, _$n5600))) →_IH
_*3

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

Lemmas:
mark'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(_n4)) → _gen_tt':s':0':plus':isNat':U11':U21':and'2(_n4), rt ∈ Ω(1 + _n4)
a__isNat'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(+(1, _n5599))) → _*3, rt ∈ Ω(_n5599)

Generator Equations:
_gen_tt':s':0':plus':isNat':U11':U21':and'2(0) ⇔ tt'
_gen_tt':s':0':plus':isNat':U11':U21':and'2(+(x, 1)) ⇔ s'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(x))

The following defined symbols remain to be analysed:
a__and', a__U11', mark', a__U21', a__plus'

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

Generator Equations:
_gen_tt':s':0':plus':isNat':U11':U21':and'2(0) ⇔ tt'
_gen_tt':s':0':plus':isNat':U11':U21':and'2(+(x, 1)) ⇔ s'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(x))

The following defined symbols remain to be analysed:
mark', a__U11', a__U21', a__plus'

Proved the following rewrite lemma:
mark'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(_n7862)) → _gen_tt':s':0':plus':isNat':U11':U21':and'2(_n7862), rt ∈ Ω(1 + _n7862)

Induction Base:
mark'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(0)) →_R^Ω(1)
tt'

Induction Step:
mark'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(+(_$n7863, 1))) →_R^Ω(1)
s'(mark'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(_$n7863))) →_IH
s'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(_$n7863))

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

Lemmas:
mark'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(_n7862)) → _gen_tt':s':0':plus':isNat':U11':U21':and'2(_n7862), rt ∈ Ω(1 + _n7862)
a__isNat'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(+(1, _n5599))) → _*3, rt ∈ Ω(_n5599)

Generator Equations:
_gen_tt':s':0':plus':isNat':U11':U21':and'2(0) ⇔ tt'
_gen_tt':s':0':plus':isNat':U11':U21':and'2(+(x, 1)) ⇔ s'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(x))

The following defined symbols remain to be analysed:
a__U11', a__U21', a__plus'

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

Generator Equations:
_gen_tt':s':0':plus':isNat':U11':U21':and'2(0) ⇔ tt'
_gen_tt':s':0':plus':isNat':U11':U21':and'2(+(x, 1)) ⇔ s'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(x))

The following defined symbols remain to be analysed:
a__U21', a__plus'

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

Generator Equations:
_gen_tt':s':0':plus':isNat':U11':U21':and'2(0) ⇔ tt'
_gen_tt':s':0':plus':isNat':U11':U21':and'2(+(x, 1)) ⇔ s'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(x))

The following defined symbols remain to be analysed:
a__plus'

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

Generator Equations:
_gen_tt':s':0':plus':isNat':U11':U21':and'2(0) ⇔ tt'
_gen_tt':s':0':plus':isNat':U11':U21':and'2(+(x, 1)) ⇔ s'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
mark'(_gen_tt':s':0':plus':isNat':U11':U21':and'2(_n7862)) → _gen_tt':s':0':plus':isNat':U11':U21':and'2(_n7862), rt ∈ Ω(1 + _n7862)