WORST_CASE(Omega(n^2),?)
proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^2, INF).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 760 ms]
(2) CpxRelTRS
(3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) typed CpxTrs
(7) OrderProof [LOWER BOUND(ID), 1 ms]
(8) typed CpxTrs
(9) RewriteLemmaProof [LOWER BOUND(ID), 255 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 78 ms]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 1617 ms]
        (18) BEST
            (19) proven lower bound
                (20) LowerBoundPropagationProof [FINISHED, 0 ms]
                (21) BOUNDS(n^2, INF)
            (22) typed CpxTrs
                (23) RewriteLemmaProof [LOWER BOUND(ID), 0 ms]
                (24) typed CpxTrs
                (25) RewriteLemmaProof [LOWER BOUND(ID), 33 ms]
                (26) typed CpxTrs
                (27) RewriteLemmaProof [LOWER BOUND(ID), 1191 ms]
                (28) typed CpxTrs
                (29) RewriteLemmaProof [LOWER BOUND(ID), 1070 ms]
                (30) typed CpxTrs


----------------------------------------

(0)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^2, INF).


The TRS R consists of the following rules:

   PLUS(0, z0) -> c
   PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
   TIMES(0, z0) -> c2
   TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
   EXP(z0, 0) -> c4
   EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
   P(s(0)) -> c6
   P(s(s(z0))) -> c7(P(s(z0)))
   TOWER(z0, z1) -> c8(TOWERITER(z0, z1, s(0)))
   TOWERITER(0, z0, z1) -> c9
   TOWERITER(s(z0), z1, z2) -> c10(TOWERITER(p(s(z0)), z1, exp(z1, z2)), P(s(z0)))
   TOWERITER(s(z0), z1, z2) -> c11(TOWERITER(p(s(z0)), z1, exp(z1, z2)), EXP(z1, z2))

The (relative) TRS S consists of the following rules:

   plus(0, z0) -> z0
   plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
   times(0, z0) -> 0
   times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
   exp(z0, 0) -> s(0)
   exp(z0, s(z1)) -> times(z0, exp(z0, z1))
   p(s(0)) -> 0
   p(s(s(z0))) -> s(p(s(z0)))
   tower(z0, z1) -> towerIter(z0, z1, s(0))
   towerIter(0, z0, z1) -> z1
   towerIter(s(z0), z1, z2) -> towerIter(p(s(z0)), z1, exp(z1, z2))

Rewrite Strategy: INNERMOST
----------------------------------------

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

(2)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^2, INF).


The TRS R consists of the following rules:

   PLUS(0, z0) -> c
   PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
   TIMES(0, z0) -> c2
   TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
   EXP(z0, 0) -> c4
   EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
   P(s(0)) -> c6
   P(s(s(z0))) -> c7(P(s(z0)))
   TOWER(z0, z1) -> c8(TOWERITER(z0, z1, s(0)))
   TOWERITER(0, z0, z1) -> c9
   TOWERITER(s(z0), z1, z2) -> c10(TOWERITER(p(s(z0)), z1, exp(z1, z2)), P(s(z0)))
   TOWERITER(s(z0), z1, z2) -> c11(TOWERITER(p(s(z0)), z1, exp(z1, z2)), EXP(z1, z2))

The (relative) TRS S consists of the following rules:

   plus(0, z0) -> z0
   plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
   times(0, z0) -> 0
   times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
   exp(z0, 0) -> s(0)
   exp(z0, s(z1)) -> times(z0, exp(z0, z1))
   p(s(0)) -> 0
   p(s(s(z0))) -> s(p(s(z0)))
   tower(z0, z1) -> towerIter(z0, z1, s(0))
   towerIter(0, z0, z1) -> z1
   towerIter(s(z0), z1, z2) -> towerIter(p(s(z0)), z1, exp(z1, z2))

Rewrite Strategy: INNERMOST
----------------------------------------

(3) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

(4)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^2, INF).


