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

a__U11(tt, M, N) → a__U12(tt, M, N)
a__U12(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__plus(N, 0) → mark(N)
a__plus(N, s(M)) → a__U11(tt, M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)
mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))
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, X3) → U12(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

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', M, N) → a__U12'(tt', M, N)
a__U12'(tt', M, N) → s'(a__plus'(mark'(N), mark'(M)))
a__plus'(N, 0') → mark'(N)
a__plus'(N, s'(M)) → a__U11'(tt', M, N)
mark'(U11'(X1, X2, X3)) → a__U11'(mark'(X1), X2, X3)
mark'(U12'(X1, X2, X3)) → a__U12'(mark'(X1), X2, X3)
mark'(plus'(X1, X2)) → a__plus'(mark'(X1), mark'(X2))
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, X3) → U12'(X1, X2, X3)
a__plus'(X1, X2) → plus'(X1, X2)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
a__U11'(tt', M, N) → a__U12'(tt', M, N)
a__U12'(tt', M, N) → s'(a__plus'(mark'(N), mark'(M)))
a__plus'(N, 0') → mark'(N)
a__plus'(N, s'(M)) → a__U11'(tt', M, N)
mark'(U11'(X1, X2, X3)) → a__U11'(mark'(X1), X2, X3)
mark'(U12'(X1, X2, X3)) → a__U12'(mark'(X1), X2, X3)
mark'(plus'(X1, X2)) → a__plus'(mark'(X1), mark'(X2))
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, X3) → U12'(X1, X2, X3)
a__plus'(X1, X2) → plus'(X1, X2)

Types:
a__U11' :: tt':s':0':U11':U12':plus' → tt':s':0':U11':U12':plus' → tt':s':0':U11':U12':plus' → tt':s':0':U11':U12':plus'
tt' :: tt':s':0':U11':U12':plus'
a__U12' :: tt':s':0':U11':U12':plus' → tt':s':0':U11':U12':plus' → tt':s':0':U11':U12':plus' → tt':s':0':U11':U12':plus'
s' :: tt':s':0':U11':U12':plus' → tt':s':0':U11':U12':plus'
a__plus' :: tt':s':0':U11':U12':plus' → tt':s':0':U11':U12':plus' → tt':s':0':U11':U12':plus'
mark' :: tt':s':0':U11':U12':plus' → tt':s':0':U11':U12':plus'
0' :: tt':s':0':U11':U12':plus'
U11' :: tt':s':0':U11':U12':plus' → tt':s':0':U11':U12':plus' → tt':s':0':U11':U12':plus' → tt':s':0':U11':U12':plus'
U12' :: tt':s':0':U11':U12':plus' → tt':s':0':U11':U12':plus' → tt':s':0':U11':U12':plus' → tt':s':0':U11':U12':plus'
plus' :: tt':s':0':U11':U12':plus' → tt':s':0':U11':U12':plus' → tt':s':0':U11':U12':plus'
_hole_tt':s':0':U11':U12':plus'1 :: tt':s':0':U11':U12':plus'
_gen_tt':s':0':U11':U12':plus'2 :: Nat → tt':s':0':U11':U12':plus'

Heuristically decided to analyse the following defined symbols:
a__U11', a__U12', a__plus', mark'

They will be analysed ascendingly in the following order:
a__U11' = a__U12'
a__U11' = a__plus'
a__U11' = mark'
a__U12' = a__plus'
a__U12' = mark'
a__plus' = mark'

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

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

They will be analysed ascendingly in the following order:
a__U11' = a__U12'
a__U11' = a__plus'
a__U11' = mark'
a__U12' = a__plus'
a__U12' = mark'
a__plus' = mark'

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

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

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

They will be analysed ascendingly in the following order:
a__U11' = a__U12'
a__U11' = a__plus'
a__U11' = mark'
a__U12' = a__plus'
a__U12' = mark'
a__plus' = mark'

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

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

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

They will be analysed ascendingly in the following order:
a__U11' = a__U12'
a__U11' = a__plus'
a__U11' = mark'
a__U12' = a__plus'
a__U12' = mark'
a__plus' = mark'

Proved the following rewrite lemma:
mark'(_gen_tt':s':0':U11':U12':plus'2(_n31122)) → _gen_tt':s':0':U11':U12':plus'2(_n31122), rt ∈ Ω(1 + _n31122)

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

Induction Step:
mark'(_gen_tt':s':0':U11':U12':plus'2(+(_$n31123, 1))) →_R^Ω(1)
s'(mark'(_gen_tt':s':0':U11':U12':plus'2(_$n31123))) →_IH
s'(_gen_tt':s':0':U11':U12':plus'2(_$n31123))

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

