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__U21(tt, M, N) → a__U22(tt, M, N)
a__U22(tt, M, N) → a__plus(a__x(mark(N), mark(M)), mark(N))
a__plus(N, 0) → mark(N)
a__plus(N, s(M)) → a__U11(tt, M, N)
a__x(N, 0) → 0
a__x(N, s(M)) → a__U21(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(U21(X1, X2, X3)) → a__U21(mark(X1), X2, X3)
mark(U22(X1, X2, X3)) → a__U22(mark(X1), X2, X3)
mark(x(X1, X2)) → a__x(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)
a__U21(X1, X2, X3) → U21(X1, X2, X3)
a__U22(X1, X2, X3) → U22(X1, X2, X3)
a__x(X1, X2) → x(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__U21'(tt', M, N) → a__U22'(tt', M, N)
a__U22'(tt', M, N) → a__plus'(a__x'(mark'(N), mark'(M)), mark'(N))
a__plus'(N, 0') → mark'(N)
a__plus'(N, s'(M)) → a__U11'(tt', M, N)
a__x'(N, 0') → 0'
a__x'(N, s'(M)) → a__U21'(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'(U21'(X1, X2, X3)) → a__U21'(mark'(X1), X2, X3)
mark'(U22'(X1, X2, X3)) → a__U22'(mark'(X1), X2, X3)
mark'(x'(X1, X2)) → a__x'(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)
a__U21'(X1, X2, X3) → U21'(X1, X2, X3)
a__U22'(X1, X2, X3) → U22'(X1, X2, X3)
a__x'(X1, X2) → x'(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__U21'(tt', M, N) → a__U22'(tt', M, N)
a__U22'(tt', M, N) → a__plus'(a__x'(mark'(N), mark'(M)), mark'(N))
a__plus'(N, 0') → mark'(N)
a__plus'(N, s'(M)) → a__U11'(tt', M, N)
a__x'(N, 0') → 0'
a__x'(N, s'(M)) → a__U21'(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'(U21'(X1, X2, X3)) → a__U21'(mark'(X1), X2, X3)
mark'(U22'(X1, X2, X3)) → a__U22'(mark'(X1), X2, X3)
mark'(x'(X1, X2)) → a__x'(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)
a__U21'(X1, X2, X3) → U21'(X1, X2, X3)
a__U22'(X1, X2, X3) → U22'(X1, X2, X3)
a__x'(X1, X2) → x'(X1, X2)

Types:
a__U11' :: tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x'
tt' :: tt':s':0':U11':U12':plus':U21':U22':x'
a__U12' :: tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x'
s' :: tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x'
a__plus' :: tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x'
mark' :: tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x'
a__U21' :: tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x'
a__U22' :: tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x'
a__x' :: tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x'
0' :: tt':s':0':U11':U12':plus':U21':U22':x'
U11' :: tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x'
U12' :: tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x'
plus' :: tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x'
U21' :: tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x'
U22' :: tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x'
x' :: tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x' → tt':s':0':U11':U12':plus':U21':U22':x'
_hole_tt':s':0':U11':U12':plus':U21':U22':x'1 :: tt':s':0':U11':U12':plus':U21':U22':x'
_gen_tt':s':0':U11':U12':plus':U21':U22':x'2 :: Nat → tt':s':0':U11':U12':plus':U21':U22':x'

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Induction Step:
a__U11'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(_$n325272, 1)), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c325885)) →_R^Ω(1)
a__U12'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(_$n325272, 1)), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c325885)) →_R^Ω(1)
s'(a__plus'(mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c325885)), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n325272))))) →_L^{Ω(1 + _c325885)}
s'(a__plus'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c325885), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n325272))))) →_L^{Ω(2 + _$n325272)}
s'(a__plus'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c325885), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n325272)))) →_R^Ω(1)
s'(a__U11'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_$n325272), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c325885))) →_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':U21':U22':x'2(0) ⇔ tt'
_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(x, 1)) ⇔ s'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(x))

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

Proved the following rewrite lemma:
a__U21'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n336614), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c337691·_n336614 + _n336614 + _n336614²)

Induction Base:
a__U21'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c))

