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


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, 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), 6 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 302 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), 4801 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 80 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 40 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 356 ms]
        (24) typed CpxTrs


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

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


The TRS R consists of the following rules:

   tower(x) -> f(a, x, s(0))
   f(a, 0, y) -> y
   f(a, s(x), y) -> f(b, y, s(x))
   f(b, y, x) -> f(a, half(x), exp(y))
   exp(0) -> s(0)
   exp(s(x)) -> double(exp(x))
   double(0) -> 0
   double(s(x)) -> s(s(double(x)))
   half(0) -> double(0)
   half(s(0)) -> half(0)
   half(s(s(x))) -> s(half(x))

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:
   tower(z0) -> f(a, z0, s(0))
   f(a, 0, z0) -> z0
   f(a, s(z0), z1) -> f(b, z1, s(z0))
   f(b, z0, z1) -> f(a, half(z1), exp(z0))
   exp(0) -> s(0)
   exp(s(z0)) -> double(exp(z0))
   double(0) -> 0
   double(s(z0)) -> s(s(double(z0)))
   half(0) -> double(0)
   half(s(0)) -> half(0)
   half(s(s(z0))) -> s(half(z0))
Tuples:
   TOWER(z0) -> c(F(a, z0, s(0)))
   F(a, 0, z0) -> c1
   F(a, s(z0), z1) -> c2(F(b, z1, s(z0)))
   F(b, z0, z1) -> c3(F(a, half(z1), exp(z0)), HALF(z1))
   F(b, z0, z1) -> c4(F(a, half(z1), exp(z0)), EXP(z0))
   EXP(0) -> c5
   EXP(s(z0)) -> c6(DOUBLE(exp(z0)), EXP(z0))
   DOUBLE(0) -> c7
   DOUBLE(s(z0)) -> c8(DOUBLE(z0))
   HALF(0) -> c9(DOUBLE(0))
   HALF(s(0)) -> c10(HALF(0))
   HALF(s(s(z0))) -> c11(HALF(z0))
S tuples:
   TOWER(z0) -> c(F(a, z0, s(0)))
   F(a, 0, z0) -> c1
   F(a, s(z0), z1) -> c2(F(b, z1, s(z0)))
   F(b, z0, z1) -> c3(F(a, half(z1), exp(z0)), HALF(z1))
   F(b, z0, z1) -> c4(F(a, half(z1), exp(z0)), EXP(z0))
   EXP(0) -> c5
   EXP(s(z0)) -> c6(DOUBLE(exp(z0)), EXP(z0))
   DOUBLE(0) -> c7
   DOUBLE(s(z0)) -> c8(DOUBLE(z0))
   HALF(0) -> c9(DOUBLE(0))
   HALF(s(0)) -> c10(HALF(0))
   HALF(s(s(z0))) -> c11(HALF(z0))
K tuples:none
Defined Rule Symbols:   tower_1, f_3, exp_1, double_1, half_1

Defined Pair Symbols:   TOWER_1, F_3, EXP_1, DOUBLE_1, HALF_1

Compound Symbols:   c_1, c1, c2_1, c3_2, c4_2, c5, c6_2, c7, c8_1, c9_1, c10_1, c11_1


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

(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^1, INF).


The TRS R consists of the following rules:

   TOWER(z0) -> c(F(a, z0, s(0)))
   F(a, 0, z0) -> c1
   F(a, s(z0), z1) -> c2(F(b, z1, s(z0)))
   F(b, z0, z1) -> c3(F(a, half(z1), exp(z0)), HALF(z1))
   F(b, z0, z1) -> c4(F(a, half(z1), exp(z0)), EXP(z0))
   EXP(0) -> c5
   EXP(s(z0)) -> c6(DOUBLE(exp(z0)), EXP(z0))
   DOUBLE(0) -> c7
   DOUBLE(s(z0)) -> c8(DOUBLE(z0))
   HALF(0) -> c9(DOUBLE(0))
   HALF(s(0)) -> c10(HALF(0))
   HALF(s(s(z0))) -> c11(HALF(z0))

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

   tower(z0) -> f(a, z0, s(0))
   f(a, 0, z0) -> z0
   f(a, s(z0), z1) -> f(b, z1, s(z0))
   f(b, z0, z1) -> f(a, half(z1), exp(z0))
   exp(0) -> s(0)
   exp(s(z0)) -> double(exp(z0))
   double(0) -> 0
   double(s(z0)) -> s(s(double(z0)))
   half(0) -> double(0)
   half(s(0)) -> half(0)
   half(s(s(z0))) -> s(half(z0))

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^1, INF).


