WORST_CASE(Omega(n^2),?)
proof of input_LnoK3WXuZJ.trs
# AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 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), 1 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 335 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 126 ms]
(14) BEST
    (15) proven lower bound
        (16) LowerBoundPropagationProof [FINISHED, 0 ms]
        (17) BOUNDS(n^1, INF)
    (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 48 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 80 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 61 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 45 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 106 ms]
        (28) typed CpxTrs
        (29) RewriteLemmaProof [LOWER BOUND(ID), 454 ms]
        (30) BEST
            (31) proven lower bound
                (32) LowerBoundPropagationProof [FINISHED, 0 ms]
                (33) BOUNDS(n^2, INF)
            (34) 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:

   log(x, s(s(y))) -> cond(le(x, s(s(y))), x, y)
   cond(true, x, y) -> s(0)
   cond(false, x, y) -> double(log(x, square(s(s(y)))))
   le(0, v) -> true
   le(s(u), 0) -> false
   le(s(u), s(v)) -> le(u, v)
   double(0) -> 0
   double(s(x)) -> s(s(double(x)))
   square(0) -> 0
   square(s(x)) -> s(plus(square(x), double(x)))
   plus(n, 0) -> n
   plus(n, s(m)) -> s(plus(n, m))

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:
   log(z0, s(s(z1))) -> cond(le(z0, s(s(z1))), z0, z1)
   cond(true, z0, z1) -> s(0)
   cond(false, z0, z1) -> double(log(z0, square(s(s(z1)))))
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   double(0) -> 0
   double(s(z0)) -> s(s(double(z0)))
   square(0) -> 0
   square(s(z0)) -> s(plus(square(z0), double(z0)))
   plus(z0, 0) -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))
Tuples:
   LOG(z0, s(s(z1))) -> c(COND(le(z0, s(s(z1))), z0, z1), LE(z0, s(s(z1))))
   COND(true, z0, z1) -> c1
   COND(false, z0, z1) -> c2(DOUBLE(log(z0, square(s(s(z1))))), LOG(z0, square(s(s(z1)))), SQUARE(s(s(z1))))
   LE(0, z0) -> c3
   LE(s(z0), 0) -> c4
   LE(s(z0), s(z1)) -> c5(LE(z0, z1))
   DOUBLE(0) -> c6
   DOUBLE(s(z0)) -> c7(DOUBLE(z0))
   SQUARE(0) -> c8
   SQUARE(s(z0)) -> c9(PLUS(square(z0), double(z0)), SQUARE(z0))
   SQUARE(s(z0)) -> c10(PLUS(square(z0), double(z0)), DOUBLE(z0))
   PLUS(z0, 0) -> c11
   PLUS(z0, s(z1)) -> c12(PLUS(z0, z1))
S tuples:
   LOG(z0, s(s(z1))) -> c(COND(le(z0, s(s(z1))), z0, z1), LE(z0, s(s(z1))))
   COND(true, z0, z1) -> c1
   COND(false, z0, z1) -> c2(DOUBLE(log(z0, square(s(s(z1))))), LOG(z0, square(s(s(z1)))), SQUARE(s(s(z1))))
   LE(0, z0) -> c3
   LE(s(z0), 0) -> c4
   LE(s(z0), s(z1)) -> c5(LE(z0, z1))
   DOUBLE(0) -> c6
   DOUBLE(s(z0)) -> c7(DOUBLE(z0))
   SQUARE(0) -> c8
   SQUARE(s(z0)) -> c9(PLUS(square(z0), double(z0)), SQUARE(z0))
   SQUARE(s(z0)) -> c10(PLUS(square(z0), double(z0)), DOUBLE(z0))
   PLUS(z0, 0) -> c11
   PLUS(z0, s(z1)) -> c12(PLUS(z0, z1))
K tuples:none
Defined Rule Symbols:   log_2, cond_3, le_2, double_1, square_1, plus_2

Defined Pair Symbols:   LOG_2, COND_3, LE_2, DOUBLE_1, SQUARE_1, PLUS_2

Compound Symbols:   c_2, c1, c2_3, c3, c4, c5_1, c6, c7_1, c8, c9_2, c10_2, c11, c12_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^2, INF).


