WORST_CASE(Omega(n^2),?)
proof of input_qdtVryQweE.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), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 9 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 379 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), 65 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 61 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 64 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 95 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 732 ms]
        (26) BEST
            (27) proven lower bound
                (28) LowerBoundPropagationProof [FINISHED, 0 ms]
                (29) BOUNDS(n^2, INF)
            (30) 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:

   le(s(x), 0) -> false
   le(0, y) -> true
   le(s(x), s(y)) -> le(x, y)
   plus(0, y) -> y
   plus(s(x), y) -> s(plus(x, y))
   times(0, y) -> 0
   times(s(x), y) -> plus(y, times(x, y))
   log(x, 0) -> baseError
   log(x, s(0)) -> baseError
   log(0, s(s(b))) -> logZeroError
   log(s(x), s(s(b))) -> loop(s(x), s(s(b)), s(0), 0)
   loop(x, s(s(b)), s(y), z) -> if(le(x, s(y)), x, s(s(b)), s(y), z)
   if(true, x, b, y, z) -> z
   if(false, x, b, y, z) -> loop(x, b, times(b, y), s(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:
   le(s(z0), 0) -> false
   le(0, z0) -> true
   le(s(z0), s(z1)) -> le(z0, z1)
   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))
   log(z0, 0) -> baseError
   log(z0, s(0)) -> baseError
   log(0, s(s(z0))) -> logZeroError
   log(s(z0), s(s(z1))) -> loop(s(z0), s(s(z1)), s(0), 0)
   loop(z0, s(s(z1)), s(z2), z3) -> if(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3)
   if(true, z0, z1, z2, z3) -> z3
   if(false, z0, z1, z2, z3) -> loop(z0, z1, times(z1, z2), s(z3))