Lemmas:
mark'(_gen_tt':s':0':U11':U12':plus'2(_n31122)) → _gen_tt':s':0':U11':U12':plus'2(_n31122), rt ∈ Ω(1 + _n31122)

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

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

They will be analysed ascendingly in the following order:
a__U11' = a__U12'
a__U11' = a__plus'
a__U11' = mark'
a__U12' = a__plus'
a__U12' = mark'
a__plus' = mark'

Proved the following rewrite lemma:
a__U11'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(_n31893), _gen_tt':s':0':U11':U12':plus'2(c)) → _*3, rt ∈ Ω(_c32507·_n31893 + _n31893 + _n31893²)

Induction Base:
a__U11'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(c))

Induction Step:
a__U11'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(+(_$n31894, 1)), _gen_tt':s':0':U11':U12':plus'2(_c32507)) →_R^Ω(1)
a__U12'(tt', _gen_tt':s':0':U11':U12':plus'2(+(_$n31894, 1)), _gen_tt':s':0':U11':U12':plus'2(_c32507)) →_R^Ω(1)
s'(a__plus'(mark'(_gen_tt':s':0':U11':U12':plus'2(_c32507)), mark'(_gen_tt':s':0':U11':U12':plus'2(+(1, _$n31894))))) →_L^{Ω(1 + _c32507)}
s'(a__plus'(_gen_tt':s':0':U11':U12':plus'2(_c32507), mark'(_gen_tt':s':0':U11':U12':plus'2(+(1, _$n31894))))) →_L^{Ω(2 + _$n31894)}
s'(a__plus'(_gen_tt':s':0':U11':U12':plus'2(_c32507), _gen_tt':s':0':U11':U12':plus'2(+(1, _$n31894)))) →_R^Ω(1)
s'(a__U11'(tt', _gen_tt':s':0':U11':U12':plus'2(_$n31894), _gen_tt':s':0':U11':U12':plus'2(_c32507))) →_IH
s'(_*3)

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

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

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

They will be analysed ascendingly in the following order:
a__U11' = a__U12'
a__U11' = a__plus'
a__U11' = mark'
a__U12' = a__plus'
a__U12' = mark'
a__plus' = mark'

Proved the following rewrite lemma:
a__U12'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(_n38268), _gen_tt':s':0':U11':U12':plus'2(c)) → _*3, rt ∈ Ω(_c39212·_n38268 + _n38268 + _n38268²)

Induction Base:
a__U12'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(c))

Induction Step:
a__U12'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(+(_$n38269, 1)), _gen_tt':s':0':U11':U12':plus'2(_c39212)) →_R^Ω(1)
s'(a__plus'(mark'(_gen_tt':s':0':U11':U12':plus'2(_c39212)), mark'(_gen_tt':s':0':U11':U12':plus'2(+(_$n38269, 1))))) →_L^{Ω(1 + _c39212)}
s'(a__plus'(_gen_tt':s':0':U11':U12':plus'2(_c39212), mark'(_gen_tt':s':0':U11':U12':plus'2(+(1, _$n38269))))) →_L^{Ω(2 + _$n38269)}
s'(a__plus'(_gen_tt':s':0':U11':U12':plus'2(_c39212), _gen_tt':s':0':U11':U12':plus'2(+(1, _$n38269)))) →_R^Ω(1)
s'(a__U11'(tt', _gen_tt':s':0':U11':U12':plus'2(_$n38269), _gen_tt':s':0':U11':U12':plus'2(_c39212))) →_R^Ω(1)
s'(a__U12'(tt', _gen_tt':s':0':U11':U12':plus'2(_$n38269), _gen_tt':s':0':U11':U12':plus'2(_c39212))) →_IH
s'(_*3)

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

Lemmas:
mark'(_gen_tt':s':0':U11':U12':plus'2(_n31122)) → _gen_tt':s':0':U11':U12':plus'2(_n31122), rt ∈ Ω(1 + _n31122)
a__U11'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(_n31893), _gen_tt':s':0':U11':U12':plus'2(c)) → _*3, rt ∈ Ω(_c32507·_n31893 + _n31893 + _n31893²)
a__U12'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(_n38268), _gen_tt':s':0':U11':U12':plus'2(c)) → _*3, rt ∈ Ω(_c39212·_n38268 + _n38268 + _n38268²)

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

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

They will be analysed ascendingly in the following order:
a__U11' = a__U12'
a__U11' = a__plus'
a__U11' = mark'
a__U12' = a__plus'
a__U12' = mark'
a__plus' = mark'

Proved the following rewrite lemma:
a__plus'(_gen_tt':s':0':U11':U12':plus'2(a), _gen_tt':s':0':U11':U12':plus'2(+(1, _n44784))) → _*3, rt ∈ Ω(_a46238·_n44784 + _n44784 + _n44784²)

Induction Base:
a__plus'(_gen_tt':s':0':U11':U12':plus'2(a), _gen_tt':s':0':U11':U12':plus'2(+(1, 0)))

Induction Step:
a__plus'(_gen_tt':s':0':U11':U12':plus'2(_a46238), _gen_tt':s':0':U11':U12':plus'2(+(1, +(_$n44785, 1)))) →_R^Ω(1)
a__U11'(tt', _gen_tt':s':0':U11':U12':plus'2(+(1, _$n44785)), _gen_tt':s':0':U11':U12':plus'2(_a46238)) →_R^Ω(1)
a__U12'(tt', _gen_tt':s':0':U11':U12':plus'2(+(1, _$n44785)), _gen_tt':s':0':U11':U12':plus'2(_a46238)) →_R^Ω(1)
s'(a__plus'(mark'(_gen_tt':s':0':U11':U12':plus'2(_a46238)), mark'(_gen_tt':s':0':U11':U12':plus'2(+(1, _$n44785))))) →_L^{Ω(1 + _a46238)}
s'(a__plus'(_gen_tt':s':0':U11':U12':plus'2(_a46238), mark'(_gen_tt':s':0':U11':U12':plus'2(+(1, _$n44785))))) →_L^{Ω(2 + _$n44785)}
s'(a__plus'(_gen_tt':s':0':U11':U12':plus'2(_a46238), _gen_tt':s':0':U11':U12':plus'2(+(1, _$n44785)))) →_IH
s'(_*3)

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

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

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