The TRS R consists of the following rules:

   LOG(z0, s(s(z1))) -> c(COND(le(z0, s(s(z1))), z0, z1), LE(z0, s(s(z1))))
   COND(true, z0, z1) -> c1
   COND(false, z0, z1) -> c2(DOUBLE(log(z0, square(s(s(z1))))), LOG(z0, square(s(s(z1)))), SQUARE(s(s(z1))))
   LE(0, z0) -> c3
   LE(s(z0), 0) -> c4
   LE(s(z0), s(z1)) -> c5(LE(z0, z1))
   DOUBLE(0) -> c6
   DOUBLE(s(z0)) -> c7(DOUBLE(z0))
   SQUARE(0) -> c8
   SQUARE(s(z0)) -> c9(PLUS(square(z0), double(z0)), SQUARE(z0))
   SQUARE(s(z0)) -> c10(PLUS(square(z0), double(z0)), DOUBLE(z0))
   PLUS(z0, 0) -> c11
   PLUS(z0, s(z1)) -> c12(PLUS(z0, z1))

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

   log(z0, s(s(z1))) -> cond(le(z0, s(s(z1))), z0, z1)
   cond(true, z0, z1) -> s(0)
   cond(false, z0, z1) -> double(log(z0, square(s(s(z1)))))
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   double(0) -> 0
   double(s(z0)) -> s(s(double(z0)))
   square(0) -> 0
   square(s(z0)) -> s(plus(square(z0), double(z0)))
   plus(z0, 0) -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))

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:

   LOG(z0, s(s(z1))) -> c(COND(le(z0, s(s(z1))), z0, z1), LE(z0, s(s(z1))))
   COND(true, z0, z1) -> c1
   COND(false, z0, z1) -> c2(DOUBLE(log(z0, square(s(s(z1))))), LOG(z0, square(s(s(z1)))), SQUARE(s(s(z1))))
   LE(0', z0) -> c3
   LE(s(z0), 0') -> c4
   LE(s(z0), s(z1)) -> c5(LE(z0, z1))
   DOUBLE(0') -> c6
   DOUBLE(s(z0)) -> c7(DOUBLE(z0))
   SQUARE(0') -> c8
   SQUARE(s(z0)) -> c9(PLUS(square(z0), double(z0)), SQUARE(z0))
   SQUARE(s(z0)) -> c10(PLUS(square(z0), double(z0)), DOUBLE(z0))
   PLUS(z0, 0') -> c11
   PLUS(z0, s(z1)) -> c12(PLUS(z0, z1))

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

   log(z0, s(s(z1))) -> cond(le(z0, s(s(z1))), z0, z1)
   cond(true, z0, z1) -> s(0')
   cond(false, z0, z1) -> double(log(z0, square(s(s(z1)))))
   le(0', z0) -> true
   le(s(z0), 0') -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   double(0') -> 0'
   double(s(z0)) -> s(s(double(z0)))
   square(0') -> 0'
   square(s(z0)) -> s(plus(square(z0), double(z0)))
   plus(z0, 0') -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
LOG(z0, s(s(z1))) -> c(COND(le(z0, s(s(z1))), z0, z1), LE(z0, s(s(z1))))
COND(true, z0, z1) -> c1
COND(false, z0, z1) -> c2(DOUBLE(log(z0, square(s(s(z1))))), LOG(z0, square(s(s(z1)))), SQUARE(s(s(z1))))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
DOUBLE(0') -> c6
DOUBLE(s(z0)) -> c7(DOUBLE(z0))
SQUARE(0') -> c8
SQUARE(s(z0)) -> c9(PLUS(square(z0), double(z0)), SQUARE(z0))
SQUARE(s(z0)) -> c10(PLUS(square(z0), double(z0)), DOUBLE(z0))
PLUS(z0, 0') -> c11
PLUS(z0, s(z1)) -> c12(PLUS(z0, z1))
log(z0, s(s(z1))) -> cond(le(z0, s(s(z1))), z0, z1)
cond(true, z0, z1) -> s(0')
cond(false, z0, z1) -> double(log(z0, square(s(s(z1)))))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
square(0') -> 0'
square(s(z0)) -> s(plus(square(z0), double(z0)))
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))

Types:
LOG :: s:0' -> s:0' -> c
s :: s:0' -> s:0'
c :: c1:c2 -> c3:c4:c5 -> c
COND :: true:false -> s:0' -> s:0' -> c1:c2
le :: s:0' -> s:0' -> true:false
LE :: s:0' -> s:0' -> c3:c4:c5
true :: true:false
c1 :: c1:c2
false :: true:false
c2 :: c6:c7 -> c -> c8:c9:c10 -> c1:c2
DOUBLE :: s:0' -> c6:c7
log :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
SQUARE :: s:0' -> c8:c9:c10
0' :: s:0'
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c8:c9:c10
c9 :: c11:c12 -> c8:c9:c10 -> c8:c9:c10
PLUS :: s:0' -> s:0' -> c11:c12
double :: s:0' -> s:0'
c10 :: c11:c12 -> c6:c7 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
cond :: true:false -> s:0' -> s:0' -> s:0'
plus :: s:0' -> s:0' -> s:0'
hole_c1_13 :: c
hole_s:0'2_13 :: s:0'
hole_c1:c23_13 :: c1:c2
hole_c3:c4:c54_13 :: c3:c4:c5
hole_true:false5_13 :: true:false
hole_c6:c76_13 :: c6:c7
hole_c8:c9:c107_13 :: c8:c9:c10
hole_c11:c128_13 :: c11:c12
gen_s:0'9_13 :: Nat -> s:0'
gen_c3:c4:c510_13 :: Nat -> c3:c4:c5
gen_c6:c711_13 :: Nat -> c6:c7
gen_c8:c9:c1012_13 :: Nat -> c8:c9:c10
gen_c11:c1213_13 :: Nat -> c11:c12

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
LOG, le, LE, DOUBLE, log, square, SQUARE, PLUS, double, plus

They will be analysed ascendingly in the following order:
le < LOG
LE < LOG
DOUBLE < LOG
log < LOG
square < LOG
SQUARE < LOG
le < log
DOUBLE < SQUARE
square < log
double < log
square < SQUARE
double < square
plus < square
PLUS < SQUARE
double < SQUARE

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

(10)
Obligation:
Innermost TRS:
Rules:
LOG(z0, s(s(z1))) -> c(COND(le(z0, s(s(z1))), z0, z1), LE(z0, s(s(z1))))
COND(true, z0, z1) -> c1
COND(false, z0, z1) -> c2(DOUBLE(log(z0, square(s(s(z1))))), LOG(z0, square(s(s(z1)))), SQUARE(s(s(z1))))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
DOUBLE(0') -> c6
DOUBLE(s(z0)) -> c7(DOUBLE(z0))
SQUARE(0') -> c8
SQUARE(s(z0)) -> c9(PLUS(square(z0), double(z0)), SQUARE(z0))
SQUARE(s(z0)) -> c10(PLUS(square(z0), double(z0)), DOUBLE(z0))
PLUS(z0, 0') -> c11
PLUS(z0, s(z1)) -> c12(PLUS(z0, z1))
log(z0, s(s(z1))) -> cond(le(z0, s(s(z1))), z0, z1)
cond(true, z0, z1) -> s(0')
cond(false, z0, z1) -> double(log(z0, square(s(s(z1)))))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
square(0') -> 0'
square(s(z0)) -> s(plus(square(z0), double(z0)))
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))

Types:
LOG :: s:0' -> s:0' -> c
s :: s:0' -> s:0'
c :: c1:c2 -> c3:c4:c5 -> c
COND :: true:false -> s:0' -> s:0' -> c1:c2
le :: s:0' -> s:0' -> true:false
LE :: s:0' -> s:0' -> c3:c4:c5
true :: true:false
c1 :: c1:c2
false :: true:false
c2 :: c6:c7 -> c -> c8:c9:c10 -> c1:c2
DOUBLE :: s:0' -> c6:c7
log :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
SQUARE :: s:0' -> c8:c9:c10
0' :: s:0'
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c8:c9:c10
c9 :: c11:c12 -> c8:c9:c10 -> c8:c9:c10
PLUS :: s:0' -> s:0' -> c11:c12
double :: s:0' -> s:0'
c10 :: c11:c12 -> c6:c7 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
cond :: true:false -> s:0' -> s:0' -> s:0'
plus :: s:0' -> s:0' -> s:0'
hole_c1_13 :: c
hole_s:0'2_13 :: s:0'
hole_c1:c23_13 :: c1:c2
hole_c3:c4:c54_13 :: c3:c4:c5
hole_true:false5_13 :: true:false
hole_c6:c76_13 :: c6:c7
hole_c8:c9:c107_13 :: c8:c9:c10
hole_c11:c128_13 :: c11:c12
gen_s:0'9_13 :: Nat -> s:0'
gen_c3:c4:c510_13 :: Nat -> c3:c4:c5
gen_c6:c711_13 :: Nat -> c6:c7
gen_c8:c9:c1012_13 :: Nat -> c8:c9:c10
gen_c11:c1213_13 :: Nat -> c11:c12


Generator Equations:
gen_s:0'9_13(0) <=> 0'
gen_s:0'9_13(+(x, 1)) <=> s(gen_s:0'9_13(x))
gen_c3:c4:c510_13(0) <=> c3
gen_c3:c4:c510_13(+(x, 1)) <=> c5(gen_c3:c4:c510_13(x))
gen_c6:c711_13(0) <=> c6
gen_c6:c711_13(+(x, 1)) <=> c7(gen_c6:c711_13(x))
gen_c8:c9:c1012_13(0) <=> c8
gen_c8:c9:c1012_13(+(x, 1)) <=> c9(c11, gen_c8:c9:c1012_13(x))
gen_c11:c1213_13(0) <=> c11
gen_c11:c1213_13(+(x, 1)) <=> c12(gen_c11:c1213_13(x))


The following defined symbols remain to be analysed:
le, LOG, LE, DOUBLE, log, square, SQUARE, PLUS, double, plus

They will be analysed ascendingly in the following order:
le < LOG
LE < LOG
DOUBLE < LOG
log < LOG
square < LOG
SQUARE < LOG
le < log
DOUBLE < SQUARE
square < log
double < log
square < SQUARE
double < square
plus < square
PLUS < SQUARE
double < SQUARE

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
le(gen_s:0'9_13(n15_13), gen_s:0'9_13(n15_13)) -> true, rt in Omega(0)

Induction Base:
le(gen_s:0'9_13(0), gen_s:0'9_13(0)) ->_R^Omega(0)
true

Induction Step:
le(gen_s:0'9_13(+(n15_13, 1)), gen_s:0'9_13(+(n15_13, 1))) ->_R^Omega(0)
le(gen_s:0'9_13(n15_13), gen_s:0'9_13(n15_13)) ->_IH
true

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

(12)
Obligation:
Innermost TRS:
Rules:
LOG(z0, s(s(z1))) -> c(COND(le(z0, s(s(z1))), z0, z1), LE(z0, s(s(z1))))
COND(true, z0, z1) -> c1
COND(false, z0, z1) -> c2(DOUBLE(log(z0, square(s(s(z1))))), LOG(z0, square(s(s(z1)))), SQUARE(s(s(z1))))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
DOUBLE(0') -> c6
DOUBLE(s(z0)) -> c7(DOUBLE(z0))
SQUARE(0') -> c8
SQUARE(s(z0)) -> c9(PLUS(square(z0), double(z0)), SQUARE(z0))
SQUARE(s(z0)) -> c10(PLUS(square(z0), double(z0)), DOUBLE(z0))
PLUS(z0, 0') -> c11
PLUS(z0, s(z1)) -> c12(PLUS(z0, z1))
log(z0, s(s(z1))) -> cond(le(z0, s(s(z1))), z0, z1)
cond(true, z0, z1) -> s(0')
cond(false, z0, z1) -> double(log(z0, square(s(s(z1)))))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
square(0') -> 0'
square(s(z0)) -> s(plus(square(z0), double(z0)))
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))

Types:
LOG :: s:0' -> s:0' -> c
s :: s:0' -> s:0'
c :: c1:c2 -> c3:c4:c5 -> c
COND :: true:false -> s:0' -> s:0' -> c1:c2
le :: s:0' -> s:0' -> true:false
LE :: s:0' -> s:0' -> c3:c4:c5
true :: true:false
c1 :: c1:c2
false :: true:false
c2 :: c6:c7 -> c -> c8:c9:c10 -> c1:c2
DOUBLE :: s:0' -> c6:c7
log :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
SQUARE :: s:0' -> c8:c9:c10
0' :: s:0'
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c8:c9:c10
c9 :: c11:c12 -> c8:c9:c10 -> c8:c9:c10
PLUS :: s:0' -> s:0' -> c11:c12
double :: s:0' -> s:0'
c10 :: c11:c12 -> c6:c7 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
cond :: true:false -> s:0' -> s:0' -> s:0'
plus :: s:0' -> s:0' -> s:0'
hole_c1_13 :: c
hole_s:0'2_13 :: s:0'
hole_c1:c23_13 :: c1:c2
hole_c3:c4:c54_13 :: c3:c4:c5
hole_true:false5_13 :: true:false
hole_c6:c76_13 :: c6:c7
hole_c8:c9:c107_13 :: c8:c9:c10
hole_c11:c128_13 :: c11:c12
gen_s:0'9_13 :: Nat -> s:0'
gen_c3:c4:c510_13 :: Nat -> c3:c4:c5
gen_c6:c711_13 :: Nat -> c6:c7
gen_c8:c9:c1012_13 :: Nat -> c8:c9:c10
gen_c11:c1213_13 :: Nat -> c11:c12


Lemmas:
le(gen_s:0'9_13(n15_13), gen_s:0'9_13(n15_13)) -> true, rt in Omega(0)


Generator Equations:
gen_s:0'9_13(0) <=> 0'
gen_s:0'9_13(+(x, 1)) <=> s(gen_s:0'9_13(x))
gen_c3:c4:c510_13(0) <=> c3
gen_c3:c4:c510_13(+(x, 1)) <=> c5(gen_c3:c4:c510_13(x))
gen_c6:c711_13(0) <=> c6
gen_c6:c711_13(+(x, 1)) <=> c7(gen_c6:c711_13(x))
gen_c8:c9:c1012_13(0) <=> c8
gen_c8:c9:c1012_13(+(x, 1)) <=> c9(c11, gen_c8:c9:c1012_13(x))
gen_c11:c1213_13(0) <=> c11
gen_c11:c1213_13(+(x, 1)) <=> c12(gen_c11:c1213_13(x))


The following defined symbols remain to be analysed:
LE, LOG, DOUBLE, log, square, SQUARE, PLUS, double, plus

They will be analysed ascendingly in the following order:
LE < LOG
DOUBLE < LOG
log < LOG
square < LOG
SQUARE < LOG
DOUBLE < SQUARE
square < log
double < log
square < SQUARE
double < square
plus < square
PLUS < SQUARE
double < SQUARE

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LE(gen_s:0'9_13(n422_13), gen_s:0'9_13(n422_13)) -> gen_c3:c4:c510_13(n422_13), rt in Omega(1 + n422_13)

Induction Base:
LE(gen_s:0'9_13(0), gen_s:0'9_13(0)) ->_R^Omega(1)
c3

Induction Step:
LE(gen_s:0'9_13(+(n422_13, 1)), gen_s:0'9_13(+(n422_13, 1))) ->_R^Omega(1)
c5(LE(gen_s:0'9_13(n422_13), gen_s:0'9_13(n422_13))) ->_IH
c5(gen_c3:c4:c510_13(c423_13))

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

(14)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
LOG(z0, s(s(z1))) -> c(COND(le(z0, s(s(z1))), z0, z1), LE(z0, s(s(z1))))
COND(true, z0, z1) -> c1
COND(false, z0, z1) -> c2(DOUBLE(log(z0, square(s(s(z1))))), LOG(z0, square(s(s(z1)))), SQUARE(s(s(z1))))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
DOUBLE(0') -> c6
DOUBLE(s(z0)) -> c7(DOUBLE(z0))
SQUARE(0') -> c8
SQUARE(s(z0)) -> c9(PLUS(square(z0), double(z0)), SQUARE(z0))
SQUARE(s(z0)) -> c10(PLUS(square(z0), double(z0)), DOUBLE(z0))
PLUS(z0, 0') -> c11
PLUS(z0, s(z1)) -> c12(PLUS(z0, z1))
log(z0, s(s(z1))) -> cond(le(z0, s(s(z1))), z0, z1)
cond(true, z0, z1) -> s(0')
cond(false, z0, z1) -> double(log(z0, square(s(s(z1)))))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
square(0') -> 0'
square(s(z0)) -> s(plus(square(z0), double(z0)))
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))

Types:
LOG :: s:0' -> s:0' -> c
s :: s:0' -> s:0'
c :: c1:c2 -> c3:c4:c5 -> c
COND :: true:false -> s:0' -> s:0' -> c1:c2
le :: s:0' -> s:0' -> true:false
LE :: s:0' -> s:0' -> c3:c4:c5
true :: true:false
c1 :: c1:c2
false :: true:false
c2 :: c6:c7 -> c -> c8:c9:c10 -> c1:c2
DOUBLE :: s:0' -> c6:c7
log :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
SQUARE :: s:0' -> c8:c9:c10
0' :: s:0'
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c8:c9:c10
c9 :: c11:c12 -> c8:c9:c10 -> c8:c9:c10
PLUS :: s:0' -> s:0' -> c11:c12
double :: s:0' -> s:0'
c10 :: c11:c12 -> c6:c7 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
cond :: true:false -> s:0' -> s:0' -> s:0'
plus :: s:0' -> s:0' -> s:0'
hole_c1_13 :: c
hole_s:0'2_13 :: s:0'
hole_c1:c23_13 :: c1:c2
hole_c3:c4:c54_13 :: c3:c4:c5
hole_true:false5_13 :: true:false
hole_c6:c76_13 :: c6:c7
hole_c8:c9:c107_13 :: c8:c9:c10
hole_c11:c128_13 :: c11:c12
gen_s:0'9_13 :: Nat -> s:0'
gen_c3:c4:c510_13 :: Nat -> c3:c4:c5
gen_c6:c711_13 :: Nat -> c6:c7
gen_c8:c9:c1012_13 :: Nat -> c8:c9:c10
gen_c11:c1213_13 :: Nat -> c11:c12


Lemmas:
le(gen_s:0'9_13(n15_13), gen_s:0'9_13(n15_13)) -> true, rt in Omega(0)


Generator Equations:
gen_s:0'9_13(0) <=> 0'
gen_s:0'9_13(+(x, 1)) <=> s(gen_s:0'9_13(x))
gen_c3:c4:c510_13(0) <=> c3
gen_c3:c4:c510_13(+(x, 1)) <=> c5(gen_c3:c4:c510_13(x))
gen_c6:c711_13(0) <=> c6
gen_c6:c711_13(+(x, 1)) <=> c7(gen_c6:c711_13(x))
gen_c8:c9:c1012_13(0) <=> c8
gen_c8:c9:c1012_13(+(x, 1)) <=> c9(c11, gen_c8:c9:c1012_13(x))
gen_c11:c1213_13(0) <=> c11
gen_c11:c1213_13(+(x, 1)) <=> c12(gen_c11:c1213_13(x))


The following defined symbols remain to be analysed:
LE, LOG, DOUBLE, log, square, SQUARE, PLUS, double, plus

They will be analysed ascendingly in the following order:
LE < LOG
DOUBLE < LOG
log < LOG
square < LOG
SQUARE < LOG
DOUBLE < SQUARE
square < log
double < log
square < SQUARE
double < square
plus < square
PLUS < SQUARE
double < SQUARE

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

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

(17)
BOUNDS(n^1, INF)

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

(18)
Obligation:
Innermost TRS:
Rules:
LOG(z0, s(s(z1))) -> c(COND(le(z0, s(s(z1))), z0, z1), LE(z0, s(s(z1))))
COND(true, z0, z1) -> c1
COND(false, z0, z1) -> c2(DOUBLE(log(z0, square(s(s(z1))))), LOG(z0, square(s(s(z1)))), SQUARE(s(s(z1))))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
DOUBLE(0') -> c6
DOUBLE(s(z0)) -> c7(DOUBLE(z0))
SQUARE(0') -> c8
SQUARE(s(z0)) -> c9(PLUS(square(z0), double(z0)), SQUARE(z0))
SQUARE(s(z0)) -> c10(PLUS(square(z0), double(z0)), DOUBLE(z0))
PLUS(z0, 0') -> c11
PLUS(z0, s(z1)) -> c12(PLUS(z0, z1))
log(z0, s(s(z1))) -> cond(le(z0, s(s(z1))), z0, z1)
cond(true, z0, z1) -> s(0')
cond(false, z0, z1) -> double(log(z0, square(s(s(z1)))))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
square(0') -> 0'
square(s(z0)) -> s(plus(square(z0), double(z0)))
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))

Types:
LOG :: s:0' -> s:0' -> c
s :: s:0' -> s:0'
c :: c1:c2 -> c3:c4:c5 -> c
COND :: true:false -> s:0' -> s:0' -> c1:c2
le :: s:0' -> s:0' -> true:false
LE :: s:0' -> s:0' -> c3:c4:c5
true :: true:false
c1 :: c1:c2
false :: true:false
c2 :: c6:c7 -> c -> c8:c9:c10 -> c1:c2
DOUBLE :: s:0' -> c6:c7
log :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
SQUARE :: s:0' -> c8:c9:c10
0' :: s:0'
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c8:c9:c10
c9 :: c11:c12 -> c8:c9:c10 -> c8:c9:c10
PLUS :: s:0' -> s:0' -> c11:c12
double :: s:0' -> s:0'
c10 :: c11:c12 -> c6:c7 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
cond :: true:false -> s:0' -> s:0' -> s:0'
plus :: s:0' -> s:0' -> s:0'
hole_c1_13 :: c
hole_s:0'2_13 :: s:0'
hole_c1:c23_13 :: c1:c2
hole_c3:c4:c54_13 :: c3:c4:c5
hole_true:false5_13 :: true:false
hole_c6:c76_13 :: c6:c7
hole_c8:c9:c107_13 :: c8:c9:c10
hole_c11:c128_13 :: c11:c12
gen_s:0'9_13 :: Nat -> s:0'
gen_c3:c4:c510_13 :: Nat -> c3:c4:c5
gen_c6:c711_13 :: Nat -> c6:c7
gen_c8:c9:c1012_13 :: Nat -> c8:c9:c10
gen_c11:c1213_13 :: Nat -> c11:c12


Lemmas:
le(gen_s:0'9_13(n15_13), gen_s:0'9_13(n15_13)) -> true, rt in Omega(0)
LE(gen_s:0'9_13(n422_13), gen_s:0'9_13(n422_13)) -> gen_c3:c4:c510_13(n422_13), rt in Omega(1 + n422_13)


Generator Equations:
gen_s:0'9_13(0) <=> 0'
gen_s:0'9_13(+(x, 1)) <=> s(gen_s:0'9_13(x))
gen_c3:c4:c510_13(0) <=> c3
gen_c3:c4:c510_13(+(x, 1)) <=> c5(gen_c3:c4:c510_13(x))
gen_c6:c711_13(0) <=> c6
gen_c6:c711_13(+(x, 1)) <=> c7(gen_c6:c711_13(x))
gen_c8:c9:c1012_13(0) <=> c8
gen_c8:c9:c1012_13(+(x, 1)) <=> c9(c11, gen_c8:c9:c1012_13(x))
gen_c11:c1213_13(0) <=> c11
gen_c11:c1213_13(+(x, 1)) <=> c12(gen_c11:c1213_13(x))


The following defined symbols remain to be analysed:
DOUBLE, LOG, log, square, SQUARE, PLUS, double, plus

They will be analysed ascendingly in the following order:
DOUBLE < LOG
log < LOG
square < LOG
SQUARE < LOG
DOUBLE < SQUARE
square < log
double < log
square < SQUARE
double < square
plus < square
PLUS < SQUARE
double < SQUARE

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
DOUBLE(gen_s:0'9_13(n1108_13)) -> gen_c6:c711_13(n1108_13), rt in Omega(1 + n1108_13)

Induction Base:
DOUBLE(gen_s:0'9_13(0)) ->_R^Omega(1)
c6

Induction Step:
DOUBLE(gen_s:0'9_13(+(n1108_13, 1))) ->_R^Omega(1)
c7(DOUBLE(gen_s:0'9_13(n1108_13))) ->_IH
c7(gen_c6:c711_13(c1109_13))

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

(20)
Obligation:
Innermost TRS:
Rules:
LOG(z0, s(s(z1))) -> c(COND(le(z0, s(s(z1))), z0, z1), LE(z0, s(s(z1))))
COND(true, z0, z1) -> c1
COND(false, z0, z1) -> c2(DOUBLE(log(z0, square(s(s(z1))))), LOG(z0, square(s(s(z1)))), SQUARE(s(s(z1))))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
DOUBLE(0') -> c6
DOUBLE(s(z0)) -> c7(DOUBLE(z0))
SQUARE(0') -> c8
SQUARE(s(z0)) -> c9(PLUS(square(z0), double(z0)), SQUARE(z0))
SQUARE(s(z0)) -> c10(PLUS(square(z0), double(z0)), DOUBLE(z0))
PLUS(z0, 0') -> c11
PLUS(z0, s(z1)) -> c12(PLUS(z0, z1))
log(z0, s(s(z1))) -> cond(le(z0, s(s(z1))), z0, z1)
cond(true, z0, z1) -> s(0')
cond(false, z0, z1) -> double(log(z0, square(s(s(z1)))))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
square(0') -> 0'
square(s(z0)) -> s(plus(square(z0), double(z0)))
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))

Types:
LOG :: s:0' -> s:0' -> c
s :: s:0' -> s:0'
c :: c1:c2 -> c3:c4:c5 -> c
COND :: true:false -> s:0' -> s:0' -> c1:c2
le :: s:0' -> s:0' -> true:false
LE :: s:0' -> s:0' -> c3:c4:c5
true :: true:false
c1 :: c1:c2
false :: true:false
c2 :: c6:c7 -> c -> c8:c9:c10 -> c1:c2
DOUBLE :: s:0' -> c6:c7
log :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
SQUARE :: s:0' -> c8:c9:c10
0' :: s:0'
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c8:c9:c10
c9 :: c11:c12 -> c8:c9:c10 -> c8:c9:c10
PLUS :: s:0' -> s:0' -> c11:c12
double :: s:0' -> s:0'
c10 :: c11:c12 -> c6:c7 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
cond :: true:false -> s:0' -> s:0' -> s:0'
plus :: s:0' -> s:0' -> s:0'
hole_c1_13 :: c
hole_s:0'2_13 :: s:0'
hole_c1:c23_13 :: c1:c2
hole_c3:c4:c54_13 :: c3:c4:c5
hole_true:false5_13 :: true:false
hole_c6:c76_13 :: c6:c7
hole_c8:c9:c107_13 :: c8:c9:c10
hole_c11:c128_13 :: c11:c12
gen_s:0'9_13 :: Nat -> s:0'
gen_c3:c4:c510_13 :: Nat -> c3:c4:c5
gen_c6:c711_13 :: Nat -> c6:c7
gen_c8:c9:c1012_13 :: Nat -> c8:c9:c10
gen_c11:c1213_13 :: Nat -> c11:c12


Lemmas:
le(gen_s:0'9_13(n15_13), gen_s:0'9_13(n15_13)) -> true, rt in Omega(0)
LE(gen_s:0'9_13(n422_13), gen_s:0'9_13(n422_13)) -> gen_c3:c4:c510_13(n422_13), rt in Omega(1 + n422_13)
DOUBLE(gen_s:0'9_13(n1108_13)) -> gen_c6:c711_13(n1108_13), rt in Omega(1 + n1108_13)


Generator Equations:
gen_s:0'9_13(0) <=> 0'
gen_s:0'9_13(+(x, 1)) <=> s(gen_s:0'9_13(x))
gen_c3:c4:c510_13(0) <=> c3
gen_c3:c4:c510_13(+(x, 1)) <=> c5(gen_c3:c4:c510_13(x))
gen_c6:c711_13(0) <=> c6
gen_c6:c711_13(+(x, 1)) <=> c7(gen_c6:c711_13(x))
gen_c8:c9:c1012_13(0) <=> c8
gen_c8:c9:c1012_13(+(x, 1)) <=> c9(c11, gen_c8:c9:c1012_13(x))
gen_c11:c1213_13(0) <=> c11
gen_c11:c1213_13(+(x, 1)) <=> c12(gen_c11:c1213_13(x))


The following defined symbols remain to be analysed:
PLUS, LOG, log, square, SQUARE, double, plus

They will be analysed ascendingly in the following order:
log < LOG
square < LOG
SQUARE < LOG
square < log
double < log
square < SQUARE
double < square
plus < square
PLUS < SQUARE
double < SQUARE

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
PLUS(gen_s:0'9_13(a), gen_s:0'9_13(n1491_13)) -> gen_c11:c1213_13(n1491_13), rt in Omega(1 + n1491_13)

Induction Base:
PLUS(gen_s:0'9_13(a), gen_s:0'9_13(0)) ->_R^Omega(1)
c11

Induction Step:
PLUS(gen_s:0'9_13(a), gen_s:0'9_13(+(n1491_13, 1))) ->_R^Omega(1)
c12(PLUS(gen_s:0'9_13(a), gen_s:0'9_13(n1491_13))) ->_IH
c12(gen_c11:c1213_13(c1492_13))

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

(22)
Obligation:
Innermost TRS:
Rules:
LOG(z0, s(s(z1))) -> c(COND(le(z0, s(s(z1))), z0, z1), LE(z0, s(s(z1))))
COND(true, z0, z1) -> c1
COND(false, z0, z1) -> c2(DOUBLE(log(z0, square(s(s(z1))))), LOG(z0, square(s(s(z1)))), SQUARE(s(s(z1))))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
DOUBLE(0') -> c6
DOUBLE(s(z0)) -> c7(DOUBLE(z0))
SQUARE(0') -> c8
SQUARE(s(z0)) -> c9(PLUS(square(z0), double(z0)), SQUARE(z0))
SQUARE(s(z0)) -> c10(PLUS(square(z0), double(z0)), DOUBLE(z0))
PLUS(z0, 0') -> c11
PLUS(z0, s(z1)) -> c12(PLUS(z0, z1))
log(z0, s(s(z1))) -> cond(le(z0, s(s(z1))), z0, z1)
cond(true, z0, z1) -> s(0')
cond(false, z0, z1) -> double(log(z0, square(s(s(z1)))))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
square(0') -> 0'
square(s(z0)) -> s(plus(square(z0), double(z0)))
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))

Types:
LOG :: s:0' -> s:0' -> c
s :: s:0' -> s:0'
c :: c1:c2 -> c3:c4:c5 -> c
COND :: true:false -> s:0' -> s:0' -> c1:c2
le :: s:0' -> s:0' -> true:false
LE :: s:0' -> s:0' -> c3:c4:c5
true :: true:false
c1 :: c1:c2
false :: true:false
c2 :: c6:c7 -> c -> c8:c9:c10 -> c1:c2
DOUBLE :: s:0' -> c6:c7
log :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
SQUARE :: s:0' -> c8:c9:c10
0' :: s:0'
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c8:c9:c10
c9 :: c11:c12 -> c8:c9:c10 -> c8:c9:c10
PLUS :: s:0' -> s:0' -> c11:c12
double :: s:0' -> s:0'
c10 :: c11:c12 -> c6:c7 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
cond :: true:false -> s:0' -> s:0' -> s:0'
plus :: s:0' -> s:0' -> s:0'
hole_c1_13 :: c
hole_s:0'2_13 :: s:0'
hole_c1:c23_13 :: c1:c2
hole_c3:c4:c54_13 :: c3:c4:c5
hole_true:false5_13 :: true:false
hole_c6:c76_13 :: c6:c7
hole_c8:c9:c107_13 :: c8:c9:c10
hole_c11:c128_13 :: c11:c12
gen_s:0'9_13 :: Nat -> s:0'
gen_c3:c4:c510_13 :: Nat -> c3:c4:c5
gen_c6:c711_13 :: Nat -> c6:c7
gen_c8:c9:c1012_13 :: Nat -> c8:c9:c10
gen_c11:c1213_13 :: Nat -> c11:c12


Lemmas:
le(gen_s:0'9_13(n15_13), gen_s:0'9_13(n15_13)) -> true, rt in Omega(0)
LE(gen_s:0'9_13(n422_13), gen_s:0'9_13(n422_13)) -> gen_c3:c4:c510_13(n422_13), rt in Omega(1 + n422_13)
DOUBLE(gen_s:0'9_13(n1108_13)) -> gen_c6:c711_13(n1108_13), rt in Omega(1 + n1108_13)
PLUS(gen_s:0'9_13(a), gen_s:0'9_13(n1491_13)) -> gen_c11:c1213_13(n1491_13), rt in Omega(1 + n1491_13)


Generator Equations:
gen_s:0'9_13(0) <=> 0'
gen_s:0'9_13(+(x, 1)) <=> s(gen_s:0'9_13(x))
gen_c3:c4:c510_13(0) <=> c3
gen_c3:c4:c510_13(+(x, 1)) <=> c5(gen_c3:c4:c510_13(x))
gen_c6:c711_13(0) <=> c6
gen_c6:c711_13(+(x, 1)) <=> c7(gen_c6:c711_13(x))
gen_c8:c9:c1012_13(0) <=> c8
gen_c8:c9:c1012_13(+(x, 1)) <=> c9(c11, gen_c8:c9:c1012_13(x))
gen_c11:c1213_13(0) <=> c11
gen_c11:c1213_13(+(x, 1)) <=> c12(gen_c11:c1213_13(x))


The following defined symbols remain to be analysed:
double, LOG, log, square, SQUARE, plus

They will be analysed ascendingly in the following order:
log < LOG
square < LOG
SQUARE < LOG
square < log
double < log
square < SQUARE
double < square
plus < square
double < SQUARE

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
double(gen_s:0'9_13(n2298_13)) -> gen_s:0'9_13(*(2, n2298_13)), rt in Omega(0)

Induction Base:
double(gen_s:0'9_13(0)) ->_R^Omega(0)
0'

Induction Step:
double(gen_s:0'9_13(+(n2298_13, 1))) ->_R^Omega(0)
s(s(double(gen_s:0'9_13(n2298_13)))) ->_IH
s(s(gen_s:0'9_13(*(2, c2299_13))))

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:
LOG(z0, s(s(z1))) -> c(COND(le(z0, s(s(z1))), z0, z1), LE(z0, s(s(z1))))
COND(true, z0, z1) -> c1
COND(false, z0, z1) -> c2(DOUBLE(log(z0, square(s(s(z1))))), LOG(z0, square(s(s(z1)))), SQUARE(s(s(z1))))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
DOUBLE(0') -> c6
DOUBLE(s(z0)) -> c7(DOUBLE(z0))
SQUARE(0') -> c8
SQUARE(s(z0)) -> c9(PLUS(square(z0), double(z0)), SQUARE(z0))
SQUARE(s(z0)) -> c10(PLUS(square(z0), double(z0)), DOUBLE(z0))
PLUS(z0, 0') -> c11
PLUS(z0, s(z1)) -> c12(PLUS(z0, z1))
log(z0, s(s(z1))) -> cond(le(z0, s(s(z1))), z0, z1)
cond(true, z0, z1) -> s(0')
cond(false, z0, z1) -> double(log(z0, square(s(s(z1)))))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
square(0') -> 0'
square(s(z0)) -> s(plus(square(z0), double(z0)))
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))

Types:
LOG :: s:0' -> s:0' -> c
s :: s:0' -> s:0'
c :: c1:c2 -> c3:c4:c5 -> c
COND :: true:false -> s:0' -> s:0' -> c1:c2
le :: s:0' -> s:0' -> true:false
LE :: s:0' -> s:0' -> c3:c4:c5
true :: true:false
c1 :: c1:c2
false :: true:false
c2 :: c6:c7 -> c -> c8:c9:c10 -> c1:c2
DOUBLE :: s:0' -> c6:c7
log :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
SQUARE :: s:0' -> c8:c9:c10
0' :: s:0'
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c8:c9:c10
c9 :: c11:c12 -> c8:c9:c10 -> c8:c9:c10
PLUS :: s:0' -> s:0' -> c11:c12
double :: s:0' -> s:0'
c10 :: c11:c12 -> c6:c7 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
cond :: true:false -> s:0' -> s:0' -> s:0'
plus :: s:0' -> s:0' -> s:0'
hole_c1_13 :: c
hole_s:0'2_13 :: s:0'
hole_c1:c23_13 :: c1:c2
hole_c3:c4:c54_13 :: c3:c4:c5
hole_true:false5_13 :: true:false
hole_c6:c76_13 :: c6:c7
hole_c8:c9:c107_13 :: c8:c9:c10
hole_c11:c128_13 :: c11:c12
gen_s:0'9_13 :: Nat -> s:0'
gen_c3:c4:c510_13 :: Nat -> c3:c4:c5
gen_c6:c711_13 :: Nat -> c6:c7
gen_c8:c9:c1012_13 :: Nat -> c8:c9:c10
gen_c11:c1213_13 :: Nat -> c11:c12


Lemmas:
le(gen_s:0'9_13(n15_13), gen_s:0'9_13(n15_13)) -> true, rt in Omega(0)
LE(gen_s:0'9_13(n422_13), gen_s:0'9_13(n422_13)) -> gen_c3:c4:c510_13(n422_13), rt in Omega(1 + n422_13)
DOUBLE(gen_s:0'9_13(n1108_13)) -> gen_c6:c711_13(n1108_13), rt in Omega(1 + n1108_13)
PLUS(gen_s:0'9_13(a), gen_s:0'9_13(n1491_13)) -> gen_c11:c1213_13(n1491_13), rt in Omega(1 + n1491_13)
double(gen_s:0'9_13(n2298_13)) -> gen_s:0'9_13(*(2, n2298_13)), rt in Omega(0)


Generator Equations:
gen_s:0'9_13(0) <=> 0'
gen_s:0'9_13(+(x, 1)) <=> s(gen_s:0'9_13(x))
gen_c3:c4:c510_13(0) <=> c3
gen_c3:c4:c510_13(+(x, 1)) <=> c5(gen_c3:c4:c510_13(x))
gen_c6:c711_13(0) <=> c6
gen_c6:c711_13(+(x, 1)) <=> c7(gen_c6:c711_13(x))
gen_c8:c9:c1012_13(0) <=> c8
gen_c8:c9:c1012_13(+(x, 1)) <=> c9(c11, gen_c8:c9:c1012_13(x))
gen_c11:c1213_13(0) <=> c11
gen_c11:c1213_13(+(x, 1)) <=> c12(gen_c11:c1213_13(x))


The following defined symbols remain to be analysed:
plus, LOG, log, square, SQUARE

They will be analysed ascendingly in the following order:
log < LOG
square < LOG
SQUARE < LOG
square < log
square < SQUARE
plus < square

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
plus(gen_s:0'9_13(a), gen_s:0'9_13(n2686_13)) -> gen_s:0'9_13(+(n2686_13, a)), rt in Omega(0)

Induction Base:
plus(gen_s:0'9_13(a), gen_s:0'9_13(0)) ->_R^Omega(0)
gen_s:0'9_13(a)

Induction Step:
plus(gen_s:0'9_13(a), gen_s:0'9_13(+(n2686_13, 1))) ->_R^Omega(0)
s(plus(gen_s:0'9_13(a), gen_s:0'9_13(n2686_13))) ->_IH
s(gen_s:0'9_13(+(a, c2687_13)))

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

(26)
Obligation:
Innermost TRS:
Rules:
LOG(z0, s(s(z1))) -> c(COND(le(z0, s(s(z1))), z0, z1), LE(z0, s(s(z1))))
COND(true, z0, z1) -> c1
COND(false, z0, z1) -> c2(DOUBLE(log(z0, square(s(s(z1))))), LOG(z0, square(s(s(z1)))), SQUARE(s(s(z1))))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
DOUBLE(0') -> c6
DOUBLE(s(z0)) -> c7(DOUBLE(z0))
SQUARE(0') -> c8
SQUARE(s(z0)) -> c9(PLUS(square(z0), double(z0)), SQUARE(z0))
SQUARE(s(z0)) -> c10(PLUS(square(z0), double(z0)), DOUBLE(z0))
PLUS(z0, 0') -> c11
PLUS(z0, s(z1)) -> c12(PLUS(z0, z1))
log(z0, s(s(z1))) -> cond(le(z0, s(s(z1))), z0, z1)
cond(true, z0, z1) -> s(0')
cond(false, z0, z1) -> double(log(z0, square(s(s(z1)))))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
square(0') -> 0'
square(s(z0)) -> s(plus(square(z0), double(z0)))
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))

Types:
LOG :: s:0' -> s:0' -> c
s :: s:0' -> s:0'
c :: c1:c2 -> c3:c4:c5 -> c
COND :: true:false -> s:0' -> s:0' -> c1:c2
le :: s:0' -> s:0' -> true:false
LE :: s:0' -> s:0' -> c3:c4:c5
true :: true:false
c1 :: c1:c2
false :: true:false
c2 :: c6:c7 -> c -> c8:c9:c10 -> c1:c2
DOUBLE :: s:0' -> c6:c7
log :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
SQUARE :: s:0' -> c8:c9:c10
0' :: s:0'
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c8:c9:c10
c9 :: c11:c12 -> c8:c9:c10 -> c8:c9:c10
PLUS :: s:0' -> s:0' -> c11:c12
double :: s:0' -> s:0'
c10 :: c11:c12 -> c6:c7 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
cond :: true:false -> s:0' -> s:0' -> s:0'
plus :: s:0' -> s:0' -> s:0'
hole_c1_13 :: c
hole_s:0'2_13 :: s:0'
hole_c1:c23_13 :: c1:c2
hole_c3:c4:c54_13 :: c3:c4:c5
hole_true:false5_13 :: true:false
hole_c6:c76_13 :: c6:c7
hole_c8:c9:c107_13 :: c8:c9:c10
hole_c11:c128_13 :: c11:c12
gen_s:0'9_13 :: Nat -> s:0'
gen_c3:c4:c510_13 :: Nat -> c3:c4:c5
gen_c6:c711_13 :: Nat -> c6:c7
gen_c8:c9:c1012_13 :: Nat -> c8:c9:c10
gen_c11:c1213_13 :: Nat -> c11:c12


Lemmas:
le(gen_s:0'9_13(n15_13), gen_s:0'9_13(n15_13)) -> true, rt in Omega(0)
LE(gen_s:0'9_13(n422_13), gen_s:0'9_13(n422_13)) -> gen_c3:c4:c510_13(n422_13), rt in Omega(1 + n422_13)
DOUBLE(gen_s:0'9_13(n1108_13)) -> gen_c6:c711_13(n1108_13), rt in Omega(1 + n1108_13)
PLUS(gen_s:0'9_13(a), gen_s:0'9_13(n1491_13)) -> gen_c11:c1213_13(n1491_13), rt in Omega(1 + n1491_13)
double(gen_s:0'9_13(n2298_13)) -> gen_s:0'9_13(*(2, n2298_13)), rt in Omega(0)
plus(gen_s:0'9_13(a), gen_s:0'9_13(n2686_13)) -> gen_s:0'9_13(+(n2686_13, a)), rt in Omega(0)


Generator Equations:
gen_s:0'9_13(0) <=> 0'
gen_s:0'9_13(+(x, 1)) <=> s(gen_s:0'9_13(x))
gen_c3:c4:c510_13(0) <=> c3
gen_c3:c4:c510_13(+(x, 1)) <=> c5(gen_c3:c4:c510_13(x))
gen_c6:c711_13(0) <=> c6
gen_c6:c711_13(+(x, 1)) <=> c7(gen_c6:c711_13(x))
gen_c8:c9:c1012_13(0) <=> c8
gen_c8:c9:c1012_13(+(x, 1)) <=> c9(c11, gen_c8:c9:c1012_13(x))
gen_c11:c1213_13(0) <=> c11
gen_c11:c1213_13(+(x, 1)) <=> c12(gen_c11:c1213_13(x))


The following defined symbols remain to be analysed:
square, LOG, log, SQUARE

They will be analysed ascendingly in the following order:
log < LOG
square < LOG
SQUARE < LOG
square < log
square < SQUARE

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
square(gen_s:0'9_13(n4033_13)) -> gen_s:0'9_13(*(n4033_13, n4033_13)), rt in Omega(0)

Induction Base:
square(gen_s:0'9_13(0)) ->_R^Omega(0)
0'

Induction Step:
square(gen_s:0'9_13(+(n4033_13, 1))) ->_R^Omega(0)
s(plus(square(gen_s:0'9_13(n4033_13)), double(gen_s:0'9_13(n4033_13)))) ->_IH
s(plus(gen_s:0'9_13(*(c4034_13, c4034_13)), double(gen_s:0'9_13(n4033_13)))) ->_L^Omega(0)
s(plus(gen_s:0'9_13(*(n4033_13, n4033_13)), gen_s:0'9_13(*(2, n4033_13)))) ->_L^Omega(0)
s(gen_s:0'9_13(+(*(2, n4033_13), *(n4033_13, n4033_13))))

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

(28)
Obligation:
Innermost TRS:
Rules:
LOG(z0, s(s(z1))) -> c(COND(le(z0, s(s(z1))), z0, z1), LE(z0, s(s(z1))))
COND(true, z0, z1) -> c1
COND(false, z0, z1) -> c2(DOUBLE(log(z0, square(s(s(z1))))), LOG(z0, square(s(s(z1)))), SQUARE(s(s(z1))))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
DOUBLE(0') -> c6
DOUBLE(s(z0)) -> c7(DOUBLE(z0))
SQUARE(0') -> c8
SQUARE(s(z0)) -> c9(PLUS(square(z0), double(z0)), SQUARE(z0))
SQUARE(s(z0)) -> c10(PLUS(square(z0), double(z0)), DOUBLE(z0))
PLUS(z0, 0') -> c11
PLUS(z0, s(z1)) -> c12(PLUS(z0, z1))
log(z0, s(s(z1))) -> cond(le(z0, s(s(z1))), z0, z1)
cond(true, z0, z1) -> s(0')
cond(false, z0, z1) -> double(log(z0, square(s(s(z1)))))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
square(0') -> 0'
square(s(z0)) -> s(plus(square(z0), double(z0)))
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))

Types:
LOG :: s:0' -> s:0' -> c
s :: s:0' -> s:0'
c :: c1:c2 -> c3:c4:c5 -> c
COND :: true:false -> s:0' -> s:0' -> c1:c2
le :: s:0' -> s:0' -> true:false
LE :: s:0' -> s:0' -> c3:c4:c5
true :: true:false
c1 :: c1:c2
false :: true:false
c2 :: c6:c7 -> c -> c8:c9:c10 -> c1:c2
DOUBLE :: s:0' -> c6:c7
log :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
SQUARE :: s:0' -> c8:c9:c10
0' :: s:0'
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c8:c9:c10
c9 :: c11:c12 -> c8:c9:c10 -> c8:c9:c10
PLUS :: s:0' -> s:0' -> c11:c12
double :: s:0' -> s:0'
c10 :: c11:c12 -> c6:c7 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
cond :: true:false -> s:0' -> s:0' -> s:0'
plus :: s:0' -> s:0' -> s:0'
hole_c1_13 :: c
hole_s:0'2_13 :: s:0'
hole_c1:c23_13 :: c1:c2
hole_c3:c4:c54_13 :: c3:c4:c5
hole_true:false5_13 :: true:false
hole_c6:c76_13 :: c6:c7
hole_c8:c9:c107_13 :: c8:c9:c10
hole_c11:c128_13 :: c11:c12
gen_s:0'9_13 :: Nat -> s:0'
gen_c3:c4:c510_13 :: Nat -> c3:c4:c5
gen_c6:c711_13 :: Nat -> c6:c7
gen_c8:c9:c1012_13 :: Nat -> c8:c9:c10
gen_c11:c1213_13 :: Nat -> c11:c12


Lemmas:
le(gen_s:0'9_13(n15_13), gen_s:0'9_13(n15_13)) -> true, rt in Omega(0)
LE(gen_s:0'9_13(n422_13), gen_s:0'9_13(n422_13)) -> gen_c3:c4:c510_13(n422_13), rt in Omega(1 + n422_13)
DOUBLE(gen_s:0'9_13(n1108_13)) -> gen_c6:c711_13(n1108_13), rt in Omega(1 + n1108_13)
PLUS(gen_s:0'9_13(a), gen_s:0'9_13(n1491_13)) -> gen_c11:c1213_13(n1491_13), rt in Omega(1 + n1491_13)
double(gen_s:0'9_13(n2298_13)) -> gen_s:0'9_13(*(2, n2298_13)), rt in Omega(0)
plus(gen_s:0'9_13(a), gen_s:0'9_13(n2686_13)) -> gen_s:0'9_13(+(n2686_13, a)), rt in Omega(0)
square(gen_s:0'9_13(n4033_13)) -> gen_s:0'9_13(*(n4033_13, n4033_13)), rt in Omega(0)


Generator Equations:
gen_s:0'9_13(0) <=> 0'
gen_s:0'9_13(+(x, 1)) <=> s(gen_s:0'9_13(x))
gen_c3:c4:c510_13(0) <=> c3
gen_c3:c4:c510_13(+(x, 1)) <=> c5(gen_c3:c4:c510_13(x))
gen_c6:c711_13(0) <=> c6
gen_c6:c711_13(+(x, 1)) <=> c7(gen_c6:c711_13(x))
gen_c8:c9:c1012_13(0) <=> c8
gen_c8:c9:c1012_13(+(x, 1)) <=> c9(c11, gen_c8:c9:c1012_13(x))
gen_c11:c1213_13(0) <=> c11
gen_c11:c1213_13(+(x, 1)) <=> c12(gen_c11:c1213_13(x))


The following defined symbols remain to be analysed:
log, LOG, SQUARE

They will be analysed ascendingly in the following order:
log < LOG
SQUARE < LOG

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
SQUARE(gen_s:0'9_13(n4876_13)) -> *14_13, rt in Omega(n4876_13 + n4876_13^2)

Induction Base:
SQUARE(gen_s:0'9_13(0))

Induction Step:
SQUARE(gen_s:0'9_13(+(n4876_13, 1))) ->_R^Omega(1)
c9(PLUS(square(gen_s:0'9_13(n4876_13)), double(gen_s:0'9_13(n4876_13))), SQUARE(gen_s:0'9_13(n4876_13))) ->_L^Omega(0)
c9(PLUS(gen_s:0'9_13(*(n4876_13, n4876_13)), double(gen_s:0'9_13(n4876_13))), SQUARE(gen_s:0'9_13(n4876_13))) ->_L^Omega(0)
c9(PLUS(gen_s:0'9_13(*(n4876_13, n4876_13)), gen_s:0'9_13(*(2, n4876_13))), SQUARE(gen_s:0'9_13(n4876_13))) ->_L^Omega(1 + 2*n4876_13)
c9(gen_c11:c1213_13(*(2, n4876_13)), SQUARE(gen_s:0'9_13(n4876_13))) ->_IH
c9(gen_c11:c1213_13(*(2, n4876_13)), *14_13)

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

(30)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
LOG(z0, s(s(z1))) -> c(COND(le(z0, s(s(z1))), z0, z1), LE(z0, s(s(z1))))
COND(true, z0, z1) -> c1
COND(false, z0, z1) -> c2(DOUBLE(log(z0, square(s(s(z1))))), LOG(z0, square(s(s(z1)))), SQUARE(s(s(z1))))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
DOUBLE(0') -> c6
DOUBLE(s(z0)) -> c7(DOUBLE(z0))
SQUARE(0') -> c8
SQUARE(s(z0)) -> c9(PLUS(square(z0), double(z0)), SQUARE(z0))
SQUARE(s(z0)) -> c10(PLUS(square(z0), double(z0)), DOUBLE(z0))
PLUS(z0, 0') -> c11
PLUS(z0, s(z1)) -> c12(PLUS(z0, z1))
log(z0, s(s(z1))) -> cond(le(z0, s(s(z1))), z0, z1)
cond(true, z0, z1) -> s(0')
cond(false, z0, z1) -> double(log(z0, square(s(s(z1)))))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
square(0') -> 0'
square(s(z0)) -> s(plus(square(z0), double(z0)))
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))

Types:
LOG :: s:0' -> s:0' -> c
s :: s:0' -> s:0'
c :: c1:c2 -> c3:c4:c5 -> c
COND :: true:false -> s:0' -> s:0' -> c1:c2
le :: s:0' -> s:0' -> true:false
LE :: s:0' -> s:0' -> c3:c4:c5
true :: true:false
c1 :: c1:c2
false :: true:false
c2 :: c6:c7 -> c -> c8:c9:c10 -> c1:c2
DOUBLE :: s:0' -> c6:c7
log :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
SQUARE :: s:0' -> c8:c9:c10
0' :: s:0'
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c8:c9:c10
c9 :: c11:c12 -> c8:c9:c10 -> c8:c9:c10
PLUS :: s:0' -> s:0' -> c11:c12
double :: s:0' -> s:0'
c10 :: c11:c12 -> c6:c7 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
cond :: true:false -> s:0' -> s:0' -> s:0'
plus :: s:0' -> s:0' -> s:0'
hole_c1_13 :: c
hole_s:0'2_13 :: s:0'
hole_c1:c23_13 :: c1:c2
hole_c3:c4:c54_13 :: c3:c4:c5
hole_true:false5_13 :: true:false
hole_c6:c76_13 :: c6:c7
hole_c8:c9:c107_13 :: c8:c9:c10
hole_c11:c128_13 :: c11:c12
gen_s:0'9_13 :: Nat -> s:0'
gen_c3:c4:c510_13 :: Nat -> c3:c4:c5
gen_c6:c711_13 :: Nat -> c6:c7
gen_c8:c9:c1012_13 :: Nat -> c8:c9:c10
gen_c11:c1213_13 :: Nat -> c11:c12


Lemmas:
le(gen_s:0'9_13(n15_13), gen_s:0'9_13(n15_13)) -> true, rt in Omega(0)
LE(gen_s:0'9_13(n422_13), gen_s:0'9_13(n422_13)) -> gen_c3:c4:c510_13(n422_13), rt in Omega(1 + n422_13)
DOUBLE(gen_s:0'9_13(n1108_13)) -> gen_c6:c711_13(n1108_13), rt in Omega(1 + n1108_13)
PLUS(gen_s:0'9_13(a), gen_s:0'9_13(n1491_13)) -> gen_c11:c1213_13(n1491_13), rt in Omega(1 + n1491_13)
double(gen_s:0'9_13(n2298_13)) -> gen_s:0'9_13(*(2, n2298_13)), rt in Omega(0)
plus(gen_s:0'9_13(a), gen_s:0'9_13(n2686_13)) -> gen_s:0'9_13(+(n2686_13, a)), rt in Omega(0)
square(gen_s:0'9_13(n4033_13)) -> gen_s:0'9_13(*(n4033_13, n4033_13)), rt in Omega(0)


Generator Equations:
gen_s:0'9_13(0) <=> 0'
gen_s:0'9_13(+(x, 1)) <=> s(gen_s:0'9_13(x))
gen_c3:c4:c510_13(0) <=> c3
gen_c3:c4:c510_13(+(x, 1)) <=> c5(gen_c3:c4:c510_13(x))
gen_c6:c711_13(0) <=> c6
gen_c6:c711_13(+(x, 1)) <=> c7(gen_c6:c711_13(x))
gen_c8:c9:c1012_13(0) <=> c8
gen_c8:c9:c1012_13(+(x, 1)) <=> c9(c11, gen_c8:c9:c1012_13(x))
gen_c11:c1213_13(0) <=> c11
gen_c11:c1213_13(+(x, 1)) <=> c12(gen_c11:c1213_13(x))


The following defined symbols remain to be analysed:
SQUARE, LOG

They will be analysed ascendingly in the following order:
SQUARE < LOG

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

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

(33)
BOUNDS(n^2, INF)

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

(34)
Obligation:
Innermost TRS:
Rules:
LOG(z0, s(s(z1))) -> c(COND(le(z0, s(s(z1))), z0, z1), LE(z0, s(s(z1))))
COND(true, z0, z1) -> c1
COND(false, z0, z1) -> c2(DOUBLE(log(z0, square(s(s(z1))))), LOG(z0, square(s(s(z1)))), SQUARE(s(s(z1))))
LE(0', z0) -> c3
LE(s(z0), 0') -> c4
LE(s(z0), s(z1)) -> c5(LE(z0, z1))
DOUBLE(0') -> c6
DOUBLE(s(z0)) -> c7(DOUBLE(z0))
SQUARE(0') -> c8
SQUARE(s(z0)) -> c9(PLUS(square(z0), double(z0)), SQUARE(z0))
SQUARE(s(z0)) -> c10(PLUS(square(z0), double(z0)), DOUBLE(z0))
PLUS(z0, 0') -> c11
PLUS(z0, s(z1)) -> c12(PLUS(z0, z1))
log(z0, s(s(z1))) -> cond(le(z0, s(s(z1))), z0, z1)
cond(true, z0, z1) -> s(0')
cond(false, z0, z1) -> double(log(z0, square(s(s(z1)))))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
square(0') -> 0'
square(s(z0)) -> s(plus(square(z0), double(z0)))
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))

Types:
LOG :: s:0' -> s:0' -> c
s :: s:0' -> s:0'
c :: c1:c2 -> c3:c4:c5 -> c
COND :: true:false -> s:0' -> s:0' -> c1:c2
le :: s:0' -> s:0' -> true:false
LE :: s:0' -> s:0' -> c3:c4:c5
true :: true:false
c1 :: c1:c2
false :: true:false
c2 :: c6:c7 -> c -> c8:c9:c10 -> c1:c2
DOUBLE :: s:0' -> c6:c7
log :: s:0' -> s:0' -> s:0'
square :: s:0' -> s:0'
SQUARE :: s:0' -> c8:c9:c10
0' :: s:0'
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c8:c9:c10
c9 :: c11:c12 -> c8:c9:c10 -> c8:c9:c10
PLUS :: s:0' -> s:0' -> c11:c12
double :: s:0' -> s:0'
c10 :: c11:c12 -> c6:c7 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
cond :: true:false -> s:0' -> s:0' -> s:0'
plus :: s:0' -> s:0' -> s:0'
hole_c1_13 :: c
hole_s:0'2_13 :: s:0'
hole_c1:c23_13 :: c1:c2
hole_c3:c4:c54_13 :: c3:c4:c5
hole_true:false5_13 :: true:false
hole_c6:c76_13 :: c6:c7
hole_c8:c9:c107_13 :: c8:c9:c10
hole_c11:c128_13 :: c11:c12
gen_s:0'9_13 :: Nat -> s:0'
gen_c3:c4:c510_13 :: Nat -> c3:c4:c5
gen_c6:c711_13 :: Nat -> c6:c7
gen_c8:c9:c1012_13 :: Nat -> c8:c9:c10
gen_c11:c1213_13 :: Nat -> c11:c12


Lemmas:
le(gen_s:0'9_13(n15_13), gen_s:0'9_13(n15_13)) -> true, rt in Omega(0)
LE(gen_s:0'9_13(n422_13), gen_s:0'9_13(n422_13)) -> gen_c3:c4:c510_13(n422_13), rt in Omega(1 + n422_13)
DOUBLE(gen_s:0'9_13(n1108_13)) -> gen_c6:c711_13(n1108_13), rt in Omega(1 + n1108_13)
PLUS(gen_s:0'9_13(a), gen_s:0'9_13(n1491_13)) -> gen_c11:c1213_13(n1491_13), rt in Omega(1 + n1491_13)
double(gen_s:0'9_13(n2298_13)) -> gen_s:0'9_13(*(2, n2298_13)), rt in Omega(0)
plus(gen_s:0'9_13(a), gen_s:0'9_13(n2686_13)) -> gen_s:0'9_13(+(n2686_13, a)), rt in Omega(0)
square(gen_s:0'9_13(n4033_13)) -> gen_s:0'9_13(*(n4033_13, n4033_13)), rt in Omega(0)
SQUARE(gen_s:0'9_13(n4876_13)) -> *14_13, rt in Omega(n4876_13 + n4876_13^2)


Generator Equations:
gen_s:0'9_13(0) <=> 0'
gen_s:0'9_13(+(x, 1)) <=> s(gen_s:0'9_13(x))
gen_c3:c4:c510_13(0) <=> c3
gen_c3:c4:c510_13(+(x, 1)) <=> c5(gen_c3:c4:c510_13(x))
gen_c6:c711_13(0) <=> c6
gen_c6:c711_13(+(x, 1)) <=> c7(gen_c6:c711_13(x))
gen_c8:c9:c1012_13(0) <=> c8
gen_c8:c9:c1012_13(+(x, 1)) <=> c9(c11, gen_c8:c9:c1012_13(x))
gen_c11:c1213_13(0) <=> c11
gen_c11:c1213_13(+(x, 1)) <=> c12(gen_c11:c1213_13(x))


The following defined symbols remain to be analysed:
LOG