The TRS R consists of the following rules:

   PLUS(0', z0) -> c
   PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
   TIMES(0', z0) -> c2
   TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
   EXP(z0, 0') -> c4
   EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
   P(s(0')) -> c6
   P(s(s(z0))) -> c7(P(s(z0)))
   TOWER(z0, z1) -> c8(TOWERITER(z0, z1, s(0')))
   TOWERITER(0', z0, z1) -> c9
   TOWERITER(s(z0), z1, z2) -> c10(TOWERITER(p(s(z0)), z1, exp(z1, z2)), P(s(z0)))
   TOWERITER(s(z0), z1, z2) -> c11(TOWERITER(p(s(z0)), z1, exp(z1, z2)), EXP(z1, z2))

The (relative) TRS S consists of the following rules:

   plus(0', z0) -> z0
   plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
   times(0', z0) -> 0'
   times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
   exp(z0, 0') -> s(0')
   exp(z0, s(z1)) -> times(z0, exp(z0, z1))
   p(s(0')) -> 0'
   p(s(s(z0))) -> s(p(s(z0)))
   tower(z0, z1) -> towerIter(z0, z1, s(0'))
   towerIter(0', z0, z1) -> z1
   towerIter(s(z0), z1, z2) -> towerIter(p(s(z0)), z1, exp(z1, z2))

Rewrite Strategy: INNERMOST
----------------------------------------

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(6)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
P(s(0')) -> c6
P(s(s(z0))) -> c7(P(s(z0)))
TOWER(z0, z1) -> c8(TOWERITER(z0, z1, s(0')))
TOWERITER(0', z0, z1) -> c9
TOWERITER(s(z0), z1, z2) -> c10(TOWERITER(p(s(z0)), z1, exp(z1, z2)), P(s(z0)))
TOWERITER(s(z0), z1, z2) -> c11(TOWERITER(p(s(z0)), z1, exp(z1, z2)), EXP(z1, z2))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
tower(z0, z1) -> towerIter(z0, z1, s(0'))
towerIter(0', z0, z1) -> z1
towerIter(s(z0), z1, z2) -> towerIter(p(s(z0)), z1, exp(z1, z2))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c6:c7 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c6:c7
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c6:c7 -> c2:c3
times :: 0':s -> 0':s -> 0':s
EXP :: 0':s -> 0':s -> c4:c5
c4 :: c4:c5
c5 :: c2:c3 -> c4:c5 -> c4:c5
exp :: 0':s -> 0':s -> 0':s
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TOWER :: 0':s -> 0':s -> c8
c8 :: c9:c10:c11 -> c8
TOWERITER :: 0':s -> 0':s -> 0':s -> c9:c10:c11
c9 :: c9:c10:c11
c10 :: c9:c10:c11 -> c6:c7 -> c9:c10:c11
c11 :: c9:c10:c11 -> c4:c5 -> c9:c10:c11
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_12 :: c:c1
hole_0':s2_12 :: 0':s
hole_c6:c73_12 :: c6:c7
hole_c2:c34_12 :: c2:c3
hole_c4:c55_12 :: c4:c5
hole_c86_12 :: c8
hole_c9:c10:c117_12 :: c9:c10:c11
gen_c:c18_12 :: Nat -> c:c1
gen_0':s9_12 :: Nat -> 0':s
gen_c6:c710_12 :: Nat -> c6:c7
gen_c2:c311_12 :: Nat -> c2:c3
gen_c4:c512_12 :: Nat -> c4:c5
gen_c9:c10:c1113_12 :: Nat -> c9:c10:c11

----------------------------------------

(7) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
PLUS, p, P, TIMES, times, EXP, exp, TOWERITER, plus, towerIter

They will be analysed ascendingly in the following order:
p < PLUS
P < PLUS
PLUS < TIMES
p < TIMES
p < times
p < TOWERITER
p < plus
p < towerIter
P < TIMES
P < TOWERITER
times < TIMES
TIMES < EXP
times < exp
plus < times
exp < EXP
EXP < TOWERITER
exp < TOWERITER
exp < towerIter

----------------------------------------

(8)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
P(s(0')) -> c6
P(s(s(z0))) -> c7(P(s(z0)))
TOWER(z0, z1) -> c8(TOWERITER(z0, z1, s(0')))
TOWERITER(0', z0, z1) -> c9
TOWERITER(s(z0), z1, z2) -> c10(TOWERITER(p(s(z0)), z1, exp(z1, z2)), P(s(z0)))
TOWERITER(s(z0), z1, z2) -> c11(TOWERITER(p(s(z0)), z1, exp(z1, z2)), EXP(z1, z2))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
tower(z0, z1) -> towerIter(z0, z1, s(0'))
towerIter(0', z0, z1) -> z1
towerIter(s(z0), z1, z2) -> towerIter(p(s(z0)), z1, exp(z1, z2))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c6:c7 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c6:c7
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c6:c7 -> c2:c3
times :: 0':s -> 0':s -> 0':s
EXP :: 0':s -> 0':s -> c4:c5
c4 :: c4:c5
c5 :: c2:c3 -> c4:c5 -> c4:c5
exp :: 0':s -> 0':s -> 0':s
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TOWER :: 0':s -> 0':s -> c8
c8 :: c9:c10:c11 -> c8
TOWERITER :: 0':s -> 0':s -> 0':s -> c9:c10:c11
c9 :: c9:c10:c11
c10 :: c9:c10:c11 -> c6:c7 -> c9:c10:c11
c11 :: c9:c10:c11 -> c4:c5 -> c9:c10:c11
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_12 :: c:c1
hole_0':s2_12 :: 0':s
hole_c6:c73_12 :: c6:c7
hole_c2:c34_12 :: c2:c3
hole_c4:c55_12 :: c4:c5
hole_c86_12 :: c8
hole_c9:c10:c117_12 :: c9:c10:c11
gen_c:c18_12 :: Nat -> c:c1
gen_0':s9_12 :: Nat -> 0':s
gen_c6:c710_12 :: Nat -> c6:c7
gen_c2:c311_12 :: Nat -> c2:c3
gen_c4:c512_12 :: Nat -> c4:c5
gen_c9:c10:c1113_12 :: Nat -> c9:c10:c11


Generator Equations:
gen_c:c18_12(0) <=> c
gen_c:c18_12(+(x, 1)) <=> c1(gen_c:c18_12(x), c6)
gen_0':s9_12(0) <=> 0'
gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x))
gen_c6:c710_12(0) <=> c6
gen_c6:c710_12(+(x, 1)) <=> c7(gen_c6:c710_12(x))
gen_c2:c311_12(0) <=> c2
gen_c2:c311_12(+(x, 1)) <=> c3(c, gen_c2:c311_12(x), c6)
gen_c4:c512_12(0) <=> c4
gen_c4:c512_12(+(x, 1)) <=> c5(c2, gen_c4:c512_12(x))
gen_c9:c10:c1113_12(0) <=> c9
gen_c9:c10:c1113_12(+(x, 1)) <=> c10(gen_c9:c10:c1113_12(x), c6)


The following defined symbols remain to be analysed:
p, PLUS, P, TIMES, times, EXP, exp, TOWERITER, plus, towerIter

They will be analysed ascendingly in the following order:
p < PLUS
P < PLUS
PLUS < TIMES
p < TIMES
p < times
p < TOWERITER
p < plus
p < towerIter
P < TIMES
P < TOWERITER
times < TIMES
TIMES < EXP
times < exp
plus < times
exp < EXP
EXP < TOWERITER
exp < TOWERITER
exp < towerIter

----------------------------------------

(9) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
p(gen_0':s9_12(+(1, n15_12))) -> gen_0':s9_12(n15_12), rt in Omega(0)

Induction Base:
p(gen_0':s9_12(+(1, 0))) ->_R^Omega(0)
0'

Induction Step:
p(gen_0':s9_12(+(1, +(n15_12, 1)))) ->_R^Omega(0)
s(p(s(gen_0':s9_12(n15_12)))) ->_IH
s(gen_0':s9_12(c16_12))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(10)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
P(s(0')) -> c6
P(s(s(z0))) -> c7(P(s(z0)))
TOWER(z0, z1) -> c8(TOWERITER(z0, z1, s(0')))
TOWERITER(0', z0, z1) -> c9
TOWERITER(s(z0), z1, z2) -> c10(TOWERITER(p(s(z0)), z1, exp(z1, z2)), P(s(z0)))
TOWERITER(s(z0), z1, z2) -> c11(TOWERITER(p(s(z0)), z1, exp(z1, z2)), EXP(z1, z2))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
tower(z0, z1) -> towerIter(z0, z1, s(0'))
towerIter(0', z0, z1) -> z1
towerIter(s(z0), z1, z2) -> towerIter(p(s(z0)), z1, exp(z1, z2))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c6:c7 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c6:c7
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c6:c7 -> c2:c3
times :: 0':s -> 0':s -> 0':s
EXP :: 0':s -> 0':s -> c4:c5
c4 :: c4:c5
c5 :: c2:c3 -> c4:c5 -> c4:c5
exp :: 0':s -> 0':s -> 0':s
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TOWER :: 0':s -> 0':s -> c8
c8 :: c9:c10:c11 -> c8
TOWERITER :: 0':s -> 0':s -> 0':s -> c9:c10:c11
c9 :: c9:c10:c11
c10 :: c9:c10:c11 -> c6:c7 -> c9:c10:c11
c11 :: c9:c10:c11 -> c4:c5 -> c9:c10:c11
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_12 :: c:c1
hole_0':s2_12 :: 0':s
hole_c6:c73_12 :: c6:c7
hole_c2:c34_12 :: c2:c3
hole_c4:c55_12 :: c4:c5
hole_c86_12 :: c8
hole_c9:c10:c117_12 :: c9:c10:c11
gen_c:c18_12 :: Nat -> c:c1
gen_0':s9_12 :: Nat -> 0':s
gen_c6:c710_12 :: Nat -> c6:c7
gen_c2:c311_12 :: Nat -> c2:c3
gen_c4:c512_12 :: Nat -> c4:c5
gen_c9:c10:c1113_12 :: Nat -> c9:c10:c11


Lemmas:
p(gen_0':s9_12(+(1, n15_12))) -> gen_0':s9_12(n15_12), rt in Omega(0)


Generator Equations:
gen_c:c18_12(0) <=> c
gen_c:c18_12(+(x, 1)) <=> c1(gen_c:c18_12(x), c6)
gen_0':s9_12(0) <=> 0'
gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x))
gen_c6:c710_12(0) <=> c6
gen_c6:c710_12(+(x, 1)) <=> c7(gen_c6:c710_12(x))
gen_c2:c311_12(0) <=> c2
gen_c2:c311_12(+(x, 1)) <=> c3(c, gen_c2:c311_12(x), c6)
gen_c4:c512_12(0) <=> c4
gen_c4:c512_12(+(x, 1)) <=> c5(c2, gen_c4:c512_12(x))
gen_c9:c10:c1113_12(0) <=> c9
gen_c9:c10:c1113_12(+(x, 1)) <=> c10(gen_c9:c10:c1113_12(x), c6)


The following defined symbols remain to be analysed:
P, PLUS, TIMES, times, EXP, exp, TOWERITER, plus, towerIter

They will be analysed ascendingly in the following order:
P < PLUS
PLUS < TIMES
P < TIMES
P < TOWERITER
times < TIMES
TIMES < EXP
times < exp
plus < times
exp < EXP
EXP < TOWERITER
exp < TOWERITER
exp < towerIter

----------------------------------------

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
P(gen_0':s9_12(+(1, n370_12))) -> gen_c6:c710_12(n370_12), rt in Omega(1 + n370_12)

Induction Base:
P(gen_0':s9_12(+(1, 0))) ->_R^Omega(1)
c6

Induction Step:
P(gen_0':s9_12(+(1, +(n370_12, 1)))) ->_R^Omega(1)
c7(P(s(gen_0':s9_12(n370_12)))) ->_IH
c7(gen_c6:c710_12(c371_12))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(12)
Complex Obligation (BEST)

----------------------------------------

(13)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
P(s(0')) -> c6
P(s(s(z0))) -> c7(P(s(z0)))
TOWER(z0, z1) -> c8(TOWERITER(z0, z1, s(0')))
TOWERITER(0', z0, z1) -> c9
TOWERITER(s(z0), z1, z2) -> c10(TOWERITER(p(s(z0)), z1, exp(z1, z2)), P(s(z0)))
TOWERITER(s(z0), z1, z2) -> c11(TOWERITER(p(s(z0)), z1, exp(z1, z2)), EXP(z1, z2))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
tower(z0, z1) -> towerIter(z0, z1, s(0'))
towerIter(0', z0, z1) -> z1
towerIter(s(z0), z1, z2) -> towerIter(p(s(z0)), z1, exp(z1, z2))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c6:c7 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c6:c7
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c6:c7 -> c2:c3
times :: 0':s -> 0':s -> 0':s
EXP :: 0':s -> 0':s -> c4:c5
c4 :: c4:c5
c5 :: c2:c3 -> c4:c5 -> c4:c5
exp :: 0':s -> 0':s -> 0':s
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TOWER :: 0':s -> 0':s -> c8
c8 :: c9:c10:c11 -> c8
TOWERITER :: 0':s -> 0':s -> 0':s -> c9:c10:c11
c9 :: c9:c10:c11
c10 :: c9:c10:c11 -> c6:c7 -> c9:c10:c11
c11 :: c9:c10:c11 -> c4:c5 -> c9:c10:c11
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_12 :: c:c1
hole_0':s2_12 :: 0':s
hole_c6:c73_12 :: c6:c7
hole_c2:c34_12 :: c2:c3
hole_c4:c55_12 :: c4:c5
hole_c86_12 :: c8
hole_c9:c10:c117_12 :: c9:c10:c11
gen_c:c18_12 :: Nat -> c:c1
gen_0':s9_12 :: Nat -> 0':s
gen_c6:c710_12 :: Nat -> c6:c7
gen_c2:c311_12 :: Nat -> c2:c3
gen_c4:c512_12 :: Nat -> c4:c5
gen_c9:c10:c1113_12 :: Nat -> c9:c10:c11


Lemmas:
p(gen_0':s9_12(+(1, n15_12))) -> gen_0':s9_12(n15_12), rt in Omega(0)


Generator Equations:
gen_c:c18_12(0) <=> c
gen_c:c18_12(+(x, 1)) <=> c1(gen_c:c18_12(x), c6)
gen_0':s9_12(0) <=> 0'
gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x))
gen_c6:c710_12(0) <=> c6
gen_c6:c710_12(+(x, 1)) <=> c7(gen_c6:c710_12(x))
gen_c2:c311_12(0) <=> c2
gen_c2:c311_12(+(x, 1)) <=> c3(c, gen_c2:c311_12(x), c6)
gen_c4:c512_12(0) <=> c4
gen_c4:c512_12(+(x, 1)) <=> c5(c2, gen_c4:c512_12(x))
gen_c9:c10:c1113_12(0) <=> c9
gen_c9:c10:c1113_12(+(x, 1)) <=> c10(gen_c9:c10:c1113_12(x), c6)


The following defined symbols remain to be analysed:
P, PLUS, TIMES, times, EXP, exp, TOWERITER, plus, towerIter

They will be analysed ascendingly in the following order:
P < PLUS
PLUS < TIMES
P < TIMES
P < TOWERITER
times < TIMES
TIMES < EXP
times < exp
plus < times
exp < EXP
EXP < TOWERITER
exp < TOWERITER
exp < towerIter

----------------------------------------

(14) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(15)
BOUNDS(n^1, INF)

----------------------------------------

(16)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
P(s(0')) -> c6
P(s(s(z0))) -> c7(P(s(z0)))
TOWER(z0, z1) -> c8(TOWERITER(z0, z1, s(0')))
TOWERITER(0', z0, z1) -> c9
TOWERITER(s(z0), z1, z2) -> c10(TOWERITER(p(s(z0)), z1, exp(z1, z2)), P(s(z0)))
TOWERITER(s(z0), z1, z2) -> c11(TOWERITER(p(s(z0)), z1, exp(z1, z2)), EXP(z1, z2))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
tower(z0, z1) -> towerIter(z0, z1, s(0'))
towerIter(0', z0, z1) -> z1
towerIter(s(z0), z1, z2) -> towerIter(p(s(z0)), z1, exp(z1, z2))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c6:c7 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c6:c7
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c6:c7 -> c2:c3
times :: 0':s -> 0':s -> 0':s
EXP :: 0':s -> 0':s -> c4:c5
c4 :: c4:c5
c5 :: c2:c3 -> c4:c5 -> c4:c5
exp :: 0':s -> 0':s -> 0':s
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TOWER :: 0':s -> 0':s -> c8
c8 :: c9:c10:c11 -> c8
TOWERITER :: 0':s -> 0':s -> 0':s -> c9:c10:c11
c9 :: c9:c10:c11
c10 :: c9:c10:c11 -> c6:c7 -> c9:c10:c11
c11 :: c9:c10:c11 -> c4:c5 -> c9:c10:c11
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_12 :: c:c1
hole_0':s2_12 :: 0':s
hole_c6:c73_12 :: c6:c7
hole_c2:c34_12 :: c2:c3
hole_c4:c55_12 :: c4:c5
hole_c86_12 :: c8
hole_c9:c10:c117_12 :: c9:c10:c11
gen_c:c18_12 :: Nat -> c:c1
gen_0':s9_12 :: Nat -> 0':s
gen_c6:c710_12 :: Nat -> c6:c7
gen_c2:c311_12 :: Nat -> c2:c3
gen_c4:c512_12 :: Nat -> c4:c5
gen_c9:c10:c1113_12 :: Nat -> c9:c10:c11


Lemmas:
p(gen_0':s9_12(+(1, n15_12))) -> gen_0':s9_12(n15_12), rt in Omega(0)
P(gen_0':s9_12(+(1, n370_12))) -> gen_c6:c710_12(n370_12), rt in Omega(1 + n370_12)


Generator Equations:
gen_c:c18_12(0) <=> c
gen_c:c18_12(+(x, 1)) <=> c1(gen_c:c18_12(x), c6)
gen_0':s9_12(0) <=> 0'
gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x))
gen_c6:c710_12(0) <=> c6
gen_c6:c710_12(+(x, 1)) <=> c7(gen_c6:c710_12(x))
gen_c2:c311_12(0) <=> c2
gen_c2:c311_12(+(x, 1)) <=> c3(c, gen_c2:c311_12(x), c6)
gen_c4:c512_12(0) <=> c4
gen_c4:c512_12(+(x, 1)) <=> c5(c2, gen_c4:c512_12(x))
gen_c9:c10:c1113_12(0) <=> c9
gen_c9:c10:c1113_12(+(x, 1)) <=> c10(gen_c9:c10:c1113_12(x), c6)


The following defined symbols remain to be analysed:
PLUS, TIMES, times, EXP, exp, TOWERITER, plus, towerIter

They will be analysed ascendingly in the following order:
PLUS < TIMES
times < TIMES
TIMES < EXP
times < exp
plus < times
exp < EXP
EXP < TOWERITER
exp < TOWERITER
exp < towerIter

----------------------------------------

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
PLUS(gen_0':s9_12(n754_12), gen_0':s9_12(b)) -> *14_12, rt in Omega(n754_12 + n754_12^2)

Induction Base:
PLUS(gen_0':s9_12(0), gen_0':s9_12(b))

Induction Step:
PLUS(gen_0':s9_12(+(n754_12, 1)), gen_0':s9_12(b)) ->_R^Omega(1)
c1(PLUS(p(s(gen_0':s9_12(n754_12))), gen_0':s9_12(b)), P(s(gen_0':s9_12(n754_12)))) ->_L^Omega(0)
c1(PLUS(gen_0':s9_12(n754_12), gen_0':s9_12(b)), P(s(gen_0':s9_12(n754_12)))) ->_IH
c1(*14_12, P(s(gen_0':s9_12(n754_12)))) ->_L^Omega(1 + n754_12)
c1(*14_12, gen_c6:c710_12(n754_12))

We have rt in Omega(n^2) and sz in O(n). Thus, we have irc_R in Omega(n^2).
----------------------------------------

(18)
Complex Obligation (BEST)

----------------------------------------

(19)
Obligation:
Proved the lower bound n^2 for the following obligation:

Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
P(s(0')) -> c6
P(s(s(z0))) -> c7(P(s(z0)))
TOWER(z0, z1) -> c8(TOWERITER(z0, z1, s(0')))
TOWERITER(0', z0, z1) -> c9
TOWERITER(s(z0), z1, z2) -> c10(TOWERITER(p(s(z0)), z1, exp(z1, z2)), P(s(z0)))
TOWERITER(s(z0), z1, z2) -> c11(TOWERITER(p(s(z0)), z1, exp(z1, z2)), EXP(z1, z2))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
tower(z0, z1) -> towerIter(z0, z1, s(0'))
towerIter(0', z0, z1) -> z1
towerIter(s(z0), z1, z2) -> towerIter(p(s(z0)), z1, exp(z1, z2))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c6:c7 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c6:c7
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c6:c7 -> c2:c3
times :: 0':s -> 0':s -> 0':s
EXP :: 0':s -> 0':s -> c4:c5
c4 :: c4:c5
c5 :: c2:c3 -> c4:c5 -> c4:c5
exp :: 0':s -> 0':s -> 0':s
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TOWER :: 0':s -> 0':s -> c8
c8 :: c9:c10:c11 -> c8
TOWERITER :: 0':s -> 0':s -> 0':s -> c9:c10:c11
c9 :: c9:c10:c11
c10 :: c9:c10:c11 -> c6:c7 -> c9:c10:c11
c11 :: c9:c10:c11 -> c4:c5 -> c9:c10:c11
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_12 :: c:c1
hole_0':s2_12 :: 0':s
hole_c6:c73_12 :: c6:c7
hole_c2:c34_12 :: c2:c3
hole_c4:c55_12 :: c4:c5
hole_c86_12 :: c8
hole_c9:c10:c117_12 :: c9:c10:c11
gen_c:c18_12 :: Nat -> c:c1
gen_0':s9_12 :: Nat -> 0':s
gen_c6:c710_12 :: Nat -> c6:c7
gen_c2:c311_12 :: Nat -> c2:c3
gen_c4:c512_12 :: Nat -> c4:c5
gen_c9:c10:c1113_12 :: Nat -> c9:c10:c11


Lemmas:
p(gen_0':s9_12(+(1, n15_12))) -> gen_0':s9_12(n15_12), rt in Omega(0)
P(gen_0':s9_12(+(1, n370_12))) -> gen_c6:c710_12(n370_12), rt in Omega(1 + n370_12)


Generator Equations:
gen_c:c18_12(0) <=> c
gen_c:c18_12(+(x, 1)) <=> c1(gen_c:c18_12(x), c6)
gen_0':s9_12(0) <=> 0'
gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x))
gen_c6:c710_12(0) <=> c6
gen_c6:c710_12(+(x, 1)) <=> c7(gen_c6:c710_12(x))
gen_c2:c311_12(0) <=> c2
gen_c2:c311_12(+(x, 1)) <=> c3(c, gen_c2:c311_12(x), c6)
gen_c4:c512_12(0) <=> c4
gen_c4:c512_12(+(x, 1)) <=> c5(c2, gen_c4:c512_12(x))
gen_c9:c10:c1113_12(0) <=> c9
gen_c9:c10:c1113_12(+(x, 1)) <=> c10(gen_c9:c10:c1113_12(x), c6)


The following defined symbols remain to be analysed:
PLUS, TIMES, times, EXP, exp, TOWERITER, plus, towerIter

They will be analysed ascendingly in the following order:
PLUS < TIMES
times < TIMES
TIMES < EXP
times < exp
plus < times
exp < EXP
EXP < TOWERITER
exp < TOWERITER
exp < towerIter

----------------------------------------

(20) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(21)
BOUNDS(n^2, INF)

----------------------------------------

(22)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
P(s(0')) -> c6
P(s(s(z0))) -> c7(P(s(z0)))
TOWER(z0, z1) -> c8(TOWERITER(z0, z1, s(0')))
TOWERITER(0', z0, z1) -> c9
TOWERITER(s(z0), z1, z2) -> c10(TOWERITER(p(s(z0)), z1, exp(z1, z2)), P(s(z0)))
TOWERITER(s(z0), z1, z2) -> c11(TOWERITER(p(s(z0)), z1, exp(z1, z2)), EXP(z1, z2))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
tower(z0, z1) -> towerIter(z0, z1, s(0'))
towerIter(0', z0, z1) -> z1
towerIter(s(z0), z1, z2) -> towerIter(p(s(z0)), z1, exp(z1, z2))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c6:c7 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c6:c7
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c6:c7 -> c2:c3
times :: 0':s -> 0':s -> 0':s
EXP :: 0':s -> 0':s -> c4:c5
c4 :: c4:c5
c5 :: c2:c3 -> c4:c5 -> c4:c5
exp :: 0':s -> 0':s -> 0':s
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TOWER :: 0':s -> 0':s -> c8
c8 :: c9:c10:c11 -> c8
TOWERITER :: 0':s -> 0':s -> 0':s -> c9:c10:c11
c9 :: c9:c10:c11
c10 :: c9:c10:c11 -> c6:c7 -> c9:c10:c11
c11 :: c9:c10:c11 -> c4:c5 -> c9:c10:c11
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_12 :: c:c1
hole_0':s2_12 :: 0':s
hole_c6:c73_12 :: c6:c7
hole_c2:c34_12 :: c2:c3
hole_c4:c55_12 :: c4:c5
hole_c86_12 :: c8
hole_c9:c10:c117_12 :: c9:c10:c11
gen_c:c18_12 :: Nat -> c:c1
gen_0':s9_12 :: Nat -> 0':s
gen_c6:c710_12 :: Nat -> c6:c7
gen_c2:c311_12 :: Nat -> c2:c3
gen_c4:c512_12 :: Nat -> c4:c5
gen_c9:c10:c1113_12 :: Nat -> c9:c10:c11


Lemmas:
p(gen_0':s9_12(+(1, n15_12))) -> gen_0':s9_12(n15_12), rt in Omega(0)
P(gen_0':s9_12(+(1, n370_12))) -> gen_c6:c710_12(n370_12), rt in Omega(1 + n370_12)
PLUS(gen_0':s9_12(n754_12), gen_0':s9_12(b)) -> *14_12, rt in Omega(n754_12 + n754_12^2)


Generator Equations:
gen_c:c18_12(0) <=> c
gen_c:c18_12(+(x, 1)) <=> c1(gen_c:c18_12(x), c6)
gen_0':s9_12(0) <=> 0'
gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x))
gen_c6:c710_12(0) <=> c6
gen_c6:c710_12(+(x, 1)) <=> c7(gen_c6:c710_12(x))
gen_c2:c311_12(0) <=> c2
gen_c2:c311_12(+(x, 1)) <=> c3(c, gen_c2:c311_12(x), c6)
gen_c4:c512_12(0) <=> c4
gen_c4:c512_12(+(x, 1)) <=> c5(c2, gen_c4:c512_12(x))
gen_c9:c10:c1113_12(0) <=> c9
gen_c9:c10:c1113_12(+(x, 1)) <=> c10(gen_c9:c10:c1113_12(x), c6)


The following defined symbols remain to be analysed:
plus, TIMES, times, EXP, exp, TOWERITER, towerIter

They will be analysed ascendingly in the following order:
times < TIMES
TIMES < EXP
times < exp
plus < times
exp < EXP
EXP < TOWERITER
exp < TOWERITER
exp < towerIter

----------------------------------------

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
plus(gen_0':s9_12(n10768_12), gen_0':s9_12(b)) -> gen_0':s9_12(+(n10768_12, b)), rt in Omega(0)

Induction Base:
plus(gen_0':s9_12(0), gen_0':s9_12(b)) ->_R^Omega(0)
gen_0':s9_12(b)

Induction Step:
plus(gen_0':s9_12(+(n10768_12, 1)), gen_0':s9_12(b)) ->_R^Omega(0)
s(plus(p(s(gen_0':s9_12(n10768_12))), gen_0':s9_12(b))) ->_L^Omega(0)
s(plus(gen_0':s9_12(n10768_12), gen_0':s9_12(b))) ->_IH
s(gen_0':s9_12(+(b, c10769_12)))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(24)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
P(s(0')) -> c6
P(s(s(z0))) -> c7(P(s(z0)))
TOWER(z0, z1) -> c8(TOWERITER(z0, z1, s(0')))
TOWERITER(0', z0, z1) -> c9
TOWERITER(s(z0), z1, z2) -> c10(TOWERITER(p(s(z0)), z1, exp(z1, z2)), P(s(z0)))
TOWERITER(s(z0), z1, z2) -> c11(TOWERITER(p(s(z0)), z1, exp(z1, z2)), EXP(z1, z2))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
tower(z0, z1) -> towerIter(z0, z1, s(0'))
towerIter(0', z0, z1) -> z1
towerIter(s(z0), z1, z2) -> towerIter(p(s(z0)), z1, exp(z1, z2))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c6:c7 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c6:c7
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c6:c7 -> c2:c3
times :: 0':s -> 0':s -> 0':s
EXP :: 0':s -> 0':s -> c4:c5
c4 :: c4:c5
c5 :: c2:c3 -> c4:c5 -> c4:c5
exp :: 0':s -> 0':s -> 0':s
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TOWER :: 0':s -> 0':s -> c8
c8 :: c9:c10:c11 -> c8
TOWERITER :: 0':s -> 0':s -> 0':s -> c9:c10:c11
c9 :: c9:c10:c11
c10 :: c9:c10:c11 -> c6:c7 -> c9:c10:c11
c11 :: c9:c10:c11 -> c4:c5 -> c9:c10:c11
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_12 :: c:c1
hole_0':s2_12 :: 0':s
hole_c6:c73_12 :: c6:c7
hole_c2:c34_12 :: c2:c3
hole_c4:c55_12 :: c4:c5
hole_c86_12 :: c8
hole_c9:c10:c117_12 :: c9:c10:c11
gen_c:c18_12 :: Nat -> c:c1
gen_0':s9_12 :: Nat -> 0':s
gen_c6:c710_12 :: Nat -> c6:c7
gen_c2:c311_12 :: Nat -> c2:c3
gen_c4:c512_12 :: Nat -> c4:c5
gen_c9:c10:c1113_12 :: Nat -> c9:c10:c11


Lemmas:
p(gen_0':s9_12(+(1, n15_12))) -> gen_0':s9_12(n15_12), rt in Omega(0)
P(gen_0':s9_12(+(1, n370_12))) -> gen_c6:c710_12(n370_12), rt in Omega(1 + n370_12)
PLUS(gen_0':s9_12(n754_12), gen_0':s9_12(b)) -> *14_12, rt in Omega(n754_12 + n754_12^2)
plus(gen_0':s9_12(n10768_12), gen_0':s9_12(b)) -> gen_0':s9_12(+(n10768_12, b)), rt in Omega(0)


Generator Equations:
gen_c:c18_12(0) <=> c
gen_c:c18_12(+(x, 1)) <=> c1(gen_c:c18_12(x), c6)
gen_0':s9_12(0) <=> 0'
gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x))
gen_c6:c710_12(0) <=> c6
gen_c6:c710_12(+(x, 1)) <=> c7(gen_c6:c710_12(x))
gen_c2:c311_12(0) <=> c2
gen_c2:c311_12(+(x, 1)) <=> c3(c, gen_c2:c311_12(x), c6)
gen_c4:c512_12(0) <=> c4
gen_c4:c512_12(+(x, 1)) <=> c5(c2, gen_c4:c512_12(x))
gen_c9:c10:c1113_12(0) <=> c9
gen_c9:c10:c1113_12(+(x, 1)) <=> c10(gen_c9:c10:c1113_12(x), c6)


The following defined symbols remain to be analysed:
times, TIMES, EXP, exp, TOWERITER, towerIter

They will be analysed ascendingly in the following order:
times < TIMES
TIMES < EXP
times < exp
exp < EXP
EXP < TOWERITER
exp < TOWERITER
exp < towerIter

----------------------------------------

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
times(gen_0':s9_12(n12029_12), gen_0':s9_12(b)) -> gen_0':s9_12(*(n12029_12, b)), rt in Omega(0)

Induction Base:
times(gen_0':s9_12(0), gen_0':s9_12(b)) ->_R^Omega(0)
0'

Induction Step:
times(gen_0':s9_12(+(n12029_12, 1)), gen_0':s9_12(b)) ->_R^Omega(0)
plus(gen_0':s9_12(b), times(p(s(gen_0':s9_12(n12029_12))), gen_0':s9_12(b))) ->_L^Omega(0)
plus(gen_0':s9_12(b), times(gen_0':s9_12(n12029_12), gen_0':s9_12(b))) ->_IH
plus(gen_0':s9_12(b), gen_0':s9_12(*(c12030_12, b))) ->_L^Omega(0)
gen_0':s9_12(+(b, *(n12029_12, b)))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(26)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
P(s(0')) -> c6
P(s(s(z0))) -> c7(P(s(z0)))
TOWER(z0, z1) -> c8(TOWERITER(z0, z1, s(0')))
TOWERITER(0', z0, z1) -> c9
TOWERITER(s(z0), z1, z2) -> c10(TOWERITER(p(s(z0)), z1, exp(z1, z2)), P(s(z0)))
TOWERITER(s(z0), z1, z2) -> c11(TOWERITER(p(s(z0)), z1, exp(z1, z2)), EXP(z1, z2))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
tower(z0, z1) -> towerIter(z0, z1, s(0'))
towerIter(0', z0, z1) -> z1
towerIter(s(z0), z1, z2) -> towerIter(p(s(z0)), z1, exp(z1, z2))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c6:c7 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c6:c7
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c6:c7 -> c2:c3
times :: 0':s -> 0':s -> 0':s
EXP :: 0':s -> 0':s -> c4:c5
c4 :: c4:c5
c5 :: c2:c3 -> c4:c5 -> c4:c5
exp :: 0':s -> 0':s -> 0':s
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TOWER :: 0':s -> 0':s -> c8
c8 :: c9:c10:c11 -> c8
TOWERITER :: 0':s -> 0':s -> 0':s -> c9:c10:c11
c9 :: c9:c10:c11
c10 :: c9:c10:c11 -> c6:c7 -> c9:c10:c11
c11 :: c9:c10:c11 -> c4:c5 -> c9:c10:c11
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_12 :: c:c1
hole_0':s2_12 :: 0':s
hole_c6:c73_12 :: c6:c7
hole_c2:c34_12 :: c2:c3
hole_c4:c55_12 :: c4:c5
hole_c86_12 :: c8
hole_c9:c10:c117_12 :: c9:c10:c11
gen_c:c18_12 :: Nat -> c:c1
gen_0':s9_12 :: Nat -> 0':s
gen_c6:c710_12 :: Nat -> c6:c7
gen_c2:c311_12 :: Nat -> c2:c3
gen_c4:c512_12 :: Nat -> c4:c5
gen_c9:c10:c1113_12 :: Nat -> c9:c10:c11


Lemmas:
p(gen_0':s9_12(+(1, n15_12))) -> gen_0':s9_12(n15_12), rt in Omega(0)
P(gen_0':s9_12(+(1, n370_12))) -> gen_c6:c710_12(n370_12), rt in Omega(1 + n370_12)
PLUS(gen_0':s9_12(n754_12), gen_0':s9_12(b)) -> *14_12, rt in Omega(n754_12 + n754_12^2)
plus(gen_0':s9_12(n10768_12), gen_0':s9_12(b)) -> gen_0':s9_12(+(n10768_12, b)), rt in Omega(0)
times(gen_0':s9_12(n12029_12), gen_0':s9_12(b)) -> gen_0':s9_12(*(n12029_12, b)), rt in Omega(0)


Generator Equations:
gen_c:c18_12(0) <=> c
gen_c:c18_12(+(x, 1)) <=> c1(gen_c:c18_12(x), c6)
gen_0':s9_12(0) <=> 0'
gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x))
gen_c6:c710_12(0) <=> c6
gen_c6:c710_12(+(x, 1)) <=> c7(gen_c6:c710_12(x))
gen_c2:c311_12(0) <=> c2
gen_c2:c311_12(+(x, 1)) <=> c3(c, gen_c2:c311_12(x), c6)
gen_c4:c512_12(0) <=> c4
gen_c4:c512_12(+(x, 1)) <=> c5(c2, gen_c4:c512_12(x))
gen_c9:c10:c1113_12(0) <=> c9
gen_c9:c10:c1113_12(+(x, 1)) <=> c10(gen_c9:c10:c1113_12(x), c6)


The following defined symbols remain to be analysed:
TIMES, EXP, exp, TOWERITER, towerIter

They will be analysed ascendingly in the following order:
TIMES < EXP
exp < EXP
EXP < TOWERITER
exp < TOWERITER
exp < towerIter

----------------------------------------

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
TIMES(gen_0':s9_12(n14119_12), gen_0':s9_12(0)) -> *14_12, rt in Omega(n14119_12 + n14119_12^2)

Induction Base:
TIMES(gen_0':s9_12(0), gen_0':s9_12(0))

Induction Step:
TIMES(gen_0':s9_12(+(n14119_12, 1)), gen_0':s9_12(0)) ->_R^Omega(1)
c3(PLUS(gen_0':s9_12(0), times(p(s(gen_0':s9_12(n14119_12))), gen_0':s9_12(0))), TIMES(p(s(gen_0':s9_12(n14119_12))), gen_0':s9_12(0)), P(s(gen_0':s9_12(n14119_12)))) ->_L^Omega(0)
c3(PLUS(gen_0':s9_12(0), times(gen_0':s9_12(n14119_12), gen_0':s9_12(0))), TIMES(p(s(gen_0':s9_12(n14119_12))), gen_0':s9_12(0)), P(s(gen_0':s9_12(n14119_12)))) ->_L^Omega(0)
c3(PLUS(gen_0':s9_12(0), gen_0':s9_12(*(n14119_12, 0))), TIMES(p(s(gen_0':s9_12(n14119_12))), gen_0':s9_12(0)), P(s(gen_0':s9_12(n14119_12)))) ->_R^Omega(1)
c3(c, TIMES(p(s(gen_0':s9_12(n14119_12))), gen_0':s9_12(0)), P(s(gen_0':s9_12(n14119_12)))) ->_L^Omega(0)
c3(c, TIMES(gen_0':s9_12(n14119_12), gen_0':s9_12(0)), P(s(gen_0':s9_12(n14119_12)))) ->_IH
c3(c, *14_12, P(s(gen_0':s9_12(n14119_12)))) ->_L^Omega(1 + n14119_12)
c3(c, *14_12, gen_c6:c710_12(n14119_12))

We have rt in Omega(n^2) and sz in O(n). Thus, we have irc_R in Omega(n^2).
----------------------------------------

(28)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
P(s(0')) -> c6
P(s(s(z0))) -> c7(P(s(z0)))
TOWER(z0, z1) -> c8(TOWERITER(z0, z1, s(0')))
TOWERITER(0', z0, z1) -> c9
TOWERITER(s(z0), z1, z2) -> c10(TOWERITER(p(s(z0)), z1, exp(z1, z2)), P(s(z0)))
TOWERITER(s(z0), z1, z2) -> c11(TOWERITER(p(s(z0)), z1, exp(z1, z2)), EXP(z1, z2))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
tower(z0, z1) -> towerIter(z0, z1, s(0'))
towerIter(0', z0, z1) -> z1
towerIter(s(z0), z1, z2) -> towerIter(p(s(z0)), z1, exp(z1, z2))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c6:c7 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c6:c7
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c6:c7 -> c2:c3
times :: 0':s -> 0':s -> 0':s
EXP :: 0':s -> 0':s -> c4:c5
c4 :: c4:c5
c5 :: c2:c3 -> c4:c5 -> c4:c5
exp :: 0':s -> 0':s -> 0':s
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TOWER :: 0':s -> 0':s -> c8
c8 :: c9:c10:c11 -> c8
TOWERITER :: 0':s -> 0':s -> 0':s -> c9:c10:c11
c9 :: c9:c10:c11
c10 :: c9:c10:c11 -> c6:c7 -> c9:c10:c11
c11 :: c9:c10:c11 -> c4:c5 -> c9:c10:c11
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_12 :: c:c1
hole_0':s2_12 :: 0':s
hole_c6:c73_12 :: c6:c7
hole_c2:c34_12 :: c2:c3
hole_c4:c55_12 :: c4:c5
hole_c86_12 :: c8
hole_c9:c10:c117_12 :: c9:c10:c11
gen_c:c18_12 :: Nat -> c:c1
gen_0':s9_12 :: Nat -> 0':s
gen_c6:c710_12 :: Nat -> c6:c7
gen_c2:c311_12 :: Nat -> c2:c3
gen_c4:c512_12 :: Nat -> c4:c5
gen_c9:c10:c1113_12 :: Nat -> c9:c10:c11


Lemmas:
p(gen_0':s9_12(+(1, n15_12))) -> gen_0':s9_12(n15_12), rt in Omega(0)
P(gen_0':s9_12(+(1, n370_12))) -> gen_c6:c710_12(n370_12), rt in Omega(1 + n370_12)
PLUS(gen_0':s9_12(n754_12), gen_0':s9_12(b)) -> *14_12, rt in Omega(n754_12 + n754_12^2)
plus(gen_0':s9_12(n10768_12), gen_0':s9_12(b)) -> gen_0':s9_12(+(n10768_12, b)), rt in Omega(0)
times(gen_0':s9_12(n12029_12), gen_0':s9_12(b)) -> gen_0':s9_12(*(n12029_12, b)), rt in Omega(0)
TIMES(gen_0':s9_12(n14119_12), gen_0':s9_12(0)) -> *14_12, rt in Omega(n14119_12 + n14119_12^2)


Generator Equations:
gen_c:c18_12(0) <=> c
gen_c:c18_12(+(x, 1)) <=> c1(gen_c:c18_12(x), c6)
gen_0':s9_12(0) <=> 0'
gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x))
gen_c6:c710_12(0) <=> c6
gen_c6:c710_12(+(x, 1)) <=> c7(gen_c6:c710_12(x))
gen_c2:c311_12(0) <=> c2
gen_c2:c311_12(+(x, 1)) <=> c3(c, gen_c2:c311_12(x), c6)
gen_c4:c512_12(0) <=> c4
gen_c4:c512_12(+(x, 1)) <=> c5(c2, gen_c4:c512_12(x))
gen_c9:c10:c1113_12(0) <=> c9
gen_c9:c10:c1113_12(+(x, 1)) <=> c10(gen_c9:c10:c1113_12(x), c6)


The following defined symbols remain to be analysed:
exp, EXP, TOWERITER, towerIter

They will be analysed ascendingly in the following order:
exp < EXP
EXP < TOWERITER
exp < TOWERITER
exp < towerIter

----------------------------------------

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
exp(gen_0':s9_12(a), gen_0':s9_12(+(1, n36334_12))) -> *14_12, rt in Omega(0)

Induction Base:
exp(gen_0':s9_12(a), gen_0':s9_12(+(1, 0)))

Induction Step:
exp(gen_0':s9_12(a), gen_0':s9_12(+(1, +(n36334_12, 1)))) ->_R^Omega(0)
times(gen_0':s9_12(a), exp(gen_0':s9_12(a), gen_0':s9_12(+(1, n36334_12)))) ->_IH
times(gen_0':s9_12(a), *14_12)

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(30)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(p(s(z0)), z1), P(s(z0)))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(p(s(z0)), z1)), TIMES(p(s(z0)), z1), P(s(z0)))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
P(s(0')) -> c6
P(s(s(z0))) -> c7(P(s(z0)))
TOWER(z0, z1) -> c8(TOWERITER(z0, z1, s(0')))
TOWERITER(0', z0, z1) -> c9
TOWERITER(s(z0), z1, z2) -> c10(TOWERITER(p(s(z0)), z1, exp(z1, z2)), P(s(z0)))
TOWERITER(s(z0), z1, z2) -> c11(TOWERITER(p(s(z0)), z1, exp(z1, z2)), EXP(z1, z2))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(p(s(z0)), z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(p(s(z0)), z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
tower(z0, z1) -> towerIter(z0, z1, s(0'))
towerIter(0', z0, z1) -> z1
towerIter(s(z0), z1, z2) -> towerIter(p(s(z0)), z1, exp(z1, z2))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c6:c7 -> c:c1
p :: 0':s -> 0':s
P :: 0':s -> c6:c7
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> c6:c7 -> c2:c3
times :: 0':s -> 0':s -> 0':s
EXP :: 0':s -> 0':s -> c4:c5
c4 :: c4:c5
c5 :: c2:c3 -> c4:c5 -> c4:c5
exp :: 0':s -> 0':s -> 0':s
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
TOWER :: 0':s -> 0':s -> c8
c8 :: c9:c10:c11 -> c8
TOWERITER :: 0':s -> 0':s -> 0':s -> c9:c10:c11
c9 :: c9:c10:c11
c10 :: c9:c10:c11 -> c6:c7 -> c9:c10:c11
c11 :: c9:c10:c11 -> c4:c5 -> c9:c10:c11
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_12 :: c:c1
hole_0':s2_12 :: 0':s
hole_c6:c73_12 :: c6:c7
hole_c2:c34_12 :: c2:c3
hole_c4:c55_12 :: c4:c5
hole_c86_12 :: c8
hole_c9:c10:c117_12 :: c9:c10:c11
gen_c:c18_12 :: Nat -> c:c1
gen_0':s9_12 :: Nat -> 0':s
gen_c6:c710_12 :: Nat -> c6:c7
gen_c2:c311_12 :: Nat -> c2:c3
gen_c4:c512_12 :: Nat -> c4:c5
gen_c9:c10:c1113_12 :: Nat -> c9:c10:c11


Lemmas:
p(gen_0':s9_12(+(1, n15_12))) -> gen_0':s9_12(n15_12), rt in Omega(0)
P(gen_0':s9_12(+(1, n370_12))) -> gen_c6:c710_12(n370_12), rt in Omega(1 + n370_12)
PLUS(gen_0':s9_12(n754_12), gen_0':s9_12(b)) -> *14_12, rt in Omega(n754_12 + n754_12^2)
plus(gen_0':s9_12(n10768_12), gen_0':s9_12(b)) -> gen_0':s9_12(+(n10768_12, b)), rt in Omega(0)
times(gen_0':s9_12(n12029_12), gen_0':s9_12(b)) -> gen_0':s9_12(*(n12029_12, b)), rt in Omega(0)
TIMES(gen_0':s9_12(n14119_12), gen_0':s9_12(0)) -> *14_12, rt in Omega(n14119_12 + n14119_12^2)
exp(gen_0':s9_12(a), gen_0':s9_12(+(1, n36334_12))) -> *14_12, rt in Omega(0)


Generator Equations:
gen_c:c18_12(0) <=> c
gen_c:c18_12(+(x, 1)) <=> c1(gen_c:c18_12(x), c6)
gen_0':s9_12(0) <=> 0'
gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x))
gen_c6:c710_12(0) <=> c6
gen_c6:c710_12(+(x, 1)) <=> c7(gen_c6:c710_12(x))
gen_c2:c311_12(0) <=> c2
gen_c2:c311_12(+(x, 1)) <=> c3(c, gen_c2:c311_12(x), c6)
gen_c4:c512_12(0) <=> c4
gen_c4:c512_12(+(x, 1)) <=> c5(c2, gen_c4:c512_12(x))
gen_c9:c10:c1113_12(0) <=> c9
gen_c9:c10:c1113_12(+(x, 1)) <=> c10(gen_c9:c10:c1113_12(x), c6)


The following defined symbols remain to be analysed:
EXP, TOWERITER, towerIter

They will be analysed ascendingly in the following order:
EXP < TOWERITER