They will be analysed ascendingly in the following order:
a__U11' = a__U12'
a__U11' = a__plus'
a__U11' = mark'
a__U12' = a__plus'
a__U12' = mark'
a__plus' = mark'

Proved the following rewrite lemma:
mark'(_gen_tt':s':0':U11':U12':plus'2(_n53175)) → _gen_tt':s':0':U11':U12':plus'2(_n53175), rt ∈ Ω(1 + _n53175)

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

Induction Step:
mark'(_gen_tt':s':0':U11':U12':plus'2(+(_$n53176, 1))) →_R^Ω(1)
s'(mark'(_gen_tt':s':0':U11':U12':plus'2(_$n53176))) →_IH
s'(_gen_tt':s':0':U11':U12':plus'2(_$n53176))

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

Lemmas:
mark'(_gen_tt':s':0':U11':U12':plus'2(_n53175)) → _gen_tt':s':0':U11':U12':plus'2(_n53175), rt ∈ Ω(1 + _n53175)
a__U11'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(_n31893), _gen_tt':s':0':U11':U12':plus'2(c)) → _*3, rt ∈ Ω(_c32507·_n31893 + _n31893 + _n31893²)
a__U12'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(_n38268), _gen_tt':s':0':U11':U12':plus'2(c)) → _*3, rt ∈ Ω(_c39212·_n38268 + _n38268 + _n38268²)
a__plus'(_gen_tt':s':0':U11':U12':plus'2(a), _gen_tt':s':0':U11':U12':plus'2(+(1, _n44784))) → _*3, rt ∈ Ω(_a46238·_n44784 + _n44784 + _n44784²)

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

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

They will be analysed ascendingly in the following order:
a__U11' = a__U12'
a__U11' = a__plus'
a__U11' = mark'
a__U12' = a__plus'
a__U12' = mark'
a__plus' = mark'

Proved the following rewrite lemma:
a__U11'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(_n54126), _gen_tt':s':0':U11':U12':plus'2(c)) → _*3, rt ∈ Ω(_c56003·_n54126 + _n54126 + _n54126²)

Induction Base:
a__U11'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(c))