The TRS R consists of the following rules:

   TOWER(z0) -> c(F(a, z0, s(0')))
   F(a, 0', z0) -> c1
   F(a, s(z0), z1) -> c2(F(b, z1, s(z0)))
   F(b, z0, z1) -> c3(F(a, half(z1), exp(z0)), HALF(z1))
   F(b, z0, z1) -> c4(F(a, half(z1), exp(z0)), EXP(z0))
   EXP(0') -> c5
   EXP(s(z0)) -> c6(DOUBLE(exp(z0)), EXP(z0))
   DOUBLE(0') -> c7
   DOUBLE(s(z0)) -> c8(DOUBLE(z0))
   HALF(0') -> c9(DOUBLE(0'))
   HALF(s(0')) -> c10(HALF(0'))
   HALF(s(s(z0))) -> c11(HALF(z0))

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

   tower(z0) -> f(a, z0, s(0'))
   f(a, 0', z0) -> z0
   f(a, s(z0), z1) -> f(b, z1, s(z0))
   f(b, z0, z1) -> f(a, half(z1), exp(z0))
   exp(0') -> s(0')
   exp(s(z0)) -> double(exp(z0))
   double(0') -> 0'
   double(s(z0)) -> s(s(double(z0)))
   half(0') -> double(0')
   half(s(0')) -> half(0')
   half(s(s(z0))) -> s(half(z0))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
TOWER(z0) -> c(F(a, z0, s(0')))
F(a, 0', z0) -> c1
F(a, s(z0), z1) -> c2(F(b, z1, s(z0)))
F(b, z0, z1) -> c3(F(a, half(z1), exp(z0)), HALF(z1))
F(b, z0, z1) -> c4(F(a, half(z1), exp(z0)), EXP(z0))
EXP(0') -> c5
EXP(s(z0)) -> c6(DOUBLE(exp(z0)), EXP(z0))
DOUBLE(0') -> c7
DOUBLE(s(z0)) -> c8(DOUBLE(z0))
HALF(0') -> c9(DOUBLE(0'))
HALF(s(0')) -> c10(HALF(0'))
HALF(s(s(z0))) -> c11(HALF(z0))
tower(z0) -> f(a, z0, s(0'))
f(a, 0', z0) -> z0
f(a, s(z0), z1) -> f(b, z1, s(z0))
f(b, z0, z1) -> f(a, half(z1), exp(z0))
exp(0') -> s(0')
exp(s(z0)) -> double(exp(z0))
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
half(0') -> double(0')
half(s(0')) -> half(0')
half(s(s(z0))) -> s(half(z0))

Types:
TOWER :: 0':s -> c
c :: c1:c2:c3:c4 -> c
F :: a:b -> 0':s -> 0':s -> c1:c2:c3:c4
a :: a:b
s :: 0':s -> 0':s
0' :: 0':s
c1 :: c1:c2:c3:c4
c2 :: c1:c2:c3:c4 -> c1:c2:c3:c4
b :: a:b
c3 :: c1:c2:c3:c4 -> c9:c10:c11 -> c1:c2:c3:c4
half :: 0':s -> 0':s
exp :: 0':s -> 0':s
HALF :: 0':s -> c9:c10:c11
c4 :: c1:c2:c3:c4 -> c5:c6 -> c1:c2:c3:c4
EXP :: 0':s -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c5:c6 -> c5:c6
DOUBLE :: 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
c9 :: c7:c8 -> c9:c10:c11
c10 :: c9:c10:c11 -> c9:c10:c11
c11 :: c9:c10:c11 -> c9:c10:c11
tower :: 0':s -> 0':s
f :: a:b -> 0':s -> 0':s -> 0':s
double :: 0':s -> 0':s
hole_c1_12 :: c
hole_0':s2_12 :: 0':s
hole_c1:c2:c3:c43_12 :: c1:c2:c3:c4
hole_a:b4_12 :: a:b
hole_c9:c10:c115_12 :: c9:c10:c11
hole_c5:c66_12 :: c5:c6
hole_c7:c87_12 :: c7:c8
gen_0':s8_12 :: Nat -> 0':s
gen_c1:c2:c3:c49_12 :: Nat -> c1:c2:c3:c4
gen_c9:c10:c1110_12 :: Nat -> c9:c10:c11
gen_c5:c611_12 :: Nat -> c5:c6
gen_c7:c812_12 :: Nat -> c7:c8

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
F, half, exp, HALF, EXP, DOUBLE, f, double

They will be analysed ascendingly in the following order:
half < F
exp < F
HALF < F
EXP < F
half < f
double < half
exp < EXP
exp < f
double < exp
DOUBLE < HALF
DOUBLE < EXP

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

(10)
Obligation:
Innermost TRS:
Rules:
TOWER(z0) -> c(F(a, z0, s(0')))
F(a, 0', z0) -> c1
F(a, s(z0), z1) -> c2(F(b, z1, s(z0)))
F(b, z0, z1) -> c3(F(a, half(z1), exp(z0)), HALF(z1))
F(b, z0, z1) -> c4(F(a, half(z1), exp(z0)), EXP(z0))
EXP(0') -> c5
EXP(s(z0)) -> c6(DOUBLE(exp(z0)), EXP(z0))
DOUBLE(0') -> c7
DOUBLE(s(z0)) -> c8(DOUBLE(z0))
HALF(0') -> c9(DOUBLE(0'))
HALF(s(0')) -> c10(HALF(0'))
HALF(s(s(z0))) -> c11(HALF(z0))
tower(z0) -> f(a, z0, s(0'))
f(a, 0', z0) -> z0
f(a, s(z0), z1) -> f(b, z1, s(z0))
f(b, z0, z1) -> f(a, half(z1), exp(z0))
exp(0') -> s(0')
exp(s(z0)) -> double(exp(z0))
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
half(0') -> double(0')
half(s(0')) -> half(0')
half(s(s(z0))) -> s(half(z0))

Types:
TOWER :: 0':s -> c
c :: c1:c2:c3:c4 -> c
F :: a:b -> 0':s -> 0':s -> c1:c2:c3:c4
a :: a:b
s :: 0':s -> 0':s
0' :: 0':s
c1 :: c1:c2:c3:c4
c2 :: c1:c2:c3:c4 -> c1:c2:c3:c4
b :: a:b
c3 :: c1:c2:c3:c4 -> c9:c10:c11 -> c1:c2:c3:c4
half :: 0':s -> 0':s
exp :: 0':s -> 0':s
HALF :: 0':s -> c9:c10:c11
c4 :: c1:c2:c3:c4 -> c5:c6 -> c1:c2:c3:c4
EXP :: 0':s -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c5:c6 -> c5:c6
DOUBLE :: 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
c9 :: c7:c8 -> c9:c10:c11
c10 :: c9:c10:c11 -> c9:c10:c11
c11 :: c9:c10:c11 -> c9:c10:c11
tower :: 0':s -> 0':s
f :: a:b -> 0':s -> 0':s -> 0':s
double :: 0':s -> 0':s
hole_c1_12 :: c
hole_0':s2_12 :: 0':s
hole_c1:c2:c3:c43_12 :: c1:c2:c3:c4
hole_a:b4_12 :: a:b
hole_c9:c10:c115_12 :: c9:c10:c11
hole_c5:c66_12 :: c5:c6
hole_c7:c87_12 :: c7:c8
gen_0':s8_12 :: Nat -> 0':s
gen_c1:c2:c3:c49_12 :: Nat -> c1:c2:c3:c4
gen_c9:c10:c1110_12 :: Nat -> c9:c10:c11
gen_c5:c611_12 :: Nat -> c5:c6
gen_c7:c812_12 :: Nat -> c7:c8


Generator Equations:
gen_0':s8_12(0) <=> 0'
gen_0':s8_12(+(x, 1)) <=> s(gen_0':s8_12(x))
gen_c1:c2:c3:c49_12(0) <=> c1
gen_c1:c2:c3:c49_12(+(x, 1)) <=> c2(gen_c1:c2:c3:c49_12(x))
gen_c9:c10:c1110_12(0) <=> c9(c7)
gen_c9:c10:c1110_12(+(x, 1)) <=> c10(gen_c9:c10:c1110_12(x))
gen_c5:c611_12(0) <=> c5
gen_c5:c611_12(+(x, 1)) <=> c6(c7, gen_c5:c611_12(x))
gen_c7:c812_12(0) <=> c7
gen_c7:c812_12(+(x, 1)) <=> c8(gen_c7:c812_12(x))


The following defined symbols remain to be analysed:
DOUBLE, F, half, exp, HALF, EXP, f, double

They will be analysed ascendingly in the following order:
half < F
exp < F
HALF < F
EXP < F
half < f
double < half
exp < EXP
exp < f
double < exp
DOUBLE < HALF
DOUBLE < EXP

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
DOUBLE(gen_0':s8_12(n14_12)) -> gen_c7:c812_12(n14_12), rt in Omega(1 + n14_12)

Induction Base:
DOUBLE(gen_0':s8_12(0)) ->_R^Omega(1)
c7

Induction Step:
DOUBLE(gen_0':s8_12(+(n14_12, 1))) ->_R^Omega(1)
c8(DOUBLE(gen_0':s8_12(n14_12))) ->_IH
c8(gen_c7:c812_12(c15_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:
TOWER(z0) -> c(F(a, z0, s(0')))
F(a, 0', z0) -> c1
F(a, s(z0), z1) -> c2(F(b, z1, s(z0)))
F(b, z0, z1) -> c3(F(a, half(z1), exp(z0)), HALF(z1))
F(b, z0, z1) -> c4(F(a, half(z1), exp(z0)), EXP(z0))
EXP(0') -> c5
EXP(s(z0)) -> c6(DOUBLE(exp(z0)), EXP(z0))
DOUBLE(0') -> c7
DOUBLE(s(z0)) -> c8(DOUBLE(z0))
HALF(0') -> c9(DOUBLE(0'))
HALF(s(0')) -> c10(HALF(0'))
HALF(s(s(z0))) -> c11(HALF(z0))
tower(z0) -> f(a, z0, s(0'))
f(a, 0', z0) -> z0
f(a, s(z0), z1) -> f(b, z1, s(z0))
f(b, z0, z1) -> f(a, half(z1), exp(z0))
exp(0') -> s(0')
exp(s(z0)) -> double(exp(z0))
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
half(0') -> double(0')
half(s(0')) -> half(0')
half(s(s(z0))) -> s(half(z0))

Types:
TOWER :: 0':s -> c
c :: c1:c2:c3:c4 -> c
F :: a:b -> 0':s -> 0':s -> c1:c2:c3:c4
a :: a:b
s :: 0':s -> 0':s
0' :: 0':s
c1 :: c1:c2:c3:c4
c2 :: c1:c2:c3:c4 -> c1:c2:c3:c4
b :: a:b
c3 :: c1:c2:c3:c4 -> c9:c10:c11 -> c1:c2:c3:c4
half :: 0':s -> 0':s
exp :: 0':s -> 0':s
HALF :: 0':s -> c9:c10:c11
c4 :: c1:c2:c3:c4 -> c5:c6 -> c1:c2:c3:c4
EXP :: 0':s -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c5:c6 -> c5:c6
DOUBLE :: 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
c9 :: c7:c8 -> c9:c10:c11
c10 :: c9:c10:c11 -> c9:c10:c11
c11 :: c9:c10:c11 -> c9:c10:c11
tower :: 0':s -> 0':s
f :: a:b -> 0':s -> 0':s -> 0':s
double :: 0':s -> 0':s
hole_c1_12 :: c
hole_0':s2_12 :: 0':s
hole_c1:c2:c3:c43_12 :: c1:c2:c3:c4
hole_a:b4_12 :: a:b
hole_c9:c10:c115_12 :: c9:c10:c11
hole_c5:c66_12 :: c5:c6
hole_c7:c87_12 :: c7:c8
gen_0':s8_12 :: Nat -> 0':s
gen_c1:c2:c3:c49_12 :: Nat -> c1:c2:c3:c4
gen_c9:c10:c1110_12 :: Nat -> c9:c10:c11
gen_c5:c611_12 :: Nat -> c5:c6
gen_c7:c812_12 :: Nat -> c7:c8


Generator Equations:
gen_0':s8_12(0) <=> 0'
gen_0':s8_12(+(x, 1)) <=> s(gen_0':s8_12(x))
gen_c1:c2:c3:c49_12(0) <=> c1
gen_c1:c2:c3:c49_12(+(x, 1)) <=> c2(gen_c1:c2:c3:c49_12(x))
gen_c9:c10:c1110_12(0) <=> c9(c7)
gen_c9:c10:c1110_12(+(x, 1)) <=> c10(gen_c9:c10:c1110_12(x))
gen_c5:c611_12(0) <=> c5
gen_c5:c611_12(+(x, 1)) <=> c6(c7, gen_c5:c611_12(x))
gen_c7:c812_12(0) <=> c7
gen_c7:c812_12(+(x, 1)) <=> c8(gen_c7:c812_12(x))


The following defined symbols remain to be analysed:
DOUBLE, F, half, exp, HALF, EXP, f, double

They will be analysed ascendingly in the following order:
half < F
exp < F
HALF < F
EXP < F
half < f
double < half
exp < EXP
exp < f
double < exp
DOUBLE < HALF
DOUBLE < EXP

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
TOWER(z0) -> c(F(a, z0, s(0')))
F(a, 0', z0) -> c1
F(a, s(z0), z1) -> c2(F(b, z1, s(z0)))
F(b, z0, z1) -> c3(F(a, half(z1), exp(z0)), HALF(z1))
F(b, z0, z1) -> c4(F(a, half(z1), exp(z0)), EXP(z0))
EXP(0') -> c5
EXP(s(z0)) -> c6(DOUBLE(exp(z0)), EXP(z0))
DOUBLE(0') -> c7
DOUBLE(s(z0)) -> c8(DOUBLE(z0))
HALF(0') -> c9(DOUBLE(0'))
HALF(s(0')) -> c10(HALF(0'))
HALF(s(s(z0))) -> c11(HALF(z0))
tower(z0) -> f(a, z0, s(0'))
f(a, 0', z0) -> z0
f(a, s(z0), z1) -> f(b, z1, s(z0))
f(b, z0, z1) -> f(a, half(z1), exp(z0))
exp(0') -> s(0')
exp(s(z0)) -> double(exp(z0))
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
half(0') -> double(0')
half(s(0')) -> half(0')
half(s(s(z0))) -> s(half(z0))

Types:
TOWER :: 0':s -> c
c :: c1:c2:c3:c4 -> c
F :: a:b -> 0':s -> 0':s -> c1:c2:c3:c4
a :: a:b
s :: 0':s -> 0':s
0' :: 0':s
c1 :: c1:c2:c3:c4
c2 :: c1:c2:c3:c4 -> c1:c2:c3:c4
b :: a:b
c3 :: c1:c2:c3:c4 -> c9:c10:c11 -> c1:c2:c3:c4
half :: 0':s -> 0':s
exp :: 0':s -> 0':s
HALF :: 0':s -> c9:c10:c11
c4 :: c1:c2:c3:c4 -> c5:c6 -> c1:c2:c3:c4
EXP :: 0':s -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c5:c6 -> c5:c6
DOUBLE :: 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
c9 :: c7:c8 -> c9:c10:c11
c10 :: c9:c10:c11 -> c9:c10:c11
c11 :: c9:c10:c11 -> c9:c10:c11
tower :: 0':s -> 0':s
f :: a:b -> 0':s -> 0':s -> 0':s
double :: 0':s -> 0':s
hole_c1_12 :: c
hole_0':s2_12 :: 0':s
hole_c1:c2:c3:c43_12 :: c1:c2:c3:c4
hole_a:b4_12 :: a:b
hole_c9:c10:c115_12 :: c9:c10:c11
hole_c5:c66_12 :: c5:c6
hole_c7:c87_12 :: c7:c8
gen_0':s8_12 :: Nat -> 0':s
gen_c1:c2:c3:c49_12 :: Nat -> c1:c2:c3:c4
gen_c9:c10:c1110_12 :: Nat -> c9:c10:c11
gen_c5:c611_12 :: Nat -> c5:c6
gen_c7:c812_12 :: Nat -> c7:c8


Lemmas:
DOUBLE(gen_0':s8_12(n14_12)) -> gen_c7:c812_12(n14_12), rt in Omega(1 + n14_12)


Generator Equations:
gen_0':s8_12(0) <=> 0'
gen_0':s8_12(+(x, 1)) <=> s(gen_0':s8_12(x))
gen_c1:c2:c3:c49_12(0) <=> c1
gen_c1:c2:c3:c49_12(+(x, 1)) <=> c2(gen_c1:c2:c3:c49_12(x))
gen_c9:c10:c1110_12(0) <=> c9(c7)
gen_c9:c10:c1110_12(+(x, 1)) <=> c10(gen_c9:c10:c1110_12(x))
gen_c5:c611_12(0) <=> c5
gen_c5:c611_12(+(x, 1)) <=> c6(c7, gen_c5:c611_12(x))
gen_c7:c812_12(0) <=> c7
gen_c7:c812_12(+(x, 1)) <=> c8(gen_c7:c812_12(x))


The following defined symbols remain to be analysed:
HALF, F, half, exp, EXP, f, double

They will be analysed ascendingly in the following order:
half < F
exp < F
HALF < F
EXP < F
half < f
double < half
exp < EXP
exp < f
double < exp

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
HALF(gen_0':s8_12(+(2, *(2, n455_12)))) -> *13_12, rt in Omega(n455_12)

Induction Base:
HALF(gen_0':s8_12(+(2, *(2, 0))))

Induction Step:
HALF(gen_0':s8_12(+(2, *(2, +(n455_12, 1))))) ->_R^Omega(1)
c11(HALF(gen_0':s8_12(+(2, *(2, n455_12))))) ->_IH
c11(*13_12)

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:
TOWER(z0) -> c(F(a, z0, s(0')))
F(a, 0', z0) -> c1
F(a, s(z0), z1) -> c2(F(b, z1, s(z0)))
F(b, z0, z1) -> c3(F(a, half(z1), exp(z0)), HALF(z1))
F(b, z0, z1) -> c4(F(a, half(z1), exp(z0)), EXP(z0))
EXP(0') -> c5
EXP(s(z0)) -> c6(DOUBLE(exp(z0)), EXP(z0))
DOUBLE(0') -> c7
DOUBLE(s(z0)) -> c8(DOUBLE(z0))
HALF(0') -> c9(DOUBLE(0'))
HALF(s(0')) -> c10(HALF(0'))
HALF(s(s(z0))) -> c11(HALF(z0))
tower(z0) -> f(a, z0, s(0'))
f(a, 0', z0) -> z0
f(a, s(z0), z1) -> f(b, z1, s(z0))
f(b, z0, z1) -> f(a, half(z1), exp(z0))
exp(0') -> s(0')
exp(s(z0)) -> double(exp(z0))
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
half(0') -> double(0')
half(s(0')) -> half(0')
half(s(s(z0))) -> s(half(z0))

Types:
TOWER :: 0':s -> c
c :: c1:c2:c3:c4 -> c
F :: a:b -> 0':s -> 0':s -> c1:c2:c3:c4
a :: a:b
s :: 0':s -> 0':s
0' :: 0':s
c1 :: c1:c2:c3:c4
c2 :: c1:c2:c3:c4 -> c1:c2:c3:c4
b :: a:b
c3 :: c1:c2:c3:c4 -> c9:c10:c11 -> c1:c2:c3:c4
half :: 0':s -> 0':s
exp :: 0':s -> 0':s
HALF :: 0':s -> c9:c10:c11
c4 :: c1:c2:c3:c4 -> c5:c6 -> c1:c2:c3:c4
EXP :: 0':s -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c5:c6 -> c5:c6
DOUBLE :: 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
c9 :: c7:c8 -> c9:c10:c11
c10 :: c9:c10:c11 -> c9:c10:c11
c11 :: c9:c10:c11 -> c9:c10:c11
tower :: 0':s -> 0':s
f :: a:b -> 0':s -> 0':s -> 0':s
double :: 0':s -> 0':s
hole_c1_12 :: c
hole_0':s2_12 :: 0':s
hole_c1:c2:c3:c43_12 :: c1:c2:c3:c4
hole_a:b4_12 :: a:b
hole_c9:c10:c115_12 :: c9:c10:c11
hole_c5:c66_12 :: c5:c6
hole_c7:c87_12 :: c7:c8
gen_0':s8_12 :: Nat -> 0':s
gen_c1:c2:c3:c49_12 :: Nat -> c1:c2:c3:c4
gen_c9:c10:c1110_12 :: Nat -> c9:c10:c11
gen_c5:c611_12 :: Nat -> c5:c6
gen_c7:c812_12 :: Nat -> c7:c8


Lemmas:
DOUBLE(gen_0':s8_12(n14_12)) -> gen_c7:c812_12(n14_12), rt in Omega(1 + n14_12)
HALF(gen_0':s8_12(+(2, *(2, n455_12)))) -> *13_12, rt in Omega(n455_12)


Generator Equations:
gen_0':s8_12(0) <=> 0'
gen_0':s8_12(+(x, 1)) <=> s(gen_0':s8_12(x))
gen_c1:c2:c3:c49_12(0) <=> c1
gen_c1:c2:c3:c49_12(+(x, 1)) <=> c2(gen_c1:c2:c3:c49_12(x))
gen_c9:c10:c1110_12(0) <=> c9(c7)
gen_c9:c10:c1110_12(+(x, 1)) <=> c10(gen_c9:c10:c1110_12(x))
gen_c5:c611_12(0) <=> c5
gen_c5:c611_12(+(x, 1)) <=> c6(c7, gen_c5:c611_12(x))
gen_c7:c812_12(0) <=> c7
gen_c7:c812_12(+(x, 1)) <=> c8(gen_c7:c812_12(x))


The following defined symbols remain to be analysed:
double, F, half, exp, EXP, f

They will be analysed ascendingly in the following order:
half < F
exp < F
EXP < F
half < f
double < half
exp < EXP
exp < f
double < exp

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
double(gen_0':s8_12(n6591_12)) -> gen_0':s8_12(*(2, n6591_12)), rt in Omega(0)

Induction Base:
double(gen_0':s8_12(0)) ->_R^Omega(0)
0'

Induction Step:
double(gen_0':s8_12(+(n6591_12, 1))) ->_R^Omega(0)
s(s(double(gen_0':s8_12(n6591_12)))) ->_IH
s(s(gen_0':s8_12(*(2, c6592_12))))

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:
TOWER(z0) -> c(F(a, z0, s(0')))
F(a, 0', z0) -> c1
F(a, s(z0), z1) -> c2(F(b, z1, s(z0)))
F(b, z0, z1) -> c3(F(a, half(z1), exp(z0)), HALF(z1))
F(b, z0, z1) -> c4(F(a, half(z1), exp(z0)), EXP(z0))
EXP(0') -> c5
EXP(s(z0)) -> c6(DOUBLE(exp(z0)), EXP(z0))
DOUBLE(0') -> c7
DOUBLE(s(z0)) -> c8(DOUBLE(z0))
HALF(0') -> c9(DOUBLE(0'))
HALF(s(0')) -> c10(HALF(0'))
HALF(s(s(z0))) -> c11(HALF(z0))
tower(z0) -> f(a, z0, s(0'))
f(a, 0', z0) -> z0
f(a, s(z0), z1) -> f(b, z1, s(z0))
f(b, z0, z1) -> f(a, half(z1), exp(z0))
exp(0') -> s(0')
exp(s(z0)) -> double(exp(z0))
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
half(0') -> double(0')
half(s(0')) -> half(0')
half(s(s(z0))) -> s(half(z0))

Types:
TOWER :: 0':s -> c
c :: c1:c2:c3:c4 -> c
F :: a:b -> 0':s -> 0':s -> c1:c2:c3:c4
a :: a:b
s :: 0':s -> 0':s
0' :: 0':s
c1 :: c1:c2:c3:c4
c2 :: c1:c2:c3:c4 -> c1:c2:c3:c4
b :: a:b
c3 :: c1:c2:c3:c4 -> c9:c10:c11 -> c1:c2:c3:c4
half :: 0':s -> 0':s
exp :: 0':s -> 0':s
HALF :: 0':s -> c9:c10:c11
c4 :: c1:c2:c3:c4 -> c5:c6 -> c1:c2:c3:c4
EXP :: 0':s -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c5:c6 -> c5:c6
DOUBLE :: 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
c9 :: c7:c8 -> c9:c10:c11
c10 :: c9:c10:c11 -> c9:c10:c11
c11 :: c9:c10:c11 -> c9:c10:c11
tower :: 0':s -> 0':s
f :: a:b -> 0':s -> 0':s -> 0':s
double :: 0':s -> 0':s
hole_c1_12 :: c
hole_0':s2_12 :: 0':s
hole_c1:c2:c3:c43_12 :: c1:c2:c3:c4
hole_a:b4_12 :: a:b
hole_c9:c10:c115_12 :: c9:c10:c11
hole_c5:c66_12 :: c5:c6
hole_c7:c87_12 :: c7:c8
gen_0':s8_12 :: Nat -> 0':s
gen_c1:c2:c3:c49_12 :: Nat -> c1:c2:c3:c4
gen_c9:c10:c1110_12 :: Nat -> c9:c10:c11
gen_c5:c611_12 :: Nat -> c5:c6
gen_c7:c812_12 :: Nat -> c7:c8


Lemmas:
DOUBLE(gen_0':s8_12(n14_12)) -> gen_c7:c812_12(n14_12), rt in Omega(1 + n14_12)
HALF(gen_0':s8_12(+(2, *(2, n455_12)))) -> *13_12, rt in Omega(n455_12)
double(gen_0':s8_12(n6591_12)) -> gen_0':s8_12(*(2, n6591_12)), rt in Omega(0)


Generator Equations:
gen_0':s8_12(0) <=> 0'
gen_0':s8_12(+(x, 1)) <=> s(gen_0':s8_12(x))
gen_c1:c2:c3:c49_12(0) <=> c1
gen_c1:c2:c3:c49_12(+(x, 1)) <=> c2(gen_c1:c2:c3:c49_12(x))
gen_c9:c10:c1110_12(0) <=> c9(c7)
gen_c9:c10:c1110_12(+(x, 1)) <=> c10(gen_c9:c10:c1110_12(x))
gen_c5:c611_12(0) <=> c5
gen_c5:c611_12(+(x, 1)) <=> c6(c7, gen_c5:c611_12(x))
gen_c7:c812_12(0) <=> c7
gen_c7:c812_12(+(x, 1)) <=> c8(gen_c7:c812_12(x))


The following defined symbols remain to be analysed:
half, F, exp, EXP, f

They will be analysed ascendingly in the following order:
half < F
exp < F
EXP < F
half < f
exp < EXP
exp < f

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
half(gen_0':s8_12(*(2, n7053_12))) -> gen_0':s8_12(n7053_12), rt in Omega(0)

Induction Base:
half(gen_0':s8_12(*(2, 0))) ->_R^Omega(0)
double(0') ->_L^Omega(0)
gen_0':s8_12(*(2, 0))

Induction Step:
half(gen_0':s8_12(*(2, +(n7053_12, 1)))) ->_R^Omega(0)
s(half(gen_0':s8_12(*(2, n7053_12)))) ->_IH
s(gen_0':s8_12(c7054_12))

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:
TOWER(z0) -> c(F(a, z0, s(0')))
F(a, 0', z0) -> c1
F(a, s(z0), z1) -> c2(F(b, z1, s(z0)))
F(b, z0, z1) -> c3(F(a, half(z1), exp(z0)), HALF(z1))
F(b, z0, z1) -> c4(F(a, half(z1), exp(z0)), EXP(z0))
EXP(0') -> c5
EXP(s(z0)) -> c6(DOUBLE(exp(z0)), EXP(z0))
DOUBLE(0') -> c7
DOUBLE(s(z0)) -> c8(DOUBLE(z0))
HALF(0') -> c9(DOUBLE(0'))
HALF(s(0')) -> c10(HALF(0'))
HALF(s(s(z0))) -> c11(HALF(z0))
tower(z0) -> f(a, z0, s(0'))
f(a, 0', z0) -> z0
f(a, s(z0), z1) -> f(b, z1, s(z0))
f(b, z0, z1) -> f(a, half(z1), exp(z0))
exp(0') -> s(0')
exp(s(z0)) -> double(exp(z0))
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
half(0') -> double(0')
half(s(0')) -> half(0')
half(s(s(z0))) -> s(half(z0))

Types:
TOWER :: 0':s -> c
c :: c1:c2:c3:c4 -> c
F :: a:b -> 0':s -> 0':s -> c1:c2:c3:c4
a :: a:b
s :: 0':s -> 0':s
0' :: 0':s
c1 :: c1:c2:c3:c4
c2 :: c1:c2:c3:c4 -> c1:c2:c3:c4
b :: a:b
c3 :: c1:c2:c3:c4 -> c9:c10:c11 -> c1:c2:c3:c4
half :: 0':s -> 0':s
exp :: 0':s -> 0':s
HALF :: 0':s -> c9:c10:c11
c4 :: c1:c2:c3:c4 -> c5:c6 -> c1:c2:c3:c4
EXP :: 0':s -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c5:c6 -> c5:c6
DOUBLE :: 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
c9 :: c7:c8 -> c9:c10:c11
c10 :: c9:c10:c11 -> c9:c10:c11
c11 :: c9:c10:c11 -> c9:c10:c11
tower :: 0':s -> 0':s
f :: a:b -> 0':s -> 0':s -> 0':s
double :: 0':s -> 0':s
hole_c1_12 :: c
hole_0':s2_12 :: 0':s
hole_c1:c2:c3:c43_12 :: c1:c2:c3:c4
hole_a:b4_12 :: a:b
hole_c9:c10:c115_12 :: c9:c10:c11
hole_c5:c66_12 :: c5:c6
hole_c7:c87_12 :: c7:c8
gen_0':s8_12 :: Nat -> 0':s
gen_c1:c2:c3:c49_12 :: Nat -> c1:c2:c3:c4
gen_c9:c10:c1110_12 :: Nat -> c9:c10:c11
gen_c5:c611_12 :: Nat -> c5:c6
gen_c7:c812_12 :: Nat -> c7:c8


Lemmas:
DOUBLE(gen_0':s8_12(n14_12)) -> gen_c7:c812_12(n14_12), rt in Omega(1 + n14_12)
HALF(gen_0':s8_12(+(2, *(2, n455_12)))) -> *13_12, rt in Omega(n455_12)
double(gen_0':s8_12(n6591_12)) -> gen_0':s8_12(*(2, n6591_12)), rt in Omega(0)
half(gen_0':s8_12(*(2, n7053_12))) -> gen_0':s8_12(n7053_12), rt in Omega(0)


Generator Equations:
gen_0':s8_12(0) <=> 0'
gen_0':s8_12(+(x, 1)) <=> s(gen_0':s8_12(x))
gen_c1:c2:c3:c49_12(0) <=> c1
gen_c1:c2:c3:c49_12(+(x, 1)) <=> c2(gen_c1:c2:c3:c49_12(x))
gen_c9:c10:c1110_12(0) <=> c9(c7)
gen_c9:c10:c1110_12(+(x, 1)) <=> c10(gen_c9:c10:c1110_12(x))
gen_c5:c611_12(0) <=> c5
gen_c5:c611_12(+(x, 1)) <=> c6(c7, gen_c5:c611_12(x))
gen_c7:c812_12(0) <=> c7
gen_c7:c812_12(+(x, 1)) <=> c8(gen_c7:c812_12(x))


The following defined symbols remain to be analysed:
exp, F, EXP, f

They will be analysed ascendingly in the following order:
exp < F
EXP < F
exp < EXP
exp < f

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
exp(gen_0':s8_12(+(1, n7675_12))) -> *13_12, rt in Omega(0)

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

Induction Step:
exp(gen_0':s8_12(+(1, +(n7675_12, 1)))) ->_R^Omega(0)
double(exp(gen_0':s8_12(+(1, n7675_12)))) ->_IH
double(*13_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:
TOWER(z0) -> c(F(a, z0, s(0')))
F(a, 0', z0) -> c1
F(a, s(z0), z1) -> c2(F(b, z1, s(z0)))
F(b, z0, z1) -> c3(F(a, half(z1), exp(z0)), HALF(z1))
F(b, z0, z1) -> c4(F(a, half(z1), exp(z0)), EXP(z0))
EXP(0') -> c5
EXP(s(z0)) -> c6(DOUBLE(exp(z0)), EXP(z0))
DOUBLE(0') -> c7
DOUBLE(s(z0)) -> c8(DOUBLE(z0))
HALF(0') -> c9(DOUBLE(0'))
HALF(s(0')) -> c10(HALF(0'))
HALF(s(s(z0))) -> c11(HALF(z0))
tower(z0) -> f(a, z0, s(0'))
f(a, 0', z0) -> z0
f(a, s(z0), z1) -> f(b, z1, s(z0))
f(b, z0, z1) -> f(a, half(z1), exp(z0))
exp(0') -> s(0')
exp(s(z0)) -> double(exp(z0))
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
half(0') -> double(0')
half(s(0')) -> half(0')
half(s(s(z0))) -> s(half(z0))

Types:
TOWER :: 0':s -> c
c :: c1:c2:c3:c4 -> c
F :: a:b -> 0':s -> 0':s -> c1:c2:c3:c4
a :: a:b
s :: 0':s -> 0':s
0' :: 0':s
c1 :: c1:c2:c3:c4
c2 :: c1:c2:c3:c4 -> c1:c2:c3:c4
b :: a:b
c3 :: c1:c2:c3:c4 -> c9:c10:c11 -> c1:c2:c3:c4
half :: 0':s -> 0':s
exp :: 0':s -> 0':s
HALF :: 0':s -> c9:c10:c11
c4 :: c1:c2:c3:c4 -> c5:c6 -> c1:c2:c3:c4
EXP :: 0':s -> c5:c6
c5 :: c5:c6
c6 :: c7:c8 -> c5:c6 -> c5:c6
DOUBLE :: 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
c9 :: c7:c8 -> c9:c10:c11
c10 :: c9:c10:c11 -> c9:c10:c11
c11 :: c9:c10:c11 -> c9:c10:c11
tower :: 0':s -> 0':s
f :: a:b -> 0':s -> 0':s -> 0':s
double :: 0':s -> 0':s
hole_c1_12 :: c
hole_0':s2_12 :: 0':s
hole_c1:c2:c3:c43_12 :: c1:c2:c3:c4
hole_a:b4_12 :: a:b
hole_c9:c10:c115_12 :: c9:c10:c11
hole_c5:c66_12 :: c5:c6
hole_c7:c87_12 :: c7:c8
gen_0':s8_12 :: Nat -> 0':s
gen_c1:c2:c3:c49_12 :: Nat -> c1:c2:c3:c4
gen_c9:c10:c1110_12 :: Nat -> c9:c10:c11
gen_c5:c611_12 :: Nat -> c5:c6
gen_c7:c812_12 :: Nat -> c7:c8


Lemmas:
DOUBLE(gen_0':s8_12(n14_12)) -> gen_c7:c812_12(n14_12), rt in Omega(1 + n14_12)
HALF(gen_0':s8_12(+(2, *(2, n455_12)))) -> *13_12, rt in Omega(n455_12)
double(gen_0':s8_12(n6591_12)) -> gen_0':s8_12(*(2, n6591_12)), rt in Omega(0)
half(gen_0':s8_12(*(2, n7053_12))) -> gen_0':s8_12(n7053_12), rt in Omega(0)
exp(gen_0':s8_12(+(1, n7675_12))) -> *13_12, rt in Omega(0)


Generator Equations:
gen_0':s8_12(0) <=> 0'
gen_0':s8_12(+(x, 1)) <=> s(gen_0':s8_12(x))
gen_c1:c2:c3:c49_12(0) <=> c1
gen_c1:c2:c3:c49_12(+(x, 1)) <=> c2(gen_c1:c2:c3:c49_12(x))
gen_c9:c10:c1110_12(0) <=> c9(c7)
gen_c9:c10:c1110_12(+(x, 1)) <=> c10(gen_c9:c10:c1110_12(x))
gen_c5:c611_12(0) <=> c5
gen_c5:c611_12(+(x, 1)) <=> c6(c7, gen_c5:c611_12(x))
gen_c7:c812_12(0) <=> c7
gen_c7:c812_12(+(x, 1)) <=> c8(gen_c7:c812_12(x))


The following defined symbols remain to be analysed:
EXP, F, f

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