Induction Step:
a__U21'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(_$n336615, 1)), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c337691)) →_R^Ω(1)
a__U22'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(_$n336615, 1)), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c337691)) →_R^Ω(1)
a__plus'(a__x'(mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c337691)), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n336615)))), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c337691))) →_L^{Ω(1 + _c337691)}
a__plus'(a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c337691), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n336615)))), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c337691))) →_L^{Ω(2 + _$n336615)}
a__plus'(a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c337691), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n336615))), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c337691))) →_R^Ω(1)
a__plus'(a__U21'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_$n336615), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c337691)), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c337691))) →_IH
a__plus'(_*3, mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c337691))) →_L^{Ω(1 + _c337691)}
a__plus'(_*3, _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c337691))

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

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

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

Proved the following rewrite lemma:
a__U22'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n363483), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c364910·_n363483 + _n363483 + _n363483²)

Induction Base:
a__U22'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c))

Induction Step:
a__U22'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(_$n363484, 1)), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c364910)) →_R^Ω(1)
a__plus'(a__x'(mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c364910)), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(_$n363484, 1)))), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c364910))) →_L^{Ω(1 + _c364910)}
a__plus'(a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c364910), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n363484)))), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c364910))) →_L^{Ω(2 + _$n363484)}
a__plus'(a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c364910), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n363484))), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c364910))) →_R^Ω(1)
a__plus'(a__U21'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_$n363484), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c364910)), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c364910))) →_R^Ω(1)
a__plus'(a__U22'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_$n363484), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c364910)), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c364910))) →_IH
a__plus'(_*3, mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c364910))) →_L^{Ω(1 + _c364910)}
a__plus'(_*3, _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c364910))

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

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

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

Proved the following rewrite lemma:
a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(a), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _n390497))) → _*3, rt ∈ Ω(_a392410·_n390497 + _n390497 + _n390497²)

Induction Base:
a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(a), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, 0)))

Induction Step:
a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a392410), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, +(_$n390498, 1)))) →_R^Ω(1)
a__U21'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n390498)), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a392410)) →_R^Ω(1)
a__U22'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n390498)), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a392410)) →_R^Ω(1)
a__plus'(a__x'(mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a392410)), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n390498)))), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a392410))) →_L^{Ω(1 + _a392410)}
a__plus'(a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a392410), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n390498)))), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a392410))) →_L^{Ω(2 + _$n390498)}
a__plus'(a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a392410), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n390498))), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a392410))) →_IH
a__plus'(_*3, mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a392410))) →_L^{Ω(1 + _a392410)}
a__plus'(_*3, _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a392410))

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

Lemmas:
mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n321190)) → _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n321190), rt ∈ Ω(1 + _n321190)
a__U11'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n325271), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c325885·_n325271 + _n325271 + _n325271²)
a__U21'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n336614), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c337691·_n336614 + _n336614 + _n336614²)
a__U22'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n363483), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c364910·_n363483 + _n363483 + _n363483²)
a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(a), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _n390497))) → _*3, rt ∈ Ω(_a392410·_n390497 + _n390497 + _n390497²)

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

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

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

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

Induction Step:
a__U12'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(_$n420701, 1)), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c422892)) →_R^Ω(1)
s'(a__plus'(mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c422892)), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(_$n420701, 1))))) →_L^{Ω(1 + _c422892)}
s'(a__plus'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c422892), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n420701))))) →_L^{Ω(2 + _$n420701)}
s'(a__plus'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c422892), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n420701)))) →_R^Ω(1)
s'(a__U11'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_$n420701), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c422892))) →_R^Ω(1)
s'(a__U12'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_$n420701), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c422892))) →_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':U21':U22':x'2(0) ⇔ tt'
_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(x, 1)) ⇔ s'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(x))

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

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

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

Induction Step:
a__plus'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a436658), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, +(_$n433954, 1)))) →_R^Ω(1)
a__U11'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n433954)), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a436658)) →_R^Ω(1)
a__U12'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n433954)), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a436658)) →_R^Ω(1)
s'(a__plus'(mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a436658)), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n433954))))) →_L^{Ω(1 + _a436658)}
s'(a__plus'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a436658), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n433954))))) →_L^{Ω(2 + _$n433954)}
s'(a__plus'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a436658), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n433954)))) →_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':U21':U22':x'2(0) ⇔ tt'
_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(x, 1)) ⇔ s'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(x))

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

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

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

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

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