Induction Step:
a__U11'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(+(_$n54127, 1)), _gen_tt':s':0':U11':U12':plus'2(_c56003)) →_R^Ω(1)
a__U12'(tt', _gen_tt':s':0':U11':U12':plus'2(+(_$n54127, 1)), _gen_tt':s':0':U11':U12':plus'2(_c56003)) →_R^Ω(1)
s'(a__plus'(mark'(_gen_tt':s':0':U11':U12':plus'2(_c56003)), mark'(_gen_tt':s':0':U11':U12':plus'2(+(1, _$n54127))))) →_L^{Ω(1 + _c56003)}
s'(a__plus'(_gen_tt':s':0':U11':U12':plus'2(_c56003), mark'(_gen_tt':s':0':U11':U12':plus'2(+(1, _$n54127))))) →_L^{Ω(2 + _$n54127)}
s'(a__plus'(_gen_tt':s':0':U11':U12':plus'2(_c56003), _gen_tt':s':0':U11':U12':plus'2(+(1, _$n54127)))) →_R^Ω(1)
s'(a__U11'(tt', _gen_tt':s':0':U11':U12':plus'2(_$n54127), _gen_tt':s':0':U11':U12':plus'2(_c56003))) →_IH
s'(_*3)

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

Lemmas:
mark'(_gen_tt':s':0':U11':U12':plus'2(_n53175)) → _gen_tt':s':0':U11':U12':plus'2(_n53175), rt ∈ Ω(1 + _n53175)
a__U11'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(_n54126), _gen_tt':s':0':U11':U12':plus'2(c)) → _*3, rt ∈ Ω(_c56003·_n54126 + _n54126 + _n54126²)
a__U12'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(_n38268), _gen_tt':s':0':U11':U12':plus'2(c)) → _*3, rt ∈ Ω(_c39212·_n38268 + _n38268 + _n38268²)
a__plus'(_gen_tt':s':0':U11':U12':plus'2(a), _gen_tt':s':0':U11':U12':plus'2(+(1, _n44784))) → _*3, rt ∈ Ω(_a46238·_n44784 + _n44784 + _n44784²)

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

The following defined symbols remain to be analysed:
a__U12'

They will be analysed ascendingly in the following order:
a__U11' = a__U12'
a__U11' = a__plus'
a__U11' = mark'
a__U12' = a__plus'
a__U12' = mark'
a__plus' = mark'

Proved the following rewrite lemma:
a__U12'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(_n62835), _gen_tt':s':0':U11':U12':plus'2(c)) → _*3, rt ∈ Ω(_c64611·_n62835 + _n62835 + _n62835²)

Induction Base:
a__U12'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(c))

Induction Step:
a__U12'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(+(_$n62836, 1)), _gen_tt':s':0':U11':U12':plus'2(_c64611)) →_R^Ω(1)
s'(a__plus'(mark'(_gen_tt':s':0':U11':U12':plus'2(_c64611)), mark'(_gen_tt':s':0':U11':U12':plus'2(+(_$n62836, 1))))) →_L^{Ω(1 + _c64611)}
s'(a__plus'(_gen_tt':s':0':U11':U12':plus'2(_c64611), mark'(_gen_tt':s':0':U11':U12':plus'2(+(1, _$n62836))))) →_L^{Ω(2 + _$n62836)}
s'(a__plus'(_gen_tt':s':0':U11':U12':plus'2(_c64611), _gen_tt':s':0':U11':U12':plus'2(+(1, _$n62836)))) →_R^Ω(1)
s'(a__U11'(tt', _gen_tt':s':0':U11':U12':plus'2(_$n62836), _gen_tt':s':0':U11':U12':plus'2(_c64611))) →_R^Ω(1)
s'(a__U12'(tt', _gen_tt':s':0':U11':U12':plus'2(_$n62836), _gen_tt':s':0':U11':U12':plus'2(_c64611))) →_IH
s'(_*3)

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

Lemmas:
mark'(_gen_tt':s':0':U11':U12':plus'2(_n53175)) → _gen_tt':s':0':U11':U12':plus'2(_n53175), rt ∈ Ω(1 + _n53175)
a__U11'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(_n54126), _gen_tt':s':0':U11':U12':plus'2(c)) → _*3, rt ∈ Ω(_c56003·_n54126 + _n54126 + _n54126²)
a__U12'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(_n62835), _gen_tt':s':0':U11':U12':plus'2(c)) → _*3, rt ∈ Ω(_c64611·_n62835 + _n62835 + _n62835²)
a__plus'(_gen_tt':s':0':U11':U12':plus'2(a), _gen_tt':s':0':U11':U12':plus'2(+(1, _n44784))) → _*3, rt ∈ Ω(_a46238·_n44784 + _n44784 + _n44784²)

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

No more defined symbols left to analyse.

The lowerbound Ω(n²) was proven with the following lemma:
a__U11'(_gen_tt':s':0':U11':U12':plus'2(0), _gen_tt':s':0':U11':U12':plus'2(_n54126), _gen_tt':s':0':U11':U12':plus'2(c)) → _*3, rt ∈ Ω(_c56003·_n54126 + _n54126 + _n54126²)