WORST_CASE(Omega(n^2),?)
proof of input_8kOARbC0fp.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 5 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 287 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), 91 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 25 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 44 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 88 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 752 ms]
        (26) BEST
            (27) proven lower bound
                (28) LowerBoundPropagationProof [FINISHED, 0 ms]
                (29) BOUNDS(n^2, INF)
            (30) typed CpxTrs
                (31) RewriteLemmaProof [LOWER BOUND(ID), 960 ms]
                (32) typed CpxTrs


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

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


The TRS R consists of the following rules:

   plus(0, x) -> x
   plus(s(x), y) -> s(plus(x, y))
   times(0, y) -> 0
   times(s(x), y) -> plus(y, times(x, y))
   exp(x, 0) -> s(0)
   exp(x, s(y)) -> times(x, exp(x, y))
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   tower(x, y) -> towerIter(0, x, y, s(0))
   towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z)
   help(true, c, x, y, z) -> z
   help(false, c, x, y, z) -> towerIter(s(c), x, y, exp(y, z))

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   plus(0, z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   times(0, z0) -> 0
   times(s(z0), z1) -> plus(z1, times(z0, z1))
   exp(z0, 0) -> s(0)
   exp(z0, s(z1)) -> times(z0, exp(z0, z1))
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   tower(z0, z1) -> towerIter(0, z0, z1, s(0))
   towerIter(z0, z1, z2, z3) -> help(ge(z0, z1), z0, z1, z2, z3)
   help(true, z0, z1, z2, z3) -> z3
   help(false, z0, z1, z2, z3) -> towerIter(s(z0), z1, z2, exp(z2, z3))
Tuples:
   PLUS(0, z0) -> c
   PLUS(s(z0), z1) -> c1(PLUS(z0, z1))
   TIMES(0, z0) -> c2
   TIMES(s(z0), z1) -> c3(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   EXP(z0, 0) -> c4
   EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
   GE(z0, 0) -> c6
   GE(0, s(z0)) -> c7
   GE(s(z0), s(z1)) -> c8(GE(z0, z1))
   TOWER(z0, z1) -> c9(TOWERITER(0, z0, z1, s(0)))
   TOWERITER(z0, z1, z2, z3) -> c10(HELP(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   HELP(true, z0, z1, z2, z3) -> c11
   HELP(false, z0, z1, z2, z3) -> c12(TOWERITER(s(z0), z1, z2, exp(z2, z3)), EXP(z2, z3))
S tuples:
   PLUS(0, z0) -> c
   PLUS(s(z0), z1) -> c1(PLUS(z0, z1))
   TIMES(0, z0) -> c2
   TIMES(s(z0), z1) -> c3(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   EXP(z0, 0) -> c4
   EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
   GE(z0, 0) -> c6
   GE(0, s(z0)) -> c7
   GE(s(z0), s(z1)) -> c8(GE(z0, z1))
   TOWER(z0, z1) -> c9(TOWERITER(0, z0, z1, s(0)))
   TOWERITER(z0, z1, z2, z3) -> c10(HELP(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   HELP(true, z0, z1, z2, z3) -> c11
   HELP(false, z0, z1, z2, z3) -> c12(TOWERITER(s(z0), z1, z2, exp(z2, z3)), EXP(z2, z3))
K tuples:none
Defined Rule Symbols:   plus_2, times_2, exp_2, ge_2, tower_2, towerIter_4, help_5

Defined Pair Symbols:   PLUS_2, TIMES_2, EXP_2, GE_2, TOWER_2, TOWERITER_4, HELP_5

Compound Symbols:   c, c1_1, c2, c3_2, c4, c5_2, c6, c7, c8_1, c9_1, c10_2, c11, c12_2


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

(3) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

(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(z0, z1))
   TIMES(0, z0) -> c2
   TIMES(s(z0), z1) -> c3(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   EXP(z0, 0) -> c4
   EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
   GE(z0, 0) -> c6
   GE(0, s(z0)) -> c7
   GE(s(z0), s(z1)) -> c8(GE(z0, z1))
   TOWER(z0, z1) -> c9(TOWERITER(0, z0, z1, s(0)))
   TOWERITER(z0, z1, z2, z3) -> c10(HELP(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   HELP(true, z0, z1, z2, z3) -> c11
   HELP(false, z0, z1, z2, z3) -> c12(TOWERITER(s(z0), z1, z2, exp(z2, z3)), EXP(z2, z3))

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

   plus(0, z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   times(0, z0) -> 0
   times(s(z0), z1) -> plus(z1, times(z0, z1))
   exp(z0, 0) -> s(0)
   exp(z0, s(z1)) -> times(z0, exp(z0, z1))
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   tower(z0, z1) -> towerIter(0, z0, z1, s(0))
   towerIter(z0, z1, z2, z3) -> help(ge(z0, z1), z0, z1, z2, z3)
   help(true, z0, z1, z2, z3) -> z3
   help(false, z0, z1, z2, z3) -> towerIter(s(z0), z1, z2, exp(z2, z3))

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

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

(6)
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(z0, z1))
   TIMES(0', z0) -> c2
   TIMES(s(z0), z1) -> c3(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   EXP(z0, 0') -> c4
   EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
   GE(z0, 0') -> c6
   GE(0', s(z0)) -> c7
   GE(s(z0), s(z1)) -> c8(GE(z0, z1))
   TOWER(z0, z1) -> c9(TOWERITER(0', z0, z1, s(0')))
   TOWERITER(z0, z1, z2, z3) -> c10(HELP(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   HELP(true, z0, z1, z2, z3) -> c11
   HELP(false, z0, z1, z2, z3) -> c12(TOWERITER(s(z0), z1, z2, exp(z2, z3)), EXP(z2, z3))

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

   plus(0', z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   times(0', z0) -> 0'
   times(s(z0), z1) -> plus(z1, times(z0, z1))
   exp(z0, 0') -> s(0')
   exp(z0, s(z1)) -> times(z0, exp(z0, z1))
   ge(z0, 0') -> true
   ge(0', s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   tower(z0, z1) -> towerIter(0', z0, z1, s(0'))
   towerIter(z0, z1, z2, z3) -> help(ge(z0, z1), z0, z1, z2, z3)
   help(true, z0, z1, z2, z3) -> z3
   help(false, z0, z1, z2, z3) -> towerIter(s(z0), z1, z2, exp(z2, z3))

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

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(8)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(z0, z1))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
GE(z0, 0') -> c6
GE(0', s(z0)) -> c7
GE(s(z0), s(z1)) -> c8(GE(z0, z1))
TOWER(z0, z1) -> c9(TOWERITER(0', z0, z1, s(0')))
TOWERITER(z0, z1, z2, z3) -> c10(HELP(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
HELP(true, z0, z1, z2, z3) -> c11
HELP(false, z0, z1, z2, z3) -> c12(TOWERITER(s(z0), z1, z2, exp(z2, z3)), EXP(z2, z3))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
tower(z0, z1) -> towerIter(0', z0, z1, s(0'))
towerIter(z0, z1, z2, z3) -> help(ge(z0, z1), z0, z1, z2, z3)
help(true, z0, z1, z2, z3) -> z3
help(false, z0, z1, z2, z3) -> towerIter(s(z0), z1, z2, exp(z2, z3))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> 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
GE :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8
c8 :: c6:c7:c8 -> c6:c7:c8
TOWER :: 0':s -> 0':s -> c9
c9 :: c10 -> c9
TOWERITER :: 0':s -> 0':s -> 0':s -> 0':s -> c10
c10 :: c11:c12 -> c6:c7:c8 -> c10
HELP :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c11:c12
ge :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c11:c12
false :: true:false
c12 :: c10 -> c4:c5 -> c11:c12
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s -> 0':s
help :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_13 :: c:c1
hole_0':s2_13 :: 0':s
hole_c2:c33_13 :: c2:c3
hole_c4:c54_13 :: c4:c5
hole_c6:c7:c85_13 :: c6:c7:c8
hole_c96_13 :: c9
hole_c107_13 :: c10
hole_c11:c128_13 :: c11:c12
hole_true:false9_13 :: true:false
gen_c:c110_13 :: Nat -> c:c1
gen_0':s11_13 :: Nat -> 0':s
gen_c2:c312_13 :: Nat -> c2:c3
gen_c4:c513_13 :: Nat -> c4:c5
gen_c6:c7:c814_13 :: Nat -> c6:c7:c8

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
PLUS, TIMES, times, EXP, exp, GE, TOWERITER, ge, 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
GE < TOWERITER
ge < TOWERITER
ge < towerIter

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

(10)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(z0, z1))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
GE(z0, 0') -> c6
GE(0', s(z0)) -> c7
GE(s(z0), s(z1)) -> c8(GE(z0, z1))
TOWER(z0, z1) -> c9(TOWERITER(0', z0, z1, s(0')))
TOWERITER(z0, z1, z2, z3) -> c10(HELP(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
HELP(true, z0, z1, z2, z3) -> c11
HELP(false, z0, z1, z2, z3) -> c12(TOWERITER(s(z0), z1, z2, exp(z2, z3)), EXP(z2, z3))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
tower(z0, z1) -> towerIter(0', z0, z1, s(0'))
towerIter(z0, z1, z2, z3) -> help(ge(z0, z1), z0, z1, z2, z3)
help(true, z0, z1, z2, z3) -> z3
help(false, z0, z1, z2, z3) -> towerIter(s(z0), z1, z2, exp(z2, z3))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> 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
GE :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8
c8 :: c6:c7:c8 -> c6:c7:c8
TOWER :: 0':s -> 0':s -> c9
c9 :: c10 -> c9
TOWERITER :: 0':s -> 0':s -> 0':s -> 0':s -> c10
c10 :: c11:c12 -> c6:c7:c8 -> c10
HELP :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c11:c12
ge :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c11:c12
false :: true:false
c12 :: c10 -> c4:c5 -> c11:c12
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s -> 0':s
help :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_13 :: c:c1
hole_0':s2_13 :: 0':s
hole_c2:c33_13 :: c2:c3
hole_c4:c54_13 :: c4:c5
hole_c6:c7:c85_13 :: c6:c7:c8
hole_c96_13 :: c9
hole_c107_13 :: c10
hole_c11:c128_13 :: c11:c12
hole_true:false9_13 :: true:false
gen_c:c110_13 :: Nat -> c:c1
gen_0':s11_13 :: Nat -> 0':s
gen_c2:c312_13 :: Nat -> c2:c3
gen_c4:c513_13 :: Nat -> c4:c5
gen_c6:c7:c814_13 :: Nat -> c6:c7:c8


Generator Equations:
gen_c:c110_13(0) <=> c
gen_c:c110_13(+(x, 1)) <=> c1(gen_c:c110_13(x))
gen_0':s11_13(0) <=> 0'
gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x))
gen_c2:c312_13(0) <=> c2
gen_c2:c312_13(+(x, 1)) <=> c3(c, gen_c2:c312_13(x))
gen_c4:c513_13(0) <=> c4
gen_c4:c513_13(+(x, 1)) <=> c5(c2, gen_c4:c513_13(x))
gen_c6:c7:c814_13(0) <=> c6
gen_c6:c7:c814_13(+(x, 1)) <=> c8(gen_c6:c7:c814_13(x))


The following defined symbols remain to be analysed:
PLUS, TIMES, times, EXP, exp, GE, TOWERITER, ge, 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
GE < TOWERITER
ge < TOWERITER
ge < towerIter

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
PLUS(gen_0':s11_13(n16_13), gen_0':s11_13(b)) -> gen_c:c110_13(n16_13), rt in Omega(1 + n16_13)

Induction Base:
PLUS(gen_0':s11_13(0), gen_0':s11_13(b)) ->_R^Omega(1)
c

Induction Step:
PLUS(gen_0':s11_13(+(n16_13, 1)), gen_0':s11_13(b)) ->_R^Omega(1)
c1(PLUS(gen_0':s11_13(n16_13), gen_0':s11_13(b))) ->_IH
c1(gen_c:c110_13(c17_13))

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(z0, z1))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
GE(z0, 0') -> c6
GE(0', s(z0)) -> c7
GE(s(z0), s(z1)) -> c8(GE(z0, z1))
TOWER(z0, z1) -> c9(TOWERITER(0', z0, z1, s(0')))
TOWERITER(z0, z1, z2, z3) -> c10(HELP(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
HELP(true, z0, z1, z2, z3) -> c11
HELP(false, z0, z1, z2, z3) -> c12(TOWERITER(s(z0), z1, z2, exp(z2, z3)), EXP(z2, z3))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
tower(z0, z1) -> towerIter(0', z0, z1, s(0'))
towerIter(z0, z1, z2, z3) -> help(ge(z0, z1), z0, z1, z2, z3)
help(true, z0, z1, z2, z3) -> z3
help(false, z0, z1, z2, z3) -> towerIter(s(z0), z1, z2, exp(z2, z3))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> 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
GE :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8
c8 :: c6:c7:c8 -> c6:c7:c8
TOWER :: 0':s -> 0':s -> c9
c9 :: c10 -> c9
TOWERITER :: 0':s -> 0':s -> 0':s -> 0':s -> c10
c10 :: c11:c12 -> c6:c7:c8 -> c10
HELP :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c11:c12
ge :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c11:c12
false :: true:false
c12 :: c10 -> c4:c5 -> c11:c12
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s -> 0':s
help :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_13 :: c:c1
hole_0':s2_13 :: 0':s
hole_c2:c33_13 :: c2:c3
hole_c4:c54_13 :: c4:c5
hole_c6:c7:c85_13 :: c6:c7:c8
hole_c96_13 :: c9
hole_c107_13 :: c10
hole_c11:c128_13 :: c11:c12
hole_true:false9_13 :: true:false
gen_c:c110_13 :: Nat -> c:c1
gen_0':s11_13 :: Nat -> 0':s
gen_c2:c312_13 :: Nat -> c2:c3
gen_c4:c513_13 :: Nat -> c4:c5
gen_c6:c7:c814_13 :: Nat -> c6:c7:c8


Generator Equations:
gen_c:c110_13(0) <=> c
gen_c:c110_13(+(x, 1)) <=> c1(gen_c:c110_13(x))
gen_0':s11_13(0) <=> 0'
gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x))
gen_c2:c312_13(0) <=> c2
gen_c2:c312_13(+(x, 1)) <=> c3(c, gen_c2:c312_13(x))
gen_c4:c513_13(0) <=> c4
gen_c4:c513_13(+(x, 1)) <=> c5(c2, gen_c4:c513_13(x))
gen_c6:c7:c814_13(0) <=> c6
gen_c6:c7:c814_13(+(x, 1)) <=> c8(gen_c6:c7:c814_13(x))


The following defined symbols remain to be analysed:
PLUS, TIMES, times, EXP, exp, GE, TOWERITER, ge, 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
GE < TOWERITER
ge < TOWERITER
ge < 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(z0, z1))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
GE(z0, 0') -> c6
GE(0', s(z0)) -> c7
GE(s(z0), s(z1)) -> c8(GE(z0, z1))
TOWER(z0, z1) -> c9(TOWERITER(0', z0, z1, s(0')))
TOWERITER(z0, z1, z2, z3) -> c10(HELP(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
HELP(true, z0, z1, z2, z3) -> c11
HELP(false, z0, z1, z2, z3) -> c12(TOWERITER(s(z0), z1, z2, exp(z2, z3)), EXP(z2, z3))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
tower(z0, z1) -> towerIter(0', z0, z1, s(0'))
towerIter(z0, z1, z2, z3) -> help(ge(z0, z1), z0, z1, z2, z3)
help(true, z0, z1, z2, z3) -> z3
help(false, z0, z1, z2, z3) -> towerIter(s(z0), z1, z2, exp(z2, z3))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> 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
GE :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8
c8 :: c6:c7:c8 -> c6:c7:c8
TOWER :: 0':s -> 0':s -> c9
c9 :: c10 -> c9
TOWERITER :: 0':s -> 0':s -> 0':s -> 0':s -> c10
c10 :: c11:c12 -> c6:c7:c8 -> c10
HELP :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c11:c12
ge :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c11:c12
false :: true:false
c12 :: c10 -> c4:c5 -> c11:c12
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s -> 0':s
help :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_13 :: c:c1
hole_0':s2_13 :: 0':s
hole_c2:c33_13 :: c2:c3
hole_c4:c54_13 :: c4:c5
hole_c6:c7:c85_13 :: c6:c7:c8
hole_c96_13 :: c9
hole_c107_13 :: c10
hole_c11:c128_13 :: c11:c12
hole_true:false9_13 :: true:false
gen_c:c110_13 :: Nat -> c:c1
gen_0':s11_13 :: Nat -> 0':s
gen_c2:c312_13 :: Nat -> c2:c3
gen_c4:c513_13 :: Nat -> c4:c5
gen_c6:c7:c814_13 :: Nat -> c6:c7:c8


Lemmas:
PLUS(gen_0':s11_13(n16_13), gen_0':s11_13(b)) -> gen_c:c110_13(n16_13), rt in Omega(1 + n16_13)


Generator Equations:
gen_c:c110_13(0) <=> c
gen_c:c110_13(+(x, 1)) <=> c1(gen_c:c110_13(x))
gen_0':s11_13(0) <=> 0'
gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x))
gen_c2:c312_13(0) <=> c2
gen_c2:c312_13(+(x, 1)) <=> c3(c, gen_c2:c312_13(x))
gen_c4:c513_13(0) <=> c4
gen_c4:c513_13(+(x, 1)) <=> c5(c2, gen_c4:c513_13(x))
gen_c6:c7:c814_13(0) <=> c6
gen_c6:c7:c814_13(+(x, 1)) <=> c8(gen_c6:c7:c814_13(x))


The following defined symbols remain to be analysed:
GE, TIMES, times, EXP, exp, TOWERITER, ge, plus, 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
GE < TOWERITER
ge < TOWERITER
ge < towerIter

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
GE(gen_0':s11_13(n667_13), gen_0':s11_13(n667_13)) -> gen_c6:c7:c814_13(n667_13), rt in Omega(1 + n667_13)

Induction Base:
GE(gen_0':s11_13(0), gen_0':s11_13(0)) ->_R^Omega(1)
c6

Induction Step:
GE(gen_0':s11_13(+(n667_13, 1)), gen_0':s11_13(+(n667_13, 1))) ->_R^Omega(1)
c8(GE(gen_0':s11_13(n667_13), gen_0':s11_13(n667_13))) ->_IH
c8(gen_c6:c7:c814_13(c668_13))

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

(18)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(z0, z1))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
GE(z0, 0') -> c6
GE(0', s(z0)) -> c7
GE(s(z0), s(z1)) -> c8(GE(z0, z1))
TOWER(z0, z1) -> c9(TOWERITER(0', z0, z1, s(0')))
TOWERITER(z0, z1, z2, z3) -> c10(HELP(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
HELP(true, z0, z1, z2, z3) -> c11
HELP(false, z0, z1, z2, z3) -> c12(TOWERITER(s(z0), z1, z2, exp(z2, z3)), EXP(z2, z3))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
tower(z0, z1) -> towerIter(0', z0, z1, s(0'))
towerIter(z0, z1, z2, z3) -> help(ge(z0, z1), z0, z1, z2, z3)
help(true, z0, z1, z2, z3) -> z3
help(false, z0, z1, z2, z3) -> towerIter(s(z0), z1, z2, exp(z2, z3))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> 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
GE :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8
c8 :: c6:c7:c8 -> c6:c7:c8
TOWER :: 0':s -> 0':s -> c9
c9 :: c10 -> c9
TOWERITER :: 0':s -> 0':s -> 0':s -> 0':s -> c10
c10 :: c11:c12 -> c6:c7:c8 -> c10
HELP :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c11:c12
ge :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c11:c12
false :: true:false
c12 :: c10 -> c4:c5 -> c11:c12
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s -> 0':s
help :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_13 :: c:c1
hole_0':s2_13 :: 0':s
hole_c2:c33_13 :: c2:c3
hole_c4:c54_13 :: c4:c5
hole_c6:c7:c85_13 :: c6:c7:c8
hole_c96_13 :: c9
hole_c107_13 :: c10
hole_c11:c128_13 :: c11:c12
hole_true:false9_13 :: true:false
gen_c:c110_13 :: Nat -> c:c1
gen_0':s11_13 :: Nat -> 0':s
gen_c2:c312_13 :: Nat -> c2:c3
gen_c4:c513_13 :: Nat -> c4:c5
gen_c6:c7:c814_13 :: Nat -> c6:c7:c8


Lemmas:
PLUS(gen_0':s11_13(n16_13), gen_0':s11_13(b)) -> gen_c:c110_13(n16_13), rt in Omega(1 + n16_13)
GE(gen_0':s11_13(n667_13), gen_0':s11_13(n667_13)) -> gen_c6:c7:c814_13(n667_13), rt in Omega(1 + n667_13)


Generator Equations:
gen_c:c110_13(0) <=> c
gen_c:c110_13(+(x, 1)) <=> c1(gen_c:c110_13(x))
gen_0':s11_13(0) <=> 0'
gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x))
gen_c2:c312_13(0) <=> c2
gen_c2:c312_13(+(x, 1)) <=> c3(c, gen_c2:c312_13(x))
gen_c4:c513_13(0) <=> c4
gen_c4:c513_13(+(x, 1)) <=> c5(c2, gen_c4:c513_13(x))
gen_c6:c7:c814_13(0) <=> c6
gen_c6:c7:c814_13(+(x, 1)) <=> c8(gen_c6:c7:c814_13(x))


The following defined symbols remain to be analysed:
ge, TIMES, times, EXP, exp, TOWERITER, plus, 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
ge < TOWERITER
ge < towerIter

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ge(gen_0':s11_13(n1467_13), gen_0':s11_13(n1467_13)) -> true, rt in Omega(0)

Induction Base:
ge(gen_0':s11_13(0), gen_0':s11_13(0)) ->_R^Omega(0)
true

Induction Step:
ge(gen_0':s11_13(+(n1467_13, 1)), gen_0':s11_13(+(n1467_13, 1))) ->_R^Omega(0)
ge(gen_0':s11_13(n1467_13), gen_0':s11_13(n1467_13)) ->_IH
true

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

(20)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(z0, z1))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
GE(z0, 0') -> c6
GE(0', s(z0)) -> c7
GE(s(z0), s(z1)) -> c8(GE(z0, z1))
TOWER(z0, z1) -> c9(TOWERITER(0', z0, z1, s(0')))
TOWERITER(z0, z1, z2, z3) -> c10(HELP(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
HELP(true, z0, z1, z2, z3) -> c11
HELP(false, z0, z1, z2, z3) -> c12(TOWERITER(s(z0), z1, z2, exp(z2, z3)), EXP(z2, z3))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
tower(z0, z1) -> towerIter(0', z0, z1, s(0'))
towerIter(z0, z1, z2, z3) -> help(ge(z0, z1), z0, z1, z2, z3)
help(true, z0, z1, z2, z3) -> z3
help(false, z0, z1, z2, z3) -> towerIter(s(z0), z1, z2, exp(z2, z3))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> 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
GE :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8
c8 :: c6:c7:c8 -> c6:c7:c8
TOWER :: 0':s -> 0':s -> c9
c9 :: c10 -> c9
TOWERITER :: 0':s -> 0':s -> 0':s -> 0':s -> c10
c10 :: c11:c12 -> c6:c7:c8 -> c10
HELP :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c11:c12
ge :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c11:c12
false :: true:false
c12 :: c10 -> c4:c5 -> c11:c12
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s -> 0':s
help :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_13 :: c:c1
hole_0':s2_13 :: 0':s
hole_c2:c33_13 :: c2:c3
hole_c4:c54_13 :: c4:c5
hole_c6:c7:c85_13 :: c6:c7:c8
hole_c96_13 :: c9
hole_c107_13 :: c10
hole_c11:c128_13 :: c11:c12
hole_true:false9_13 :: true:false
gen_c:c110_13 :: Nat -> c:c1
gen_0':s11_13 :: Nat -> 0':s
gen_c2:c312_13 :: Nat -> c2:c3
gen_c4:c513_13 :: Nat -> c4:c5
gen_c6:c7:c814_13 :: Nat -> c6:c7:c8


Lemmas:
PLUS(gen_0':s11_13(n16_13), gen_0':s11_13(b)) -> gen_c:c110_13(n16_13), rt in Omega(1 + n16_13)
GE(gen_0':s11_13(n667_13), gen_0':s11_13(n667_13)) -> gen_c6:c7:c814_13(n667_13), rt in Omega(1 + n667_13)
ge(gen_0':s11_13(n1467_13), gen_0':s11_13(n1467_13)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c110_13(0) <=> c
gen_c:c110_13(+(x, 1)) <=> c1(gen_c:c110_13(x))
gen_0':s11_13(0) <=> 0'
gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x))
gen_c2:c312_13(0) <=> c2
gen_c2:c312_13(+(x, 1)) <=> c3(c, gen_c2:c312_13(x))
gen_c4:c513_13(0) <=> c4
gen_c4:c513_13(+(x, 1)) <=> c5(c2, gen_c4:c513_13(x))
gen_c6:c7:c814_13(0) <=> c6
gen_c6:c7:c814_13(+(x, 1)) <=> c8(gen_c6:c7:c814_13(x))


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

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

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

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

Induction Step:
plus(gen_0':s11_13(+(n1897_13, 1)), gen_0':s11_13(b)) ->_R^Omega(0)
s(plus(gen_0':s11_13(n1897_13), gen_0':s11_13(b))) ->_IH
s(gen_0':s11_13(+(b, c1898_13)))

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

(22)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(z0, z1))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
GE(z0, 0') -> c6
GE(0', s(z0)) -> c7
GE(s(z0), s(z1)) -> c8(GE(z0, z1))
TOWER(z0, z1) -> c9(TOWERITER(0', z0, z1, s(0')))
TOWERITER(z0, z1, z2, z3) -> c10(HELP(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
HELP(true, z0, z1, z2, z3) -> c11
HELP(false, z0, z1, z2, z3) -> c12(TOWERITER(s(z0), z1, z2, exp(z2, z3)), EXP(z2, z3))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
tower(z0, z1) -> towerIter(0', z0, z1, s(0'))
towerIter(z0, z1, z2, z3) -> help(ge(z0, z1), z0, z1, z2, z3)
help(true, z0, z1, z2, z3) -> z3
help(false, z0, z1, z2, z3) -> towerIter(s(z0), z1, z2, exp(z2, z3))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> 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
GE :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8
c8 :: c6:c7:c8 -> c6:c7:c8
TOWER :: 0':s -> 0':s -> c9
c9 :: c10 -> c9
TOWERITER :: 0':s -> 0':s -> 0':s -> 0':s -> c10
c10 :: c11:c12 -> c6:c7:c8 -> c10
HELP :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c11:c12
ge :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c11:c12
false :: true:false
c12 :: c10 -> c4:c5 -> c11:c12
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s -> 0':s
help :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_13 :: c:c1
hole_0':s2_13 :: 0':s
hole_c2:c33_13 :: c2:c3
hole_c4:c54_13 :: c4:c5
hole_c6:c7:c85_13 :: c6:c7:c8
hole_c96_13 :: c9
hole_c107_13 :: c10
hole_c11:c128_13 :: c11:c12
hole_true:false9_13 :: true:false
gen_c:c110_13 :: Nat -> c:c1
gen_0':s11_13 :: Nat -> 0':s
gen_c2:c312_13 :: Nat -> c2:c3
gen_c4:c513_13 :: Nat -> c4:c5
gen_c6:c7:c814_13 :: Nat -> c6:c7:c8


Lemmas:
PLUS(gen_0':s11_13(n16_13), gen_0':s11_13(b)) -> gen_c:c110_13(n16_13), rt in Omega(1 + n16_13)
GE(gen_0':s11_13(n667_13), gen_0':s11_13(n667_13)) -> gen_c6:c7:c814_13(n667_13), rt in Omega(1 + n667_13)
ge(gen_0':s11_13(n1467_13), gen_0':s11_13(n1467_13)) -> true, rt in Omega(0)
plus(gen_0':s11_13(n1897_13), gen_0':s11_13(b)) -> gen_0':s11_13(+(n1897_13, b)), rt in Omega(0)


Generator Equations:
gen_c:c110_13(0) <=> c
gen_c:c110_13(+(x, 1)) <=> c1(gen_c:c110_13(x))
gen_0':s11_13(0) <=> 0'
gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x))
gen_c2:c312_13(0) <=> c2
gen_c2:c312_13(+(x, 1)) <=> c3(c, gen_c2:c312_13(x))
gen_c4:c513_13(0) <=> c4
gen_c4:c513_13(+(x, 1)) <=> c5(c2, gen_c4:c513_13(x))
gen_c6:c7:c814_13(0) <=> c6
gen_c6:c7:c814_13(+(x, 1)) <=> c8(gen_c6:c7:c814_13(x))


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

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

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

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

Induction Step:
times(gen_0':s11_13(+(n3334_13, 1)), gen_0':s11_13(b)) ->_R^Omega(0)
plus(gen_0':s11_13(b), times(gen_0':s11_13(n3334_13), gen_0':s11_13(b))) ->_IH
plus(gen_0':s11_13(b), gen_0':s11_13(*(c3335_13, b))) ->_L^Omega(0)
gen_0':s11_13(+(b, *(n3334_13, b)))

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(z0, z1))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
GE(z0, 0') -> c6
GE(0', s(z0)) -> c7
GE(s(z0), s(z1)) -> c8(GE(z0, z1))
TOWER(z0, z1) -> c9(TOWERITER(0', z0, z1, s(0')))
TOWERITER(z0, z1, z2, z3) -> c10(HELP(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
HELP(true, z0, z1, z2, z3) -> c11
HELP(false, z0, z1, z2, z3) -> c12(TOWERITER(s(z0), z1, z2, exp(z2, z3)), EXP(z2, z3))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
tower(z0, z1) -> towerIter(0', z0, z1, s(0'))
towerIter(z0, z1, z2, z3) -> help(ge(z0, z1), z0, z1, z2, z3)
help(true, z0, z1, z2, z3) -> z3
help(false, z0, z1, z2, z3) -> towerIter(s(z0), z1, z2, exp(z2, z3))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> 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
GE :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8
c8 :: c6:c7:c8 -> c6:c7:c8
TOWER :: 0':s -> 0':s -> c9
c9 :: c10 -> c9
TOWERITER :: 0':s -> 0':s -> 0':s -> 0':s -> c10
c10 :: c11:c12 -> c6:c7:c8 -> c10
HELP :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c11:c12
ge :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c11:c12
false :: true:false
c12 :: c10 -> c4:c5 -> c11:c12
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s -> 0':s
help :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_13 :: c:c1
hole_0':s2_13 :: 0':s
hole_c2:c33_13 :: c2:c3
hole_c4:c54_13 :: c4:c5
hole_c6:c7:c85_13 :: c6:c7:c8
hole_c96_13 :: c9
hole_c107_13 :: c10
hole_c11:c128_13 :: c11:c12
hole_true:false9_13 :: true:false
gen_c:c110_13 :: Nat -> c:c1
gen_0':s11_13 :: Nat -> 0':s
gen_c2:c312_13 :: Nat -> c2:c3
gen_c4:c513_13 :: Nat -> c4:c5
gen_c6:c7:c814_13 :: Nat -> c6:c7:c8


Lemmas:
PLUS(gen_0':s11_13(n16_13), gen_0':s11_13(b)) -> gen_c:c110_13(n16_13), rt in Omega(1 + n16_13)
GE(gen_0':s11_13(n667_13), gen_0':s11_13(n667_13)) -> gen_c6:c7:c814_13(n667_13), rt in Omega(1 + n667_13)
ge(gen_0':s11_13(n1467_13), gen_0':s11_13(n1467_13)) -> true, rt in Omega(0)
plus(gen_0':s11_13(n1897_13), gen_0':s11_13(b)) -> gen_0':s11_13(+(n1897_13, b)), rt in Omega(0)
times(gen_0':s11_13(n3334_13), gen_0':s11_13(b)) -> gen_0':s11_13(*(n3334_13, b)), rt in Omega(0)


Generator Equations:
gen_c:c110_13(0) <=> c
gen_c:c110_13(+(x, 1)) <=> c1(gen_c:c110_13(x))
gen_0':s11_13(0) <=> 0'
gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x))
gen_c2:c312_13(0) <=> c2
gen_c2:c312_13(+(x, 1)) <=> c3(c, gen_c2:c312_13(x))
gen_c4:c513_13(0) <=> c4
gen_c4:c513_13(+(x, 1)) <=> c5(c2, gen_c4:c513_13(x))
gen_c6:c7:c814_13(0) <=> c6
gen_c6:c7:c814_13(+(x, 1)) <=> c8(gen_c6:c7:c814_13(x))


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

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
TIMES(gen_0':s11_13(n5138_13), gen_0':s11_13(b)) -> *15_13, rt in Omega(b*n5138_13 + n5138_13)

Induction Base:
TIMES(gen_0':s11_13(0), gen_0':s11_13(b))

Induction Step:
TIMES(gen_0':s11_13(+(n5138_13, 1)), gen_0':s11_13(b)) ->_R^Omega(1)
c3(PLUS(gen_0':s11_13(b), times(gen_0':s11_13(n5138_13), gen_0':s11_13(b))), TIMES(gen_0':s11_13(n5138_13), gen_0':s11_13(b))) ->_L^Omega(0)
c3(PLUS(gen_0':s11_13(b), gen_0':s11_13(*(n5138_13, b))), TIMES(gen_0':s11_13(n5138_13), gen_0':s11_13(b))) ->_L^Omega(1 + b)
c3(gen_c:c110_13(b), TIMES(gen_0':s11_13(n5138_13), gen_0':s11_13(*(n5138_13, b)))) ->_IH
c3(gen_c:c110_13(*(n5138_13, b)), *15_13)

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

(26)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(z0, z1))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
GE(z0, 0') -> c6
GE(0', s(z0)) -> c7
GE(s(z0), s(z1)) -> c8(GE(z0, z1))
TOWER(z0, z1) -> c9(TOWERITER(0', z0, z1, s(0')))
TOWERITER(z0, z1, z2, z3) -> c10(HELP(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
HELP(true, z0, z1, z2, z3) -> c11
HELP(false, z0, z1, z2, z3) -> c12(TOWERITER(s(z0), z1, z2, exp(z2, z3)), EXP(z2, z3))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
tower(z0, z1) -> towerIter(0', z0, z1, s(0'))
towerIter(z0, z1, z2, z3) -> help(ge(z0, z1), z0, z1, z2, z3)
help(true, z0, z1, z2, z3) -> z3
help(false, z0, z1, z2, z3) -> towerIter(s(z0), z1, z2, exp(z2, z3))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> 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
GE :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8
c8 :: c6:c7:c8 -> c6:c7:c8
TOWER :: 0':s -> 0':s -> c9
c9 :: c10 -> c9
TOWERITER :: 0':s -> 0':s -> 0':s -> 0':s -> c10
c10 :: c11:c12 -> c6:c7:c8 -> c10
HELP :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c11:c12
ge :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c11:c12
false :: true:false
c12 :: c10 -> c4:c5 -> c11:c12
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s -> 0':s
help :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_13 :: c:c1
hole_0':s2_13 :: 0':s
hole_c2:c33_13 :: c2:c3
hole_c4:c54_13 :: c4:c5
hole_c6:c7:c85_13 :: c6:c7:c8
hole_c96_13 :: c9
hole_c107_13 :: c10
hole_c11:c128_13 :: c11:c12
hole_true:false9_13 :: true:false
gen_c:c110_13 :: Nat -> c:c1
gen_0':s11_13 :: Nat -> 0':s
gen_c2:c312_13 :: Nat -> c2:c3
gen_c4:c513_13 :: Nat -> c4:c5
gen_c6:c7:c814_13 :: Nat -> c6:c7:c8


Lemmas:
PLUS(gen_0':s11_13(n16_13), gen_0':s11_13(b)) -> gen_c:c110_13(n16_13), rt in Omega(1 + n16_13)
GE(gen_0':s11_13(n667_13), gen_0':s11_13(n667_13)) -> gen_c6:c7:c814_13(n667_13), rt in Omega(1 + n667_13)
ge(gen_0':s11_13(n1467_13), gen_0':s11_13(n1467_13)) -> true, rt in Omega(0)
plus(gen_0':s11_13(n1897_13), gen_0':s11_13(b)) -> gen_0':s11_13(+(n1897_13, b)), rt in Omega(0)
times(gen_0':s11_13(n3334_13), gen_0':s11_13(b)) -> gen_0':s11_13(*(n3334_13, b)), rt in Omega(0)


Generator Equations:
gen_c:c110_13(0) <=> c
gen_c:c110_13(+(x, 1)) <=> c1(gen_c:c110_13(x))
gen_0':s11_13(0) <=> 0'
gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x))
gen_c2:c312_13(0) <=> c2
gen_c2:c312_13(+(x, 1)) <=> c3(c, gen_c2:c312_13(x))
gen_c4:c513_13(0) <=> c4
gen_c4:c513_13(+(x, 1)) <=> c5(c2, gen_c4:c513_13(x))
gen_c6:c7:c814_13(0) <=> c6
gen_c6:c7:c814_13(+(x, 1)) <=> c8(gen_c6:c7:c814_13(x))


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

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

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

(29)
BOUNDS(n^2, INF)

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

(30)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(z0, z1))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
GE(z0, 0') -> c6
GE(0', s(z0)) -> c7
GE(s(z0), s(z1)) -> c8(GE(z0, z1))
TOWER(z0, z1) -> c9(TOWERITER(0', z0, z1, s(0')))
TOWERITER(z0, z1, z2, z3) -> c10(HELP(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
HELP(true, z0, z1, z2, z3) -> c11
HELP(false, z0, z1, z2, z3) -> c12(TOWERITER(s(z0), z1, z2, exp(z2, z3)), EXP(z2, z3))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
tower(z0, z1) -> towerIter(0', z0, z1, s(0'))
towerIter(z0, z1, z2, z3) -> help(ge(z0, z1), z0, z1, z2, z3)
help(true, z0, z1, z2, z3) -> z3
help(false, z0, z1, z2, z3) -> towerIter(s(z0), z1, z2, exp(z2, z3))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> 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
GE :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8
c8 :: c6:c7:c8 -> c6:c7:c8
TOWER :: 0':s -> 0':s -> c9
c9 :: c10 -> c9
TOWERITER :: 0':s -> 0':s -> 0':s -> 0':s -> c10
c10 :: c11:c12 -> c6:c7:c8 -> c10
HELP :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c11:c12
ge :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c11:c12
false :: true:false
c12 :: c10 -> c4:c5 -> c11:c12
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s -> 0':s
help :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_13 :: c:c1
hole_0':s2_13 :: 0':s
hole_c2:c33_13 :: c2:c3
hole_c4:c54_13 :: c4:c5
hole_c6:c7:c85_13 :: c6:c7:c8
hole_c96_13 :: c9
hole_c107_13 :: c10
hole_c11:c128_13 :: c11:c12
hole_true:false9_13 :: true:false
gen_c:c110_13 :: Nat -> c:c1
gen_0':s11_13 :: Nat -> 0':s
gen_c2:c312_13 :: Nat -> c2:c3
gen_c4:c513_13 :: Nat -> c4:c5
gen_c6:c7:c814_13 :: Nat -> c6:c7:c8


Lemmas:
PLUS(gen_0':s11_13(n16_13), gen_0':s11_13(b)) -> gen_c:c110_13(n16_13), rt in Omega(1 + n16_13)
GE(gen_0':s11_13(n667_13), gen_0':s11_13(n667_13)) -> gen_c6:c7:c814_13(n667_13), rt in Omega(1 + n667_13)
ge(gen_0':s11_13(n1467_13), gen_0':s11_13(n1467_13)) -> true, rt in Omega(0)
plus(gen_0':s11_13(n1897_13), gen_0':s11_13(b)) -> gen_0':s11_13(+(n1897_13, b)), rt in Omega(0)
times(gen_0':s11_13(n3334_13), gen_0':s11_13(b)) -> gen_0':s11_13(*(n3334_13, b)), rt in Omega(0)
TIMES(gen_0':s11_13(n5138_13), gen_0':s11_13(b)) -> *15_13, rt in Omega(b*n5138_13 + n5138_13)


Generator Equations:
gen_c:c110_13(0) <=> c
gen_c:c110_13(+(x, 1)) <=> c1(gen_c:c110_13(x))
gen_0':s11_13(0) <=> 0'
gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x))
gen_c2:c312_13(0) <=> c2
gen_c2:c312_13(+(x, 1)) <=> c3(c, gen_c2:c312_13(x))
gen_c4:c513_13(0) <=> c4
gen_c4:c513_13(+(x, 1)) <=> c5(c2, gen_c4:c513_13(x))
gen_c6:c7:c814_13(0) <=> c6
gen_c6:c7:c814_13(+(x, 1)) <=> c8(gen_c6:c7:c814_13(x))


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

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

(31) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
exp(gen_0':s11_13(a), gen_0':s11_13(+(1, n37868_13))) -> *15_13, rt in Omega(0)

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

Induction Step:
exp(gen_0':s11_13(a), gen_0':s11_13(+(1, +(n37868_13, 1)))) ->_R^Omega(0)
times(gen_0':s11_13(a), exp(gen_0':s11_13(a), gen_0':s11_13(+(1, n37868_13)))) ->_IH
times(gen_0':s11_13(a), *15_13)

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

(32)
Obligation:
Innermost TRS:
Rules:
PLUS(0', z0) -> c
PLUS(s(z0), z1) -> c1(PLUS(z0, z1))
TIMES(0', z0) -> c2
TIMES(s(z0), z1) -> c3(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
EXP(z0, 0') -> c4
EXP(z0, s(z1)) -> c5(TIMES(z0, exp(z0, z1)), EXP(z0, z1))
GE(z0, 0') -> c6
GE(0', s(z0)) -> c7
GE(s(z0), s(z1)) -> c8(GE(z0, z1))
TOWER(z0, z1) -> c9(TOWERITER(0', z0, z1, s(0')))
TOWERITER(z0, z1, z2, z3) -> c10(HELP(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
HELP(true, z0, z1, z2, z3) -> c11
HELP(false, z0, z1, z2, z3) -> c12(TOWERITER(s(z0), z1, z2, exp(z2, z3)), EXP(z2, z3))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> plus(z1, times(z0, z1))
exp(z0, 0') -> s(0')
exp(z0, s(z1)) -> times(z0, exp(z0, z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
tower(z0, z1) -> towerIter(0', z0, z1, s(0'))
towerIter(z0, z1, z2, z3) -> help(ge(z0, z1), z0, z1, z2, z3)
help(true, z0, z1, z2, z3) -> z3
help(false, z0, z1, z2, z3) -> towerIter(s(z0), z1, z2, exp(z2, z3))

Types:
PLUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
TIMES :: 0':s -> 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c2:c3 -> 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
GE :: 0':s -> 0':s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8
c8 :: c6:c7:c8 -> c6:c7:c8
TOWER :: 0':s -> 0':s -> c9
c9 :: c10 -> c9
TOWERITER :: 0':s -> 0':s -> 0':s -> 0':s -> c10
c10 :: c11:c12 -> c6:c7:c8 -> c10
HELP :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c11:c12
ge :: 0':s -> 0':s -> true:false
true :: true:false
c11 :: c11:c12
false :: true:false
c12 :: c10 -> c4:c5 -> c11:c12
plus :: 0':s -> 0':s -> 0':s
tower :: 0':s -> 0':s -> 0':s
towerIter :: 0':s -> 0':s -> 0':s -> 0':s -> 0':s
help :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
hole_c:c11_13 :: c:c1
hole_0':s2_13 :: 0':s
hole_c2:c33_13 :: c2:c3
hole_c4:c54_13 :: c4:c5
hole_c6:c7:c85_13 :: c6:c7:c8
hole_c96_13 :: c9
hole_c107_13 :: c10
hole_c11:c128_13 :: c11:c12
hole_true:false9_13 :: true:false
gen_c:c110_13 :: Nat -> c:c1
gen_0':s11_13 :: Nat -> 0':s
gen_c2:c312_13 :: Nat -> c2:c3
gen_c4:c513_13 :: Nat -> c4:c5
gen_c6:c7:c814_13 :: Nat -> c6:c7:c8


Lemmas:
PLUS(gen_0':s11_13(n16_13), gen_0':s11_13(b)) -> gen_c:c110_13(n16_13), rt in Omega(1 + n16_13)
GE(gen_0':s11_13(n667_13), gen_0':s11_13(n667_13)) -> gen_c6:c7:c814_13(n667_13), rt in Omega(1 + n667_13)
ge(gen_0':s11_13(n1467_13), gen_0':s11_13(n1467_13)) -> true, rt in Omega(0)
plus(gen_0':s11_13(n1897_13), gen_0':s11_13(b)) -> gen_0':s11_13(+(n1897_13, b)), rt in Omega(0)
times(gen_0':s11_13(n3334_13), gen_0':s11_13(b)) -> gen_0':s11_13(*(n3334_13, b)), rt in Omega(0)
TIMES(gen_0':s11_13(n5138_13), gen_0':s11_13(b)) -> *15_13, rt in Omega(b*n5138_13 + n5138_13)
exp(gen_0':s11_13(a), gen_0':s11_13(+(1, n37868_13))) -> *15_13, rt in Omega(0)


Generator Equations:
gen_c:c110_13(0) <=> c
gen_c:c110_13(+(x, 1)) <=> c1(gen_c:c110_13(x))
gen_0':s11_13(0) <=> 0'
gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x))
gen_c2:c312_13(0) <=> c2
gen_c2:c312_13(+(x, 1)) <=> c3(c, gen_c2:c312_13(x))
gen_c4:c513_13(0) <=> c4
gen_c4:c513_13(+(x, 1)) <=> c5(c2, gen_c4:c513_13(x))
gen_c6:c7:c814_13(0) <=> c6
gen_c6:c7:c814_13(+(x, 1)) <=> c8(gen_c6:c7:c814_13(x))


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

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