Lemmas:
mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n450080)) → _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n450080), rt ∈ Ω(1 + _n450080)
a__U11'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n325271), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c325885·_n325271 + _n325271 + _n325271²)
a__U21'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n336614), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c337691·_n336614 + _n336614 + _n336614²)
a__U22'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n363483), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c364910·_n363483 + _n363483 + _n363483²)
a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(a), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _n390497))) → _*3, rt ∈ Ω(_a392410·_n390497 + _n390497 + _n390497²)
a__U12'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n420700), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c422892·_n420700 + _n420700 + _n420700²)
a__plus'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(a), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _n433953))) → _*3, rt ∈ Ω(_a436658·_n433953 + _n433953 + _n433953²)

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

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

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

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

Induction Step:
a__U11'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(_$n454522, 1)), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c457661)) →_R^Ω(1)
a__U12'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(_$n454522, 1)), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c457661)) →_R^Ω(1)
s'(a__plus'(mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c457661)), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n454522))))) →_L^{Ω(1 + _c457661)}
s'(a__plus'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c457661), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n454522))))) →_L^{Ω(2 + _$n454522)}
s'(a__plus'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c457661), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n454522)))) →_R^Ω(1)
s'(a__U11'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_$n454522), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c457661))) →_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':U21':U22':x'2(_n450080)) → _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n450080), rt ∈ Ω(1 + _n450080)
a__U11'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n454521), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c457661·_n454521 + _n454521 + _n454521²)
a__U21'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n336614), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c337691·_n336614 + _n336614 + _n336614²)
a__U22'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n363483), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c364910·_n363483 + _n363483 + _n363483²)
a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(a), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _n390497))) → _*3, rt ∈ Ω(_a392410·_n390497 + _n390497 + _n390497²)
a__U12'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n420700), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c422892·_n420700 + _n420700 + _n420700²)
a__plus'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(a), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _n433953))) → _*3, rt ∈ Ω(_a436658·_n433953 + _n433953 + _n433953²)

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

The following defined symbols remain to be analysed:
a__U21', a__U12', a__U22', a__x'

Proved the following rewrite lemma:
a__U21'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n470532), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c473714·_n470532 + _n470532 + _n470532²)

Induction Base:
a__U21'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c))

Induction Step:
a__U21'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(_$n470533, 1)), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c473714)) →_R^Ω(1)
a__U22'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(_$n470533, 1)), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c473714)) →_R^Ω(1)
a__plus'(a__x'(mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c473714)), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n470533)))), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c473714))) →_L^{Ω(1 + _c473714)}
a__plus'(a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c473714), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n470533)))), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c473714))) →_L^{Ω(2 + _$n470533)}
a__plus'(a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c473714), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n470533))), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c473714))) →_R^Ω(1)
a__plus'(a__U21'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_$n470533), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c473714)), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c473714))) →_IH
a__plus'(_*3, mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c473714))) →_L^{Ω(1 + _c473714)}
a__plus'(_*3, _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c473714))

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

Lemmas:
mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n450080)) → _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n450080), rt ∈ Ω(1 + _n450080)
a__U11'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n454521), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c457661·_n454521 + _n454521 + _n454521²)
a__U21'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n470532), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c473714·_n470532 + _n470532 + _n470532²)
a__U22'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n363483), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c364910·_n363483 + _n363483 + _n363483²)
a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(a), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _n390497))) → _*3, rt ∈ Ω(_a392410·_n390497 + _n390497 + _n390497²)
a__U12'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n420700), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c422892·_n420700 + _n420700 + _n420700²)
a__plus'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(a), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _n433953))) → _*3, rt ∈ Ω(_a436658·_n433953 + _n433953 + _n433953²)

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

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

Proved the following rewrite lemma:
a__U22'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n503621), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c506712·_n503621 + _n503621 + _n503621²)

Induction Base:
a__U22'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c))

Induction Step:
a__U22'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(_$n503622, 1)), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c506712)) →_R^Ω(1)
a__plus'(a__x'(mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c506712)), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(_$n503622, 1)))), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c506712))) →_L^{Ω(1 + _c506712)}
a__plus'(a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c506712), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n503622)))), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c506712))) →_L^{Ω(2 + _$n503622)}
a__plus'(a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c506712), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n503622))), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c506712))) →_R^Ω(1)
a__plus'(a__U21'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_$n503622), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c506712)), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c506712))) →_R^Ω(1)
a__plus'(a__U22'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_$n503622), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c506712)), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c506712))) →_IH
a__plus'(_*3, mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c506712))) →_L^{Ω(1 + _c506712)}
a__plus'(_*3, _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c506712))

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