Tuples:
   LE(s(z0), 0) -> c
   LE(0, z0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   PLUS(0, z0) -> c3
   PLUS(s(z0), z1) -> c4(PLUS(z0, z1))
   TIMES(0, z0) -> c5
   TIMES(s(z0), z1) -> c6(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   LOG(z0, 0) -> c7
   LOG(z0, s(0)) -> c8
   LOG(0, s(s(z0))) -> c9
   LOG(s(z0), s(s(z1))) -> c10(LOOP(s(z0), s(s(z1)), s(0), 0))
   LOOP(z0, s(s(z1)), s(z2), z3) -> c11(IF(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3), LE(z0, s(z2)))
   IF(true, z0, z1, z2, z3) -> c12
   IF(false, z0, z1, z2, z3) -> c13(LOOP(z0, z1, times(z1, z2), s(z3)), TIMES(z1, z2))
S tuples:
   LE(s(z0), 0) -> c
   LE(0, z0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   PLUS(0, z0) -> c3
   PLUS(s(z0), z1) -> c4(PLUS(z0, z1))
   TIMES(0, z0) -> c5
   TIMES(s(z0), z1) -> c6(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   LOG(z0, 0) -> c7
   LOG(z0, s(0)) -> c8
   LOG(0, s(s(z0))) -> c9
   LOG(s(z0), s(s(z1))) -> c10(LOOP(s(z0), s(s(z1)), s(0), 0))
   LOOP(z0, s(s(z1)), s(z2), z3) -> c11(IF(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3), LE(z0, s(z2)))
   IF(true, z0, z1, z2, z3) -> c12
   IF(false, z0, z1, z2, z3) -> c13(LOOP(z0, z1, times(z1, z2), s(z3)), TIMES(z1, z2))
K tuples:none
Defined Rule Symbols:   le_2, plus_2, times_2, log_2, loop_4, if_5

Defined Pair Symbols:   LE_2, PLUS_2, TIMES_2, LOG_2, LOOP_4, IF_5

Compound Symbols:   c, c1, c2_1, c3, c4_1, c5, c6_2, c7, c8, c9, c10_1, c11_2, c12, c13_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:

   LE(s(z0), 0) -> c
   LE(0, z0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   PLUS(0, z0) -> c3
   PLUS(s(z0), z1) -> c4(PLUS(z0, z1))
   TIMES(0, z0) -> c5
   TIMES(s(z0), z1) -> c6(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   LOG(z0, 0) -> c7
   LOG(z0, s(0)) -> c8
   LOG(0, s(s(z0))) -> c9
   LOG(s(z0), s(s(z1))) -> c10(LOOP(s(z0), s(s(z1)), s(0), 0))
   LOOP(z0, s(s(z1)), s(z2), z3) -> c11(IF(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3), LE(z0, s(z2)))
   IF(true, z0, z1, z2, z3) -> c12
   IF(false, z0, z1, z2, z3) -> c13(LOOP(z0, z1, times(z1, z2), s(z3)), TIMES(z1, z2))

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

   le(s(z0), 0) -> false
   le(0, z0) -> true
   le(s(z0), s(z1)) -> le(z0, z1)
   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))
   log(z0, 0) -> baseError
   log(z0, s(0)) -> baseError
   log(0, s(s(z0))) -> logZeroError
   log(s(z0), s(s(z1))) -> loop(s(z0), s(s(z1)), s(0), 0)
   loop(z0, s(s(z1)), s(z2), z3) -> if(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3)
   if(true, z0, z1, z2, z3) -> z3
   if(false, z0, z1, z2, z3) -> loop(z0, z1, times(z1, z2), s(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:

   LE(s(z0), 0') -> c
   LE(0', z0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   PLUS(0', z0) -> c3
   PLUS(s(z0), z1) -> c4(PLUS(z0, z1))
   TIMES(0', z0) -> c5
   TIMES(s(z0), z1) -> c6(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   LOG(z0, 0') -> c7
   LOG(z0, s(0')) -> c8
   LOG(0', s(s(z0))) -> c9
   LOG(s(z0), s(s(z1))) -> c10(LOOP(s(z0), s(s(z1)), s(0'), 0'))
   LOOP(z0, s(s(z1)), s(z2), z3) -> c11(IF(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3), LE(z0, s(z2)))
   IF(true, z0, z1, z2, z3) -> c12
   IF(false, z0, z1, z2, z3) -> c13(LOOP(z0, z1, times(z1, z2), s(z3)), TIMES(z1, z2))

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

   le(s(z0), 0') -> false
   le(0', z0) -> true
   le(s(z0), s(z1)) -> le(z0, z1)
   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))
   log(z0, 0') -> baseError
   log(z0, s(0')) -> baseError
   log(0', s(s(z0))) -> logZeroError
   log(s(z0), s(s(z1))) -> loop(s(z0), s(s(z1)), s(0'), 0')
   loop(z0, s(s(z1)), s(z2), z3) -> if(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3)
   if(true, z0, z1, z2, z3) -> z3
   if(false, z0, z1, z2, z3) -> loop(z0, z1, times(z1, z2), s(z3))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
LE(s(z0), 0') -> c
LE(0', z0) -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
PLUS(0', z0) -> c3
PLUS(s(z0), z1) -> c4(PLUS(z0, z1))
TIMES(0', z0) -> c5
TIMES(s(z0), z1) -> c6(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
LOG(z0, 0') -> c7
LOG(z0, s(0')) -> c8
LOG(0', s(s(z0))) -> c9
LOG(s(z0), s(s(z1))) -> c10(LOOP(s(z0), s(s(z1)), s(0'), 0'))
LOOP(z0, s(s(z1)), s(z2), z3) -> c11(IF(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3), LE(z0, s(z2)))
IF(true, z0, z1, z2, z3) -> c12
IF(false, z0, z1, z2, z3) -> c13(LOOP(z0, z1, times(z1, z2), s(z3)), TIMES(z1, z2))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
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))
log(z0, 0') -> baseError
log(z0, s(0')) -> baseError
log(0', s(s(z0))) -> logZeroError
log(s(z0), s(s(z1))) -> loop(s(z0), s(s(z1)), s(0'), 0')
loop(z0, s(s(z1)), s(z2), z3) -> if(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3)
if(true, z0, z1, z2, z3) -> z3
if(false, z0, z1, z2, z3) -> loop(z0, z1, times(z1, z2), s(z3))

Types:
LE :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c:c1:c2
s :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError
0' :: s:0':baseError:logZeroError
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
PLUS :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
TIMES :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c5:c6
c5 :: c5:c6
c6 :: c3:c4 -> c5:c6 -> c5:c6
times :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
LOG :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c7:c8:c9:c10
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c7:c8:c9:c10
c10 :: c11 -> c7:c8:c9:c10
LOOP :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c11
c11 :: c12:c13 -> c:c1:c2 -> c11
IF :: true:false -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c12:c13
le :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> true:false
true :: true:false
c12 :: c12:c13
false :: true:false
c13 :: c11 -> c5:c6 -> c12:c13
plus :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
log :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
baseError :: s:0':baseError:logZeroError
logZeroError :: s:0':baseError:logZeroError
loop :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
if :: true:false -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
hole_c:c1:c21_14 :: c:c1:c2
hole_s:0':baseError:logZeroError2_14 :: s:0':baseError:logZeroError
hole_c3:c43_14 :: c3:c4
hole_c5:c64_14 :: c5:c6
hole_c7:c8:c9:c105_14 :: c7:c8:c9:c10
hole_c116_14 :: c11
hole_c12:c137_14 :: c12:c13
hole_true:false8_14 :: true:false
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_s:0':baseError:logZeroError10_14 :: Nat -> s:0':baseError:logZeroError
gen_c3:c411_14 :: Nat -> c3:c4
gen_c5:c612_14 :: Nat -> c5:c6

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
LE, PLUS, TIMES, times, LOOP, le, plus, loop

They will be analysed ascendingly in the following order:
LE < LOOP
PLUS < TIMES
times < TIMES
TIMES < LOOP
times < LOOP
plus < times
times < loop
le < LOOP
le < loop

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

(10)
Obligation:
Innermost TRS:
Rules:
LE(s(z0), 0') -> c
LE(0', z0) -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
PLUS(0', z0) -> c3
PLUS(s(z0), z1) -> c4(PLUS(z0, z1))
TIMES(0', z0) -> c5
TIMES(s(z0), z1) -> c6(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
LOG(z0, 0') -> c7
LOG(z0, s(0')) -> c8
LOG(0', s(s(z0))) -> c9
LOG(s(z0), s(s(z1))) -> c10(LOOP(s(z0), s(s(z1)), s(0'), 0'))
LOOP(z0, s(s(z1)), s(z2), z3) -> c11(IF(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3), LE(z0, s(z2)))
IF(true, z0, z1, z2, z3) -> c12
IF(false, z0, z1, z2, z3) -> c13(LOOP(z0, z1, times(z1, z2), s(z3)), TIMES(z1, z2))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
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))
log(z0, 0') -> baseError
log(z0, s(0')) -> baseError
log(0', s(s(z0))) -> logZeroError
log(s(z0), s(s(z1))) -> loop(s(z0), s(s(z1)), s(0'), 0')
loop(z0, s(s(z1)), s(z2), z3) -> if(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3)
if(true, z0, z1, z2, z3) -> z3
if(false, z0, z1, z2, z3) -> loop(z0, z1, times(z1, z2), s(z3))

Types:
LE :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c:c1:c2
s :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError
0' :: s:0':baseError:logZeroError
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
PLUS :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
TIMES :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c5:c6
c5 :: c5:c6
c6 :: c3:c4 -> c5:c6 -> c5:c6
times :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
LOG :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c7:c8:c9:c10
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c7:c8:c9:c10
c10 :: c11 -> c7:c8:c9:c10
LOOP :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c11
c11 :: c12:c13 -> c:c1:c2 -> c11
IF :: true:false -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c12:c13
le :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> true:false
true :: true:false
c12 :: c12:c13
false :: true:false
c13 :: c11 -> c5:c6 -> c12:c13
plus :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
log :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
baseError :: s:0':baseError:logZeroError
logZeroError :: s:0':baseError:logZeroError
loop :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
if :: true:false -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
hole_c:c1:c21_14 :: c:c1:c2
hole_s:0':baseError:logZeroError2_14 :: s:0':baseError:logZeroError
hole_c3:c43_14 :: c3:c4
hole_c5:c64_14 :: c5:c6
hole_c7:c8:c9:c105_14 :: c7:c8:c9:c10
hole_c116_14 :: c11
hole_c12:c137_14 :: c12:c13
hole_true:false8_14 :: true:false
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_s:0':baseError:logZeroError10_14 :: Nat -> s:0':baseError:logZeroError
gen_c3:c411_14 :: Nat -> c3:c4
gen_c5:c612_14 :: Nat -> c5:c6


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_s:0':baseError:logZeroError10_14(0) <=> 0'
gen_s:0':baseError:logZeroError10_14(+(x, 1)) <=> s(gen_s:0':baseError:logZeroError10_14(x))
gen_c3:c411_14(0) <=> c3
gen_c3:c411_14(+(x, 1)) <=> c4(gen_c3:c411_14(x))
gen_c5:c612_14(0) <=> c5
gen_c5:c612_14(+(x, 1)) <=> c6(c3, gen_c5:c612_14(x))


The following defined symbols remain to be analysed:
LE, PLUS, TIMES, times, LOOP, le, plus, loop

They will be analysed ascendingly in the following order:
LE < LOOP
PLUS < TIMES
times < TIMES
TIMES < LOOP
times < LOOP
plus < times
times < loop
le < LOOP
le < loop

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LE(gen_s:0':baseError:logZeroError10_14(+(1, n14_14)), gen_s:0':baseError:logZeroError10_14(n14_14)) -> gen_c:c1:c29_14(n14_14), rt in Omega(1 + n14_14)

Induction Base:
LE(gen_s:0':baseError:logZeroError10_14(+(1, 0)), gen_s:0':baseError:logZeroError10_14(0)) ->_R^Omega(1)
c

Induction Step:
LE(gen_s:0':baseError:logZeroError10_14(+(1, +(n14_14, 1))), gen_s:0':baseError:logZeroError10_14(+(n14_14, 1))) ->_R^Omega(1)
c2(LE(gen_s:0':baseError:logZeroError10_14(+(1, n14_14)), gen_s:0':baseError:logZeroError10_14(n14_14))) ->_IH
c2(gen_c:c1:c29_14(c15_14))

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:
LE(s(z0), 0') -> c
LE(0', z0) -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
PLUS(0', z0) -> c3
PLUS(s(z0), z1) -> c4(PLUS(z0, z1))
TIMES(0', z0) -> c5
TIMES(s(z0), z1) -> c6(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
LOG(z0, 0') -> c7
LOG(z0, s(0')) -> c8
LOG(0', s(s(z0))) -> c9
LOG(s(z0), s(s(z1))) -> c10(LOOP(s(z0), s(s(z1)), s(0'), 0'))
LOOP(z0, s(s(z1)), s(z2), z3) -> c11(IF(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3), LE(z0, s(z2)))
IF(true, z0, z1, z2, z3) -> c12
IF(false, z0, z1, z2, z3) -> c13(LOOP(z0, z1, times(z1, z2), s(z3)), TIMES(z1, z2))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
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))
log(z0, 0') -> baseError
log(z0, s(0')) -> baseError
log(0', s(s(z0))) -> logZeroError
log(s(z0), s(s(z1))) -> loop(s(z0), s(s(z1)), s(0'), 0')
loop(z0, s(s(z1)), s(z2), z3) -> if(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3)
if(true, z0, z1, z2, z3) -> z3
if(false, z0, z1, z2, z3) -> loop(z0, z1, times(z1, z2), s(z3))

Types:
LE :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c:c1:c2
s :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError
0' :: s:0':baseError:logZeroError
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
PLUS :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
TIMES :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c5:c6
c5 :: c5:c6
c6 :: c3:c4 -> c5:c6 -> c5:c6
times :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
LOG :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c7:c8:c9:c10
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c7:c8:c9:c10
c10 :: c11 -> c7:c8:c9:c10
LOOP :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c11
c11 :: c12:c13 -> c:c1:c2 -> c11
IF :: true:false -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c12:c13
le :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> true:false
true :: true:false
c12 :: c12:c13
false :: true:false
c13 :: c11 -> c5:c6 -> c12:c13
plus :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
log :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
baseError :: s:0':baseError:logZeroError
logZeroError :: s:0':baseError:logZeroError
loop :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
if :: true:false -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
hole_c:c1:c21_14 :: c:c1:c2
hole_s:0':baseError:logZeroError2_14 :: s:0':baseError:logZeroError
hole_c3:c43_14 :: c3:c4
hole_c5:c64_14 :: c5:c6
hole_c7:c8:c9:c105_14 :: c7:c8:c9:c10
hole_c116_14 :: c11
hole_c12:c137_14 :: c12:c13
hole_true:false8_14 :: true:false
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_s:0':baseError:logZeroError10_14 :: Nat -> s:0':baseError:logZeroError
gen_c3:c411_14 :: Nat -> c3:c4
gen_c5:c612_14 :: Nat -> c5:c6


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_s:0':baseError:logZeroError10_14(0) <=> 0'
gen_s:0':baseError:logZeroError10_14(+(x, 1)) <=> s(gen_s:0':baseError:logZeroError10_14(x))
gen_c3:c411_14(0) <=> c3
gen_c3:c411_14(+(x, 1)) <=> c4(gen_c3:c411_14(x))
gen_c5:c612_14(0) <=> c5
gen_c5:c612_14(+(x, 1)) <=> c6(c3, gen_c5:c612_14(x))


The following defined symbols remain to be analysed:
LE, PLUS, TIMES, times, LOOP, le, plus, loop

They will be analysed ascendingly in the following order:
LE < LOOP
PLUS < TIMES
times < TIMES
TIMES < LOOP
times < LOOP
plus < times
times < loop
le < LOOP
le < loop

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
LE(s(z0), 0') -> c
LE(0', z0) -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
PLUS(0', z0) -> c3
PLUS(s(z0), z1) -> c4(PLUS(z0, z1))
TIMES(0', z0) -> c5
TIMES(s(z0), z1) -> c6(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
LOG(z0, 0') -> c7
LOG(z0, s(0')) -> c8
LOG(0', s(s(z0))) -> c9
LOG(s(z0), s(s(z1))) -> c10(LOOP(s(z0), s(s(z1)), s(0'), 0'))
LOOP(z0, s(s(z1)), s(z2), z3) -> c11(IF(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3), LE(z0, s(z2)))
IF(true, z0, z1, z2, z3) -> c12
IF(false, z0, z1, z2, z3) -> c13(LOOP(z0, z1, times(z1, z2), s(z3)), TIMES(z1, z2))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
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))
log(z0, 0') -> baseError
log(z0, s(0')) -> baseError
log(0', s(s(z0))) -> logZeroError
log(s(z0), s(s(z1))) -> loop(s(z0), s(s(z1)), s(0'), 0')
loop(z0, s(s(z1)), s(z2), z3) -> if(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3)
if(true, z0, z1, z2, z3) -> z3
if(false, z0, z1, z2, z3) -> loop(z0, z1, times(z1, z2), s(z3))

Types:
LE :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c:c1:c2
s :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError
0' :: s:0':baseError:logZeroError
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
PLUS :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
TIMES :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c5:c6
c5 :: c5:c6
c6 :: c3:c4 -> c5:c6 -> c5:c6
times :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
LOG :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c7:c8:c9:c10
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c7:c8:c9:c10
c10 :: c11 -> c7:c8:c9:c10
LOOP :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c11
c11 :: c12:c13 -> c:c1:c2 -> c11
IF :: true:false -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c12:c13
le :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> true:false
true :: true:false
c12 :: c12:c13
false :: true:false
c13 :: c11 -> c5:c6 -> c12:c13
plus :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
log :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
baseError :: s:0':baseError:logZeroError
logZeroError :: s:0':baseError:logZeroError
loop :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
if :: true:false -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
hole_c:c1:c21_14 :: c:c1:c2
hole_s:0':baseError:logZeroError2_14 :: s:0':baseError:logZeroError
hole_c3:c43_14 :: c3:c4
hole_c5:c64_14 :: c5:c6
hole_c7:c8:c9:c105_14 :: c7:c8:c9:c10
hole_c116_14 :: c11
hole_c12:c137_14 :: c12:c13
hole_true:false8_14 :: true:false
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_s:0':baseError:logZeroError10_14 :: Nat -> s:0':baseError:logZeroError
gen_c3:c411_14 :: Nat -> c3:c4
gen_c5:c612_14 :: Nat -> c5:c6


Lemmas:
LE(gen_s:0':baseError:logZeroError10_14(+(1, n14_14)), gen_s:0':baseError:logZeroError10_14(n14_14)) -> gen_c:c1:c29_14(n14_14), rt in Omega(1 + n14_14)


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_s:0':baseError:logZeroError10_14(0) <=> 0'
gen_s:0':baseError:logZeroError10_14(+(x, 1)) <=> s(gen_s:0':baseError:logZeroError10_14(x))
gen_c3:c411_14(0) <=> c3
gen_c3:c411_14(+(x, 1)) <=> c4(gen_c3:c411_14(x))
gen_c5:c612_14(0) <=> c5
gen_c5:c612_14(+(x, 1)) <=> c6(c3, gen_c5:c612_14(x))


The following defined symbols remain to be analysed:
PLUS, TIMES, times, LOOP, le, plus, loop

They will be analysed ascendingly in the following order:
PLUS < TIMES
times < TIMES
TIMES < LOOP
times < LOOP
plus < times
times < loop
le < LOOP
le < loop

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
PLUS(gen_s:0':baseError:logZeroError10_14(n678_14), gen_s:0':baseError:logZeroError10_14(b)) -> gen_c3:c411_14(n678_14), rt in Omega(1 + n678_14)

Induction Base:
PLUS(gen_s:0':baseError:logZeroError10_14(0), gen_s:0':baseError:logZeroError10_14(b)) ->_R^Omega(1)
c3

Induction Step:
PLUS(gen_s:0':baseError:logZeroError10_14(+(n678_14, 1)), gen_s:0':baseError:logZeroError10_14(b)) ->_R^Omega(1)
c4(PLUS(gen_s:0':baseError:logZeroError10_14(n678_14), gen_s:0':baseError:logZeroError10_14(b))) ->_IH
c4(gen_c3:c411_14(c679_14))

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:
LE(s(z0), 0') -> c
LE(0', z0) -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
PLUS(0', z0) -> c3
PLUS(s(z0), z1) -> c4(PLUS(z0, z1))
TIMES(0', z0) -> c5
TIMES(s(z0), z1) -> c6(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
LOG(z0, 0') -> c7
LOG(z0, s(0')) -> c8
LOG(0', s(s(z0))) -> c9
LOG(s(z0), s(s(z1))) -> c10(LOOP(s(z0), s(s(z1)), s(0'), 0'))
LOOP(z0, s(s(z1)), s(z2), z3) -> c11(IF(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3), LE(z0, s(z2)))
IF(true, z0, z1, z2, z3) -> c12
IF(false, z0, z1, z2, z3) -> c13(LOOP(z0, z1, times(z1, z2), s(z3)), TIMES(z1, z2))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
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))
log(z0, 0') -> baseError
log(z0, s(0')) -> baseError
log(0', s(s(z0))) -> logZeroError
log(s(z0), s(s(z1))) -> loop(s(z0), s(s(z1)), s(0'), 0')
loop(z0, s(s(z1)), s(z2), z3) -> if(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3)
if(true, z0, z1, z2, z3) -> z3
if(false, z0, z1, z2, z3) -> loop(z0, z1, times(z1, z2), s(z3))

Types:
LE :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c:c1:c2
s :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError
0' :: s:0':baseError:logZeroError
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
PLUS :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
TIMES :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c5:c6
c5 :: c5:c6
c6 :: c3:c4 -> c5:c6 -> c5:c6
times :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
LOG :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c7:c8:c9:c10
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c7:c8:c9:c10
c10 :: c11 -> c7:c8:c9:c10
LOOP :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c11
c11 :: c12:c13 -> c:c1:c2 -> c11
IF :: true:false -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c12:c13
le :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> true:false
true :: true:false
c12 :: c12:c13
false :: true:false
c13 :: c11 -> c5:c6 -> c12:c13
plus :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
log :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
baseError :: s:0':baseError:logZeroError
logZeroError :: s:0':baseError:logZeroError
loop :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
if :: true:false -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
hole_c:c1:c21_14 :: c:c1:c2
hole_s:0':baseError:logZeroError2_14 :: s:0':baseError:logZeroError
hole_c3:c43_14 :: c3:c4
hole_c5:c64_14 :: c5:c6
hole_c7:c8:c9:c105_14 :: c7:c8:c9:c10
hole_c116_14 :: c11
hole_c12:c137_14 :: c12:c13
hole_true:false8_14 :: true:false
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_s:0':baseError:logZeroError10_14 :: Nat -> s:0':baseError:logZeroError
gen_c3:c411_14 :: Nat -> c3:c4
gen_c5:c612_14 :: Nat -> c5:c6


Lemmas:
LE(gen_s:0':baseError:logZeroError10_14(+(1, n14_14)), gen_s:0':baseError:logZeroError10_14(n14_14)) -> gen_c:c1:c29_14(n14_14), rt in Omega(1 + n14_14)
PLUS(gen_s:0':baseError:logZeroError10_14(n678_14), gen_s:0':baseError:logZeroError10_14(b)) -> gen_c3:c411_14(n678_14), rt in Omega(1 + n678_14)


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_s:0':baseError:logZeroError10_14(0) <=> 0'
gen_s:0':baseError:logZeroError10_14(+(x, 1)) <=> s(gen_s:0':baseError:logZeroError10_14(x))
gen_c3:c411_14(0) <=> c3
gen_c3:c411_14(+(x, 1)) <=> c4(gen_c3:c411_14(x))
gen_c5:c612_14(0) <=> c5
gen_c5:c612_14(+(x, 1)) <=> c6(c3, gen_c5:c612_14(x))


The following defined symbols remain to be analysed:
le, TIMES, times, LOOP, plus, loop

They will be analysed ascendingly in the following order:
times < TIMES
TIMES < LOOP
times < LOOP
plus < times
times < loop
le < LOOP
le < loop

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
le(gen_s:0':baseError:logZeroError10_14(+(1, n1426_14)), gen_s:0':baseError:logZeroError10_14(n1426_14)) -> false, rt in Omega(0)

Induction Base:
le(gen_s:0':baseError:logZeroError10_14(+(1, 0)), gen_s:0':baseError:logZeroError10_14(0)) ->_R^Omega(0)
false

Induction Step:
le(gen_s:0':baseError:logZeroError10_14(+(1, +(n1426_14, 1))), gen_s:0':baseError:logZeroError10_14(+(n1426_14, 1))) ->_R^Omega(0)
le(gen_s:0':baseError:logZeroError10_14(+(1, n1426_14)), gen_s:0':baseError:logZeroError10_14(n1426_14)) ->_IH
false

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:
LE(s(z0), 0') -> c
LE(0', z0) -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
PLUS(0', z0) -> c3
PLUS(s(z0), z1) -> c4(PLUS(z0, z1))
TIMES(0', z0) -> c5
TIMES(s(z0), z1) -> c6(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
LOG(z0, 0') -> c7
LOG(z0, s(0')) -> c8
LOG(0', s(s(z0))) -> c9
LOG(s(z0), s(s(z1))) -> c10(LOOP(s(z0), s(s(z1)), s(0'), 0'))
LOOP(z0, s(s(z1)), s(z2), z3) -> c11(IF(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3), LE(z0, s(z2)))
IF(true, z0, z1, z2, z3) -> c12
IF(false, z0, z1, z2, z3) -> c13(LOOP(z0, z1, times(z1, z2), s(z3)), TIMES(z1, z2))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
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))
log(z0, 0') -> baseError
log(z0, s(0')) -> baseError
log(0', s(s(z0))) -> logZeroError
log(s(z0), s(s(z1))) -> loop(s(z0), s(s(z1)), s(0'), 0')
loop(z0, s(s(z1)), s(z2), z3) -> if(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3)
if(true, z0, z1, z2, z3) -> z3
if(false, z0, z1, z2, z3) -> loop(z0, z1, times(z1, z2), s(z3))

Types:
LE :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c:c1:c2
s :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError
0' :: s:0':baseError:logZeroError
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
PLUS :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
TIMES :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c5:c6
c5 :: c5:c6
c6 :: c3:c4 -> c5:c6 -> c5:c6
times :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
LOG :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c7:c8:c9:c10
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c7:c8:c9:c10
c10 :: c11 -> c7:c8:c9:c10
LOOP :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c11
c11 :: c12:c13 -> c:c1:c2 -> c11
IF :: true:false -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c12:c13
le :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> true:false
true :: true:false
c12 :: c12:c13
false :: true:false
c13 :: c11 -> c5:c6 -> c12:c13
plus :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
log :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
baseError :: s:0':baseError:logZeroError
logZeroError :: s:0':baseError:logZeroError
loop :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
if :: true:false -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
hole_c:c1:c21_14 :: c:c1:c2
hole_s:0':baseError:logZeroError2_14 :: s:0':baseError:logZeroError
hole_c3:c43_14 :: c3:c4
hole_c5:c64_14 :: c5:c6
hole_c7:c8:c9:c105_14 :: c7:c8:c9:c10
hole_c116_14 :: c11
hole_c12:c137_14 :: c12:c13
hole_true:false8_14 :: true:false
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_s:0':baseError:logZeroError10_14 :: Nat -> s:0':baseError:logZeroError
gen_c3:c411_14 :: Nat -> c3:c4
gen_c5:c612_14 :: Nat -> c5:c6


Lemmas:
LE(gen_s:0':baseError:logZeroError10_14(+(1, n14_14)), gen_s:0':baseError:logZeroError10_14(n14_14)) -> gen_c:c1:c29_14(n14_14), rt in Omega(1 + n14_14)
PLUS(gen_s:0':baseError:logZeroError10_14(n678_14), gen_s:0':baseError:logZeroError10_14(b)) -> gen_c3:c411_14(n678_14), rt in Omega(1 + n678_14)
le(gen_s:0':baseError:logZeroError10_14(+(1, n1426_14)), gen_s:0':baseError:logZeroError10_14(n1426_14)) -> false, rt in Omega(0)


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_s:0':baseError:logZeroError10_14(0) <=> 0'
gen_s:0':baseError:logZeroError10_14(+(x, 1)) <=> s(gen_s:0':baseError:logZeroError10_14(x))
gen_c3:c411_14(0) <=> c3
gen_c3:c411_14(+(x, 1)) <=> c4(gen_c3:c411_14(x))
gen_c5:c612_14(0) <=> c5
gen_c5:c612_14(+(x, 1)) <=> c6(c3, gen_c5:c612_14(x))


The following defined symbols remain to be analysed:
plus, TIMES, times, LOOP, loop

They will be analysed ascendingly in the following order:
times < TIMES
TIMES < LOOP
times < LOOP
plus < times
times < loop

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
plus(gen_s:0':baseError:logZeroError10_14(n1867_14), gen_s:0':baseError:logZeroError10_14(b)) -> gen_s:0':baseError:logZeroError10_14(+(n1867_14, b)), rt in Omega(0)

Induction Base:
plus(gen_s:0':baseError:logZeroError10_14(0), gen_s:0':baseError:logZeroError10_14(b)) ->_R^Omega(0)
gen_s:0':baseError:logZeroError10_14(b)

Induction Step:
plus(gen_s:0':baseError:logZeroError10_14(+(n1867_14, 1)), gen_s:0':baseError:logZeroError10_14(b)) ->_R^Omega(0)
s(plus(gen_s:0':baseError:logZeroError10_14(n1867_14), gen_s:0':baseError:logZeroError10_14(b))) ->_IH
s(gen_s:0':baseError:logZeroError10_14(+(b, c1868_14)))

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:
LE(s(z0), 0') -> c
LE(0', z0) -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
PLUS(0', z0) -> c3
PLUS(s(z0), z1) -> c4(PLUS(z0, z1))
TIMES(0', z0) -> c5
TIMES(s(z0), z1) -> c6(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
LOG(z0, 0') -> c7
LOG(z0, s(0')) -> c8
LOG(0', s(s(z0))) -> c9
LOG(s(z0), s(s(z1))) -> c10(LOOP(s(z0), s(s(z1)), s(0'), 0'))
LOOP(z0, s(s(z1)), s(z2), z3) -> c11(IF(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3), LE(z0, s(z2)))
IF(true, z0, z1, z2, z3) -> c12
IF(false, z0, z1, z2, z3) -> c13(LOOP(z0, z1, times(z1, z2), s(z3)), TIMES(z1, z2))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
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))
log(z0, 0') -> baseError
log(z0, s(0')) -> baseError
log(0', s(s(z0))) -> logZeroError
log(s(z0), s(s(z1))) -> loop(s(z0), s(s(z1)), s(0'), 0')
loop(z0, s(s(z1)), s(z2), z3) -> if(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3)
if(true, z0, z1, z2, z3) -> z3
if(false, z0, z1, z2, z3) -> loop(z0, z1, times(z1, z2), s(z3))

Types:
LE :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c:c1:c2
s :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError
0' :: s:0':baseError:logZeroError
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
PLUS :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
TIMES :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c5:c6
c5 :: c5:c6
c6 :: c3:c4 -> c5:c6 -> c5:c6
times :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
LOG :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c7:c8:c9:c10
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c7:c8:c9:c10
c10 :: c11 -> c7:c8:c9:c10
LOOP :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c11
c11 :: c12:c13 -> c:c1:c2 -> c11
IF :: true:false -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c12:c13
le :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> true:false
true :: true:false
c12 :: c12:c13
false :: true:false
c13 :: c11 -> c5:c6 -> c12:c13
plus :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
log :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
baseError :: s:0':baseError:logZeroError
logZeroError :: s:0':baseError:logZeroError
loop :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
if :: true:false -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
hole_c:c1:c21_14 :: c:c1:c2
hole_s:0':baseError:logZeroError2_14 :: s:0':baseError:logZeroError
hole_c3:c43_14 :: c3:c4
hole_c5:c64_14 :: c5:c6
hole_c7:c8:c9:c105_14 :: c7:c8:c9:c10
hole_c116_14 :: c11
hole_c12:c137_14 :: c12:c13
hole_true:false8_14 :: true:false
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_s:0':baseError:logZeroError10_14 :: Nat -> s:0':baseError:logZeroError
gen_c3:c411_14 :: Nat -> c3:c4
gen_c5:c612_14 :: Nat -> c5:c6


Lemmas:
LE(gen_s:0':baseError:logZeroError10_14(+(1, n14_14)), gen_s:0':baseError:logZeroError10_14(n14_14)) -> gen_c:c1:c29_14(n14_14), rt in Omega(1 + n14_14)
PLUS(gen_s:0':baseError:logZeroError10_14(n678_14), gen_s:0':baseError:logZeroError10_14(b)) -> gen_c3:c411_14(n678_14), rt in Omega(1 + n678_14)
le(gen_s:0':baseError:logZeroError10_14(+(1, n1426_14)), gen_s:0':baseError:logZeroError10_14(n1426_14)) -> false, rt in Omega(0)
plus(gen_s:0':baseError:logZeroError10_14(n1867_14), gen_s:0':baseError:logZeroError10_14(b)) -> gen_s:0':baseError:logZeroError10_14(+(n1867_14, b)), rt in Omega(0)


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_s:0':baseError:logZeroError10_14(0) <=> 0'
gen_s:0':baseError:logZeroError10_14(+(x, 1)) <=> s(gen_s:0':baseError:logZeroError10_14(x))
gen_c3:c411_14(0) <=> c3
gen_c3:c411_14(+(x, 1)) <=> c4(gen_c3:c411_14(x))
gen_c5:c612_14(0) <=> c5
gen_c5:c612_14(+(x, 1)) <=> c6(c3, gen_c5:c612_14(x))


The following defined symbols remain to be analysed:
times, TIMES, LOOP, loop

They will be analysed ascendingly in the following order:
times < TIMES
TIMES < LOOP
times < LOOP
times < loop

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
times(gen_s:0':baseError:logZeroError10_14(n3246_14), gen_s:0':baseError:logZeroError10_14(b)) -> gen_s:0':baseError:logZeroError10_14(*(n3246_14, b)), rt in Omega(0)

Induction Base:
times(gen_s:0':baseError:logZeroError10_14(0), gen_s:0':baseError:logZeroError10_14(b)) ->_R^Omega(0)
0'

Induction Step:
times(gen_s:0':baseError:logZeroError10_14(+(n3246_14, 1)), gen_s:0':baseError:logZeroError10_14(b)) ->_R^Omega(0)
plus(gen_s:0':baseError:logZeroError10_14(b), times(gen_s:0':baseError:logZeroError10_14(n3246_14), gen_s:0':baseError:logZeroError10_14(b))) ->_IH
plus(gen_s:0':baseError:logZeroError10_14(b), gen_s:0':baseError:logZeroError10_14(*(c3247_14, b))) ->_L^Omega(0)
gen_s:0':baseError:logZeroError10_14(+(b, *(n3246_14, 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:
LE(s(z0), 0') -> c
LE(0', z0) -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
PLUS(0', z0) -> c3
PLUS(s(z0), z1) -> c4(PLUS(z0, z1))
TIMES(0', z0) -> c5
TIMES(s(z0), z1) -> c6(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
LOG(z0, 0') -> c7
LOG(z0, s(0')) -> c8
LOG(0', s(s(z0))) -> c9
LOG(s(z0), s(s(z1))) -> c10(LOOP(s(z0), s(s(z1)), s(0'), 0'))
LOOP(z0, s(s(z1)), s(z2), z3) -> c11(IF(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3), LE(z0, s(z2)))
IF(true, z0, z1, z2, z3) -> c12
IF(false, z0, z1, z2, z3) -> c13(LOOP(z0, z1, times(z1, z2), s(z3)), TIMES(z1, z2))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
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))
log(z0, 0') -> baseError
log(z0, s(0')) -> baseError
log(0', s(s(z0))) -> logZeroError
log(s(z0), s(s(z1))) -> loop(s(z0), s(s(z1)), s(0'), 0')
loop(z0, s(s(z1)), s(z2), z3) -> if(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3)
if(true, z0, z1, z2, z3) -> z3
if(false, z0, z1, z2, z3) -> loop(z0, z1, times(z1, z2), s(z3))

Types:
LE :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c:c1:c2
s :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError
0' :: s:0':baseError:logZeroError
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
PLUS :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
TIMES :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c5:c6
c5 :: c5:c6
c6 :: c3:c4 -> c5:c6 -> c5:c6
times :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
LOG :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c7:c8:c9:c10
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c7:c8:c9:c10
c10 :: c11 -> c7:c8:c9:c10
LOOP :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c11
c11 :: c12:c13 -> c:c1:c2 -> c11
IF :: true:false -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c12:c13
le :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> true:false
true :: true:false
c12 :: c12:c13
false :: true:false
c13 :: c11 -> c5:c6 -> c12:c13
plus :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
log :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
baseError :: s:0':baseError:logZeroError
logZeroError :: s:0':baseError:logZeroError
loop :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
if :: true:false -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
hole_c:c1:c21_14 :: c:c1:c2
hole_s:0':baseError:logZeroError2_14 :: s:0':baseError:logZeroError
hole_c3:c43_14 :: c3:c4
hole_c5:c64_14 :: c5:c6
hole_c7:c8:c9:c105_14 :: c7:c8:c9:c10
hole_c116_14 :: c11
hole_c12:c137_14 :: c12:c13
hole_true:false8_14 :: true:false
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_s:0':baseError:logZeroError10_14 :: Nat -> s:0':baseError:logZeroError
gen_c3:c411_14 :: Nat -> c3:c4
gen_c5:c612_14 :: Nat -> c5:c6


Lemmas:
LE(gen_s:0':baseError:logZeroError10_14(+(1, n14_14)), gen_s:0':baseError:logZeroError10_14(n14_14)) -> gen_c:c1:c29_14(n14_14), rt in Omega(1 + n14_14)
PLUS(gen_s:0':baseError:logZeroError10_14(n678_14), gen_s:0':baseError:logZeroError10_14(b)) -> gen_c3:c411_14(n678_14), rt in Omega(1 + n678_14)
le(gen_s:0':baseError:logZeroError10_14(+(1, n1426_14)), gen_s:0':baseError:logZeroError10_14(n1426_14)) -> false, rt in Omega(0)
plus(gen_s:0':baseError:logZeroError10_14(n1867_14), gen_s:0':baseError:logZeroError10_14(b)) -> gen_s:0':baseError:logZeroError10_14(+(n1867_14, b)), rt in Omega(0)
times(gen_s:0':baseError:logZeroError10_14(n3246_14), gen_s:0':baseError:logZeroError10_14(b)) -> gen_s:0':baseError:logZeroError10_14(*(n3246_14, b)), rt in Omega(0)


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_s:0':baseError:logZeroError10_14(0) <=> 0'
gen_s:0':baseError:logZeroError10_14(+(x, 1)) <=> s(gen_s:0':baseError:logZeroError10_14(x))
gen_c3:c411_14(0) <=> c3
gen_c3:c411_14(+(x, 1)) <=> c4(gen_c3:c411_14(x))
gen_c5:c612_14(0) <=> c5
gen_c5:c612_14(+(x, 1)) <=> c6(c3, gen_c5:c612_14(x))


The following defined symbols remain to be analysed:
TIMES, LOOP, loop

They will be analysed ascendingly in the following order:
TIMES < LOOP

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
TIMES(gen_s:0':baseError:logZeroError10_14(n4956_14), gen_s:0':baseError:logZeroError10_14(b)) -> *13_14, rt in Omega(b*n4956_14 + n4956_14)

Induction Base:
TIMES(gen_s:0':baseError:logZeroError10_14(0), gen_s:0':baseError:logZeroError10_14(b))

Induction Step:
TIMES(gen_s:0':baseError:logZeroError10_14(+(n4956_14, 1)), gen_s:0':baseError:logZeroError10_14(b)) ->_R^Omega(1)
c6(PLUS(gen_s:0':baseError:logZeroError10_14(b), times(gen_s:0':baseError:logZeroError10_14(n4956_14), gen_s:0':baseError:logZeroError10_14(b))), TIMES(gen_s:0':baseError:logZeroError10_14(n4956_14), gen_s:0':baseError:logZeroError10_14(b))) ->_L^Omega(0)
c6(PLUS(gen_s:0':baseError:logZeroError10_14(b), gen_s:0':baseError:logZeroError10_14(*(n4956_14, b))), TIMES(gen_s:0':baseError:logZeroError10_14(n4956_14), gen_s:0':baseError:logZeroError10_14(b))) ->_L^Omega(1 + b)
c6(gen_c3:c411_14(b), TIMES(gen_s:0':baseError:logZeroError10_14(n4956_14), gen_s:0':baseError:logZeroError10_14(*(n4956_14, b)))) ->_IH
c6(gen_c3:c411_14(*(n4956_14, b)), *13_14)

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:
LE(s(z0), 0') -> c
LE(0', z0) -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
PLUS(0', z0) -> c3
PLUS(s(z0), z1) -> c4(PLUS(z0, z1))
TIMES(0', z0) -> c5
TIMES(s(z0), z1) -> c6(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
LOG(z0, 0') -> c7
LOG(z0, s(0')) -> c8
LOG(0', s(s(z0))) -> c9
LOG(s(z0), s(s(z1))) -> c10(LOOP(s(z0), s(s(z1)), s(0'), 0'))
LOOP(z0, s(s(z1)), s(z2), z3) -> c11(IF(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3), LE(z0, s(z2)))
IF(true, z0, z1, z2, z3) -> c12
IF(false, z0, z1, z2, z3) -> c13(LOOP(z0, z1, times(z1, z2), s(z3)), TIMES(z1, z2))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
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))
log(z0, 0') -> baseError
log(z0, s(0')) -> baseError
log(0', s(s(z0))) -> logZeroError
log(s(z0), s(s(z1))) -> loop(s(z0), s(s(z1)), s(0'), 0')
loop(z0, s(s(z1)), s(z2), z3) -> if(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3)
if(true, z0, z1, z2, z3) -> z3
if(false, z0, z1, z2, z3) -> loop(z0, z1, times(z1, z2), s(z3))

Types:
LE :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c:c1:c2
s :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError
0' :: s:0':baseError:logZeroError
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
PLUS :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
TIMES :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c5:c6
c5 :: c5:c6
c6 :: c3:c4 -> c5:c6 -> c5:c6
times :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
LOG :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c7:c8:c9:c10
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c7:c8:c9:c10
c10 :: c11 -> c7:c8:c9:c10
LOOP :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c11
c11 :: c12:c13 -> c:c1:c2 -> c11
IF :: true:false -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c12:c13
le :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> true:false
true :: true:false
c12 :: c12:c13
false :: true:false
c13 :: c11 -> c5:c6 -> c12:c13
plus :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
log :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
baseError :: s:0':baseError:logZeroError
logZeroError :: s:0':baseError:logZeroError
loop :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
if :: true:false -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
hole_c:c1:c21_14 :: c:c1:c2
hole_s:0':baseError:logZeroError2_14 :: s:0':baseError:logZeroError
hole_c3:c43_14 :: c3:c4
hole_c5:c64_14 :: c5:c6
hole_c7:c8:c9:c105_14 :: c7:c8:c9:c10
hole_c116_14 :: c11
hole_c12:c137_14 :: c12:c13
hole_true:false8_14 :: true:false
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_s:0':baseError:logZeroError10_14 :: Nat -> s:0':baseError:logZeroError
gen_c3:c411_14 :: Nat -> c3:c4
gen_c5:c612_14 :: Nat -> c5:c6


Lemmas:
LE(gen_s:0':baseError:logZeroError10_14(+(1, n14_14)), gen_s:0':baseError:logZeroError10_14(n14_14)) -> gen_c:c1:c29_14(n14_14), rt in Omega(1 + n14_14)
PLUS(gen_s:0':baseError:logZeroError10_14(n678_14), gen_s:0':baseError:logZeroError10_14(b)) -> gen_c3:c411_14(n678_14), rt in Omega(1 + n678_14)
le(gen_s:0':baseError:logZeroError10_14(+(1, n1426_14)), gen_s:0':baseError:logZeroError10_14(n1426_14)) -> false, rt in Omega(0)
plus(gen_s:0':baseError:logZeroError10_14(n1867_14), gen_s:0':baseError:logZeroError10_14(b)) -> gen_s:0':baseError:logZeroError10_14(+(n1867_14, b)), rt in Omega(0)
times(gen_s:0':baseError:logZeroError10_14(n3246_14), gen_s:0':baseError:logZeroError10_14(b)) -> gen_s:0':baseError:logZeroError10_14(*(n3246_14, b)), rt in Omega(0)


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_s:0':baseError:logZeroError10_14(0) <=> 0'
gen_s:0':baseError:logZeroError10_14(+(x, 1)) <=> s(gen_s:0':baseError:logZeroError10_14(x))
gen_c3:c411_14(0) <=> c3
gen_c3:c411_14(+(x, 1)) <=> c4(gen_c3:c411_14(x))
gen_c5:c612_14(0) <=> c5
gen_c5:c612_14(+(x, 1)) <=> c6(c3, gen_c5:c612_14(x))


The following defined symbols remain to be analysed:
TIMES, LOOP, loop

They will be analysed ascendingly in the following order:
TIMES < LOOP

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

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

(29)
BOUNDS(n^2, INF)

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

(30)
Obligation:
Innermost TRS:
Rules:
LE(s(z0), 0') -> c
LE(0', z0) -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
PLUS(0', z0) -> c3
PLUS(s(z0), z1) -> c4(PLUS(z0, z1))
TIMES(0', z0) -> c5
TIMES(s(z0), z1) -> c6(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
LOG(z0, 0') -> c7
LOG(z0, s(0')) -> c8
LOG(0', s(s(z0))) -> c9
LOG(s(z0), s(s(z1))) -> c10(LOOP(s(z0), s(s(z1)), s(0'), 0'))
LOOP(z0, s(s(z1)), s(z2), z3) -> c11(IF(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3), LE(z0, s(z2)))
IF(true, z0, z1, z2, z3) -> c12
IF(false, z0, z1, z2, z3) -> c13(LOOP(z0, z1, times(z1, z2), s(z3)), TIMES(z1, z2))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
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))
log(z0, 0') -> baseError
log(z0, s(0')) -> baseError
log(0', s(s(z0))) -> logZeroError
log(s(z0), s(s(z1))) -> loop(s(z0), s(s(z1)), s(0'), 0')
loop(z0, s(s(z1)), s(z2), z3) -> if(le(z0, s(z2)), z0, s(s(z1)), s(z2), z3)
if(true, z0, z1, z2, z3) -> z3
if(false, z0, z1, z2, z3) -> loop(z0, z1, times(z1, z2), s(z3))

Types:
LE :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c:c1:c2
s :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError
0' :: s:0':baseError:logZeroError
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
PLUS :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
TIMES :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c5:c6
c5 :: c5:c6
c6 :: c3:c4 -> c5:c6 -> c5:c6
times :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
LOG :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c7:c8:c9:c10
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c7:c8:c9:c10
c10 :: c11 -> c7:c8:c9:c10
LOOP :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c11
c11 :: c12:c13 -> c:c1:c2 -> c11
IF :: true:false -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> c12:c13
le :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> true:false
true :: true:false
c12 :: c12:c13
false :: true:false
c13 :: c11 -> c5:c6 -> c12:c13
plus :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
log :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
baseError :: s:0':baseError:logZeroError
logZeroError :: s:0':baseError:logZeroError
loop :: s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
if :: true:false -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError -> s:0':baseError:logZeroError
hole_c:c1:c21_14 :: c:c1:c2
hole_s:0':baseError:logZeroError2_14 :: s:0':baseError:logZeroError
hole_c3:c43_14 :: c3:c4
hole_c5:c64_14 :: c5:c6
hole_c7:c8:c9:c105_14 :: c7:c8:c9:c10
hole_c116_14 :: c11
hole_c12:c137_14 :: c12:c13
hole_true:false8_14 :: true:false
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_s:0':baseError:logZeroError10_14 :: Nat -> s:0':baseError:logZeroError
gen_c3:c411_14 :: Nat -> c3:c4
gen_c5:c612_14 :: Nat -> c5:c6


Lemmas:
LE(gen_s:0':baseError:logZeroError10_14(+(1, n14_14)), gen_s:0':baseError:logZeroError10_14(n14_14)) -> gen_c:c1:c29_14(n14_14), rt in Omega(1 + n14_14)
PLUS(gen_s:0':baseError:logZeroError10_14(n678_14), gen_s:0':baseError:logZeroError10_14(b)) -> gen_c3:c411_14(n678_14), rt in Omega(1 + n678_14)
le(gen_s:0':baseError:logZeroError10_14(+(1, n1426_14)), gen_s:0':baseError:logZeroError10_14(n1426_14)) -> false, rt in Omega(0)
plus(gen_s:0':baseError:logZeroError10_14(n1867_14), gen_s:0':baseError:logZeroError10_14(b)) -> gen_s:0':baseError:logZeroError10_14(+(n1867_14, b)), rt in Omega(0)
times(gen_s:0':baseError:logZeroError10_14(n3246_14), gen_s:0':baseError:logZeroError10_14(b)) -> gen_s:0':baseError:logZeroError10_14(*(n3246_14, b)), rt in Omega(0)
TIMES(gen_s:0':baseError:logZeroError10_14(n4956_14), gen_s:0':baseError:logZeroError10_14(b)) -> *13_14, rt in Omega(b*n4956_14 + n4956_14)


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_s:0':baseError:logZeroError10_14(0) <=> 0'
gen_s:0':baseError:logZeroError10_14(+(x, 1)) <=> s(gen_s:0':baseError:logZeroError10_14(x))
gen_c3:c411_14(0) <=> c3
gen_c3:c411_14(+(x, 1)) <=> c4(gen_c3:c411_14(x))
gen_c5:c612_14(0) <=> c5
gen_c5:c612_14(+(x, 1)) <=> c6(c3, gen_c5:c612_14(x))


The following defined symbols remain to be analysed:
LOOP, loop