Lemmas:
mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n450080)) → _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n450080), rt ∈ Ω(1 + _n450080)
a__U11'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n454521), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c457661·_n454521 + _n454521 + _n454521²)
a__U21'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n470532), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c473714·_n470532 + _n470532 + _n470532²)
a__U22'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n503621), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c506712·_n503621 + _n503621 + _n503621²)
a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(a), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _n390497))) → _*3, rt ∈ Ω(_a392410·_n390497 + _n390497 + _n390497²)
a__U12'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n420700), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c422892·_n420700 + _n420700 + _n420700²)
a__plus'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(a), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _n433953))) → _*3, rt ∈ Ω(_a436658·_n433953 + _n433953 + _n433953²)

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

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

Proved the following rewrite lemma:
a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(a), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _n535455))) → _*3, rt ∈ Ω(_a538619·_n535455 + _n535455 + _n535455²)

Induction Base:
a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(a), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, 0)))

Induction Step:
a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a538619), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, +(_$n535456, 1)))) →_R^Ω(1)
a__U21'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n535456)), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a538619)) →_R^Ω(1)
a__U22'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n535456)), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a538619)) →_R^Ω(1)
a__plus'(a__x'(mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a538619)), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n535456)))), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a538619))) →_L^{Ω(1 + _a538619)}
a__plus'(a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a538619), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n535456)))), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a538619))) →_L^{Ω(2 + _$n535456)}
a__plus'(a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a538619), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n535456))), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a538619))) →_IH
a__plus'(_*3, mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a538619))) →_L^{Ω(1 + _a538619)}
a__plus'(_*3, _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_a538619))

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

Lemmas:
mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n450080)) → _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n450080), rt ∈ Ω(1 + _n450080)
a__U11'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n454521), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c457661·_n454521 + _n454521 + _n454521²)
a__U21'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n470532), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c473714·_n470532 + _n470532 + _n470532²)
a__U22'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n503621), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c506712·_n503621 + _n503621 + _n503621²)
a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(a), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _n535455))) → _*3, rt ∈ Ω(_a538619·_n535455 + _n535455 + _n535455²)
a__U12'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n420700), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c422892·_n420700 + _n420700 + _n420700²)
a__plus'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(a), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _n433953))) → _*3, rt ∈ Ω(_a436658·_n433953 + _n433953 + _n433953²)

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

The following defined symbols remain to be analysed:
a__U12'

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

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

Induction Step:
a__U12'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(_$n569463, 1)), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c572486)) →_R^Ω(1)
s'(a__plus'(mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c572486)), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(_$n569463, 1))))) →_L^{Ω(1 + _c572486)}
s'(a__plus'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c572486), mark'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n569463))))) →_L^{Ω(2 + _$n569463)}
s'(a__plus'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c572486), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _$n569463)))) →_R^Ω(1)
s'(a__U11'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_$n569463), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c572486))) →_R^Ω(1)
s'(a__U12'(tt', _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_$n569463), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_c572486))) →_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':U21':U22':x'2(_n450080)) → _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n450080), rt ∈ Ω(1 + _n450080)
a__U11'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n454521), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c457661·_n454521 + _n454521 + _n454521²)
a__U21'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n470532), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c473714·_n470532 + _n470532 + _n470532²)
a__U22'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n503621), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c506712·_n503621 + _n503621 + _n503621²)
a__x'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(a), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _n535455))) → _*3, rt ∈ Ω(_a538619·_n535455 + _n535455 + _n535455²)
a__U12'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n569462), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c572486·_n569462 + _n569462 + _n569462²)
a__plus'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(a), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(1, _n433953))) → _*3, rt ∈ Ω(_a436658·_n433953 + _n433953 + _n433953²)

Generator Equations:
_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(0) ⇔ tt'
_gen_tt':s':0':U11':U12':plus':U21':U22':x'2(+(x, 1)) ⇔ s'(_gen_tt':s':0':U11':U12':plus':U21':U22':x'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':U21':U22':x'2(0), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(_n454521), _gen_tt':s':0':U11':U12':plus':U21':U22':x'2(c)) → _*3, rt ∈ Ω(_c457661·_n454521 + _n454521 + _n454521²)