WORST_CASE(Omega(n^2),?)
proof of input_ZoCe3zRAM3.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), 7 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 307 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 92 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), 94 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 98 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 49 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 807 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:

   table -> gen(s(0))
   gen(x) -> if1(le(x, 10), x)
   if1(false, x) -> nil
   if1(true, x) -> if2(x, x)
   if2(x, y) -> if3(le(y, 10), x, y)
   if3(true, x, y) -> cons(entry(x, y, times(x, y)), if2(x, s(y)))
   if3(false, x, y) -> gen(s(x))
   le(0, y) -> true
   le(s(x), 0) -> false
   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))
   10 -> s(s(s(s(s(s(s(s(s(s(0))))))))))

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:
   table -> gen(s(0))
   gen(z0) -> if1(le(z0, 10), z0)
   if1(false, z0) -> nil
   if1(true, z0) -> if2(z0, z0)
   if2(z0, z1) -> if3(le(z1, 10), z0, z1)
   if3(true, z0, z1) -> cons(entry(z0, z1, times(z0, z1)), if2(z0, s(z1)))
   if3(false, z0, z1) -> gen(s(z0))
   le(0, z0) -> true
   le(s(z0), 0) -> false
   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))
   10 -> s(s(s(s(s(s(s(s(s(s(0))))))))))
Tuples:
   TABLE -> c(GEN(s(0)))
   GEN(z0) -> c1(IF1(le(z0, 10), z0), LE(z0, 10), 10')
   IF1(false, z0) -> c2
   IF1(true, z0) -> c3(IF2(z0, z0))
   IF2(z0, z1) -> c4(IF3(le(z1, 10), z0, z1), LE(z1, 10), 10')
   IF3(true, z0, z1) -> c5(TIMES(z0, z1))
   IF3(true, z0, z1) -> c6(IF2(z0, s(z1)))
   IF3(false, z0, z1) -> c7(GEN(s(z0)))
   LE(0, z0) -> c8
   LE(s(z0), 0) -> c9
   LE(s(z0), s(z1)) -> c10(LE(z0, z1))
   PLUS(0, z0) -> c11
   PLUS(s(z0), z1) -> c12(PLUS(z0, z1))
   TIMES(0, z0) -> c13
   TIMES(s(z0), z1) -> c14(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   10' -> c15
S tuples:
   TABLE -> c(GEN(s(0)))
   GEN(z0) -> c1(IF1(le(z0, 10), z0), LE(z0, 10), 10')
   IF1(false, z0) -> c2
   IF1(true, z0) -> c3(IF2(z0, z0))
   IF2(z0, z1) -> c4(IF3(le(z1, 10), z0, z1), LE(z1, 10), 10')
   IF3(true, z0, z1) -> c5(TIMES(z0, z1))
   IF3(true, z0, z1) -> c6(IF2(z0, s(z1)))
   IF3(false, z0, z1) -> c7(GEN(s(z0)))
   LE(0, z0) -> c8
   LE(s(z0), 0) -> c9
   LE(s(z0), s(z1)) -> c10(LE(z0, z1))
   PLUS(0, z0) -> c11
   PLUS(s(z0), z1) -> c12(PLUS(z0, z1))
   TIMES(0, z0) -> c13
   TIMES(s(z0), z1) -> c14(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   10' -> c15
K tuples:none
Defined Rule Symbols:   table, gen_1, if1_2, if2_2, if3_3, le_2, plus_2, times_2, 10

Defined Pair Symbols:   TABLE, GEN_1, IF1_2, IF2_2, IF3_3, LE_2, PLUS_2, TIMES_2, 10'

Compound Symbols:   c_1, c1_3, c2, c3_1, c4_3, c5_1, c6_1, c7_1, c8, c9, c10_1, c11, c12_1, c13, c14_2, c15


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

(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:

   TABLE -> c(GEN(s(0)))
   GEN(z0) -> c1(IF1(le(z0, 10), z0), LE(z0, 10), 10')
   IF1(false, z0) -> c2
   IF1(true, z0) -> c3(IF2(z0, z0))
   IF2(z0, z1) -> c4(IF3(le(z1, 10), z0, z1), LE(z1, 10), 10')
   IF3(true, z0, z1) -> c5(TIMES(z0, z1))
   IF3(true, z0, z1) -> c6(IF2(z0, s(z1)))
   IF3(false, z0, z1) -> c7(GEN(s(z0)))
   LE(0, z0) -> c8
   LE(s(z0), 0) -> c9
   LE(s(z0), s(z1)) -> c10(LE(z0, z1))
   PLUS(0, z0) -> c11
   PLUS(s(z0), z1) -> c12(PLUS(z0, z1))
   TIMES(0, z0) -> c13
   TIMES(s(z0), z1) -> c14(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   10' -> c15

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

   table -> gen(s(0))
   gen(z0) -> if1(le(z0, 10), z0)
   if1(false, z0) -> nil
   if1(true, z0) -> if2(z0, z0)
   if2(z0, z1) -> if3(le(z1, 10), z0, z1)
   if3(true, z0, z1) -> cons(entry(z0, z1, times(z0, z1)), if2(z0, s(z1)))
   if3(false, z0, z1) -> gen(s(z0))
   le(0, z0) -> true
   le(s(z0), 0) -> false
   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))
   10 -> s(s(s(s(s(s(s(s(s(s(0))))))))))

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:

   TABLE -> c(GEN(s(0')))
   GEN(z0) -> c1(IF1(le(z0, 10'), z0), LE(z0, 10'), 10')
   IF1(false, z0) -> c2
   IF1(true, z0) -> c3(IF2(z0, z0))
   IF2(z0, z1) -> c4(IF3(le(z1, 10'), z0, z1), LE(z1, 10'), 10')
   IF3(true, z0, z1) -> c5(TIMES(z0, z1))
   IF3(true, z0, z1) -> c6(IF2(z0, s(z1)))
   IF3(false, z0, z1) -> c7(GEN(s(z0)))
   LE(0', z0) -> c8
   LE(s(z0), 0') -> c9
   LE(s(z0), s(z1)) -> c10(LE(z0, z1))
   PLUS(0', z0) -> c11
   PLUS(s(z0), z1) -> c12(PLUS(z0, z1))
   TIMES(0', z0) -> c13
   TIMES(s(z0), z1) -> c14(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   10' -> c15

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

   table -> gen(s(0'))
   gen(z0) -> if1(le(z0, 10'), z0)
   if1(false, z0) -> nil
   if1(true, z0) -> if2(z0, z0)
   if2(z0, z1) -> if3(le(z1, 10'), z0, z1)
   if3(true, z0, z1) -> cons(entry(z0, z1, times(z0, z1)), if2(z0, s(z1)))
   if3(false, z0, z1) -> gen(s(z0))
   le(0', z0) -> true
   le(s(z0), 0') -> false
   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))
   10' -> s(s(s(s(s(s(s(s(s(s(0'))))))))))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
TABLE -> c(GEN(s(0')))
GEN(z0) -> c1(IF1(le(z0, 10'), z0), LE(z0, 10'), 10')
IF1(false, z0) -> c2
IF1(true, z0) -> c3(IF2(z0, z0))
IF2(z0, z1) -> c4(IF3(le(z1, 10'), z0, z1), LE(z1, 10'), 10')
IF3(true, z0, z1) -> c5(TIMES(z0, z1))
IF3(true, z0, z1) -> c6(IF2(z0, s(z1)))
IF3(false, z0, z1) -> c7(GEN(s(z0)))
LE(0', z0) -> c8
LE(s(z0), 0') -> c9
LE(s(z0), s(z1)) -> c10(LE(z0, z1))
PLUS(0', z0) -> c11
PLUS(s(z0), z1) -> c12(PLUS(z0, z1))
TIMES(0', z0) -> c13
TIMES(s(z0), z1) -> c14(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
10' -> c15
table -> gen(s(0'))
gen(z0) -> if1(le(z0, 10'), z0)
if1(false, z0) -> nil
if1(true, z0) -> if2(z0, z0)
if2(z0, z1) -> if3(le(z1, 10'), z0, z1)
if3(true, z0, z1) -> cons(entry(z0, z1, times(z0, z1)), if2(z0, s(z1)))
if3(false, z0, z1) -> gen(s(z0))
le(0', z0) -> true
le(s(z0), 0') -> false
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))
10' -> s(s(s(s(s(s(s(s(s(s(0'))))))))))

Types:
TABLE :: c
c :: c1 -> c
GEN :: 0':s:c15 -> c1
s :: 0':s:c15 -> 0':s:c15
0' :: 0':s:c15
c1 :: c2:c3 -> c8:c9:c10 -> 0':s:c15 -> c1
IF1 :: false:true -> 0':s:c15 -> c2:c3
le :: 0':s:c15 -> 0':s:c15 -> false:true
10' :: 0':s:c15
LE :: 0':s:c15 -> 0':s:c15 -> c8:c9:c10
false :: false:true
c2 :: c2:c3
true :: false:true
c3 :: c4 -> c2:c3
IF2 :: 0':s:c15 -> 0':s:c15 -> c4
c4 :: c5:c6:c7 -> c8:c9:c10 -> 0':s:c15 -> c4
IF3 :: false:true -> 0':s:c15 -> 0':s:c15 -> c5:c6:c7
c5 :: c13:c14 -> c5:c6:c7
TIMES :: 0':s:c15 -> 0':s:c15 -> c13:c14
c6 :: c4 -> c5:c6:c7
c7 :: c1 -> c5:c6:c7
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
PLUS :: 0':s:c15 -> 0':s:c15 -> c11:c12
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
c13 :: c13:c14
c14 :: c11:c12 -> c13:c14 -> c13:c14
times :: 0':s:c15 -> 0':s:c15 -> 0':s:c15
c15 :: 0':s:c15
table :: nil:cons
gen :: 0':s:c15 -> nil:cons
if1 :: false:true -> 0':s:c15 -> nil:cons
nil :: nil:cons
if2 :: 0':s:c15 -> 0':s:c15 -> nil:cons
if3 :: false:true -> 0':s:c15 -> 0':s:c15 -> nil:cons
cons :: entry -> nil:cons -> nil:cons
entry :: 0':s:c15 -> 0':s:c15 -> 0':s:c15 -> entry
plus :: 0':s:c15 -> 0':s:c15 -> 0':s:c15
hole_c1_16 :: c
hole_c12_16 :: c1
hole_0':s:c153_16 :: 0':s:c15
hole_c2:c34_16 :: c2:c3
hole_c8:c9:c105_16 :: c8:c9:c10
hole_false:true6_16 :: false:true
hole_c47_16 :: c4
hole_c5:c6:c78_16 :: c5:c6:c7
hole_c13:c149_16 :: c13:c14
hole_c11:c1210_16 :: c11:c12
hole_nil:cons11_16 :: nil:cons
hole_entry12_16 :: entry
gen_0':s:c1513_16 :: Nat -> 0':s:c15
gen_c8:c9:c1014_16 :: Nat -> c8:c9:c10
gen_c13:c1415_16 :: Nat -> c13:c14
gen_c11:c1216_16 :: Nat -> c11:c12
gen_nil:cons17_16 :: Nat -> nil:cons

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
GEN, le, LE, IF2, TIMES, PLUS, times, gen, if2, plus

They will be analysed ascendingly in the following order:
le < GEN
LE < GEN
GEN = IF2
le < IF2
le < gen
le < if2
LE < IF2
TIMES < IF2
PLUS < TIMES
times < TIMES
times < if2
plus < times
gen = if2

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

(10)
Obligation:
Innermost TRS:
Rules:
TABLE -> c(GEN(s(0')))
GEN(z0) -> c1(IF1(le(z0, 10'), z0), LE(z0, 10'), 10')
IF1(false, z0) -> c2
IF1(true, z0) -> c3(IF2(z0, z0))
IF2(z0, z1) -> c4(IF3(le(z1, 10'), z0, z1), LE(z1, 10'), 10')
IF3(true, z0, z1) -> c5(TIMES(z0, z1))
IF3(true, z0, z1) -> c6(IF2(z0, s(z1)))
IF3(false, z0, z1) -> c7(GEN(s(z0)))
LE(0', z0) -> c8
LE(s(z0), 0') -> c9
LE(s(z0), s(z1)) -> c10(LE(z0, z1))
PLUS(0', z0) -> c11
PLUS(s(z0), z1) -> c12(PLUS(z0, z1))
TIMES(0', z0) -> c13
TIMES(s(z0), z1) -> c14(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
10' -> c15
table -> gen(s(0'))
gen(z0) -> if1(le(z0, 10'), z0)
if1(false, z0) -> nil
if1(true, z0) -> if2(z0, z0)
if2(z0, z1) -> if3(le(z1, 10'), z0, z1)
if3(true, z0, z1) -> cons(entry(z0, z1, times(z0, z1)), if2(z0, s(z1)))
if3(false, z0, z1) -> gen(s(z0))
le(0', z0) -> true
le(s(z0), 0') -> false
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))
10' -> s(s(s(s(s(s(s(s(s(s(0'))))))))))

Types:
TABLE :: c
c :: c1 -> c
GEN :: 0':s:c15 -> c1
s :: 0':s:c15 -> 0':s:c15
0' :: 0':s:c15
c1 :: c2:c3 -> c8:c9:c10 -> 0':s:c15 -> c1
IF1 :: false:true -> 0':s:c15 -> c2:c3
le :: 0':s:c15 -> 0':s:c15 -> false:true
10' :: 0':s:c15
LE :: 0':s:c15 -> 0':s:c15 -> c8:c9:c10
false :: false:true
c2 :: c2:c3
true :: false:true
c3 :: c4 -> c2:c3
IF2 :: 0':s:c15 -> 0':s:c15 -> c4
c4 :: c5:c6:c7 -> c8:c9:c10 -> 0':s:c15 -> c4
IF3 :: false:true -> 0':s:c15 -> 0':s:c15 -> c5:c6:c7
c5 :: c13:c14 -> c5:c6:c7
TIMES :: 0':s:c15 -> 0':s:c15 -> c13:c14
c6 :: c4 -> c5:c6:c7
c7 :: c1 -> c5:c6:c7
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
PLUS :: 0':s:c15 -> 0':s:c15 -> c11:c12
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
c13 :: c13:c14
c14 :: c11:c12 -> c13:c14 -> c13:c14
times :: 0':s:c15 -> 0':s:c15 -> 0':s:c15
c15 :: 0':s:c15
table :: nil:cons
gen :: 0':s:c15 -> nil:cons
if1 :: false:true -> 0':s:c15 -> nil:cons
nil :: nil:cons
if2 :: 0':s:c15 -> 0':s:c15 -> nil:cons
if3 :: false:true -> 0':s:c15 -> 0':s:c15 -> nil:cons
cons :: entry -> nil:cons -> nil:cons
entry :: 0':s:c15 -> 0':s:c15 -> 0':s:c15 -> entry
plus :: 0':s:c15 -> 0':s:c15 -> 0':s:c15
hole_c1_16 :: c
hole_c12_16 :: c1
hole_0':s:c153_16 :: 0':s:c15
hole_c2:c34_16 :: c2:c3
hole_c8:c9:c105_16 :: c8:c9:c10
hole_false:true6_16 :: false:true
hole_c47_16 :: c4
hole_c5:c6:c78_16 :: c5:c6:c7
hole_c13:c149_16 :: c13:c14
hole_c11:c1210_16 :: c11:c12
hole_nil:cons11_16 :: nil:cons
hole_entry12_16 :: entry
gen_0':s:c1513_16 :: Nat -> 0':s:c15
gen_c8:c9:c1014_16 :: Nat -> c8:c9:c10
gen_c13:c1415_16 :: Nat -> c13:c14
gen_c11:c1216_16 :: Nat -> c11:c12
gen_nil:cons17_16 :: Nat -> nil:cons


Generator Equations:
gen_0':s:c1513_16(0) <=> 0'
gen_0':s:c1513_16(+(x, 1)) <=> s(gen_0':s:c1513_16(x))
gen_c8:c9:c1014_16(0) <=> c8
gen_c8:c9:c1014_16(+(x, 1)) <=> c10(gen_c8:c9:c1014_16(x))
gen_c13:c1415_16(0) <=> c13
gen_c13:c1415_16(+(x, 1)) <=> c14(c11, gen_c13:c1415_16(x))
gen_c11:c1216_16(0) <=> c11
gen_c11:c1216_16(+(x, 1)) <=> c12(gen_c11:c1216_16(x))
gen_nil:cons17_16(0) <=> nil
gen_nil:cons17_16(+(x, 1)) <=> cons(entry(0', 0', 0'), gen_nil:cons17_16(x))


The following defined symbols remain to be analysed:
le, GEN, LE, IF2, TIMES, PLUS, times, gen, if2, plus

They will be analysed ascendingly in the following order:
le < GEN
LE < GEN
GEN = IF2
le < IF2
le < gen
le < if2
LE < IF2
TIMES < IF2
PLUS < TIMES
times < TIMES
times < if2
plus < times
gen = if2

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
le(gen_0':s:c1513_16(n19_16), gen_0':s:c1513_16(n19_16)) -> true, rt in Omega(0)

Induction Base:
le(gen_0':s:c1513_16(0), gen_0':s:c1513_16(0)) ->_R^Omega(0)
true

Induction Step:
le(gen_0':s:c1513_16(+(n19_16, 1)), gen_0':s:c1513_16(+(n19_16, 1))) ->_R^Omega(0)
le(gen_0':s:c1513_16(n19_16), gen_0':s:c1513_16(n19_16)) ->_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:
TABLE -> c(GEN(s(0')))
GEN(z0) -> c1(IF1(le(z0, 10'), z0), LE(z0, 10'), 10')
IF1(false, z0) -> c2
IF1(true, z0) -> c3(IF2(z0, z0))
IF2(z0, z1) -> c4(IF3(le(z1, 10'), z0, z1), LE(z1, 10'), 10')
IF3(true, z0, z1) -> c5(TIMES(z0, z1))
IF3(true, z0, z1) -> c6(IF2(z0, s(z1)))
IF3(false, z0, z1) -> c7(GEN(s(z0)))
LE(0', z0) -> c8
LE(s(z0), 0') -> c9
LE(s(z0), s(z1)) -> c10(LE(z0, z1))
PLUS(0', z0) -> c11
PLUS(s(z0), z1) -> c12(PLUS(z0, z1))
TIMES(0', z0) -> c13
TIMES(s(z0), z1) -> c14(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
10' -> c15
table -> gen(s(0'))
gen(z0) -> if1(le(z0, 10'), z0)
if1(false, z0) -> nil
if1(true, z0) -> if2(z0, z0)
if2(z0, z1) -> if3(le(z1, 10'), z0, z1)
if3(true, z0, z1) -> cons(entry(z0, z1, times(z0, z1)), if2(z0, s(z1)))
if3(false, z0, z1) -> gen(s(z0))
le(0', z0) -> true
le(s(z0), 0') -> false
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))
10' -> s(s(s(s(s(s(s(s(s(s(0'))))))))))

Types:
TABLE :: c
c :: c1 -> c
GEN :: 0':s:c15 -> c1
s :: 0':s:c15 -> 0':s:c15
0' :: 0':s:c15
c1 :: c2:c3 -> c8:c9:c10 -> 0':s:c15 -> c1
IF1 :: false:true -> 0':s:c15 -> c2:c3
le :: 0':s:c15 -> 0':s:c15 -> false:true
10' :: 0':s:c15
LE :: 0':s:c15 -> 0':s:c15 -> c8:c9:c10
false :: false:true
c2 :: c2:c3
true :: false:true
c3 :: c4 -> c2:c3
IF2 :: 0':s:c15 -> 0':s:c15 -> c4
c4 :: c5:c6:c7 -> c8:c9:c10 -> 0':s:c15 -> c4
IF3 :: false:true -> 0':s:c15 -> 0':s:c15 -> c5:c6:c7
c5 :: c13:c14 -> c5:c6:c7
TIMES :: 0':s:c15 -> 0':s:c15 -> c13:c14
c6 :: c4 -> c5:c6:c7
c7 :: c1 -> c5:c6:c7
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
PLUS :: 0':s:c15 -> 0':s:c15 -> c11:c12
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
c13 :: c13:c14
c14 :: c11:c12 -> c13:c14 -> c13:c14
times :: 0':s:c15 -> 0':s:c15 -> 0':s:c15
c15 :: 0':s:c15
table :: nil:cons
gen :: 0':s:c15 -> nil:cons
if1 :: false:true -> 0':s:c15 -> nil:cons
nil :: nil:cons
if2 :: 0':s:c15 -> 0':s:c15 -> nil:cons
if3 :: false:true -> 0':s:c15 -> 0':s:c15 -> nil:cons
cons :: entry -> nil:cons -> nil:cons
entry :: 0':s:c15 -> 0':s:c15 -> 0':s:c15 -> entry
plus :: 0':s:c15 -> 0':s:c15 -> 0':s:c15
hole_c1_16 :: c
hole_c12_16 :: c1
hole_0':s:c153_16 :: 0':s:c15
hole_c2:c34_16 :: c2:c3
hole_c8:c9:c105_16 :: c8:c9:c10
hole_false:true6_16 :: false:true
hole_c47_16 :: c4
hole_c5:c6:c78_16 :: c5:c6:c7
hole_c13:c149_16 :: c13:c14
hole_c11:c1210_16 :: c11:c12
hole_nil:cons11_16 :: nil:cons
hole_entry12_16 :: entry
gen_0':s:c1513_16 :: Nat -> 0':s:c15
gen_c8:c9:c1014_16 :: Nat -> c8:c9:c10
gen_c13:c1415_16 :: Nat -> c13:c14
gen_c11:c1216_16 :: Nat -> c11:c12
gen_nil:cons17_16 :: Nat -> nil:cons


Lemmas:
le(gen_0':s:c1513_16(n19_16), gen_0':s:c1513_16(n19_16)) -> true, rt in Omega(0)


Generator Equations:
gen_0':s:c1513_16(0) <=> 0'
gen_0':s:c1513_16(+(x, 1)) <=> s(gen_0':s:c1513_16(x))
gen_c8:c9:c1014_16(0) <=> c8
gen_c8:c9:c1014_16(+(x, 1)) <=> c10(gen_c8:c9:c1014_16(x))
gen_c13:c1415_16(0) <=> c13
gen_c13:c1415_16(+(x, 1)) <=> c14(c11, gen_c13:c1415_16(x))
gen_c11:c1216_16(0) <=> c11
gen_c11:c1216_16(+(x, 1)) <=> c12(gen_c11:c1216_16(x))
gen_nil:cons17_16(0) <=> nil
gen_nil:cons17_16(+(x, 1)) <=> cons(entry(0', 0', 0'), gen_nil:cons17_16(x))


The following defined symbols remain to be analysed:
LE, GEN, IF2, TIMES, PLUS, times, gen, if2, plus

They will be analysed ascendingly in the following order:
LE < GEN
GEN = IF2
LE < IF2
TIMES < IF2
PLUS < TIMES
times < TIMES
times < if2
plus < times
gen = if2

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LE(gen_0':s:c1513_16(n444_16), gen_0':s:c1513_16(n444_16)) -> gen_c8:c9:c1014_16(n444_16), rt in Omega(1 + n444_16)

Induction Base:
LE(gen_0':s:c1513_16(0), gen_0':s:c1513_16(0)) ->_R^Omega(1)
c8

Induction Step:
LE(gen_0':s:c1513_16(+(n444_16, 1)), gen_0':s:c1513_16(+(n444_16, 1))) ->_R^Omega(1)
c10(LE(gen_0':s:c1513_16(n444_16), gen_0':s:c1513_16(n444_16))) ->_IH
c10(gen_c8:c9:c1014_16(c445_16))

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:
TABLE -> c(GEN(s(0')))
GEN(z0) -> c1(IF1(le(z0, 10'), z0), LE(z0, 10'), 10')
IF1(false, z0) -> c2
IF1(true, z0) -> c3(IF2(z0, z0))
IF2(z0, z1) -> c4(IF3(le(z1, 10'), z0, z1), LE(z1, 10'), 10')
IF3(true, z0, z1) -> c5(TIMES(z0, z1))
IF3(true, z0, z1) -> c6(IF2(z0, s(z1)))
IF3(false, z0, z1) -> c7(GEN(s(z0)))
LE(0', z0) -> c8
LE(s(z0), 0') -> c9
LE(s(z0), s(z1)) -> c10(LE(z0, z1))
PLUS(0', z0) -> c11
PLUS(s(z0), z1) -> c12(PLUS(z0, z1))
TIMES(0', z0) -> c13
TIMES(s(z0), z1) -> c14(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
10' -> c15
table -> gen(s(0'))
gen(z0) -> if1(le(z0, 10'), z0)
if1(false, z0) -> nil
if1(true, z0) -> if2(z0, z0)
if2(z0, z1) -> if3(le(z1, 10'), z0, z1)
if3(true, z0, z1) -> cons(entry(z0, z1, times(z0, z1)), if2(z0, s(z1)))
if3(false, z0, z1) -> gen(s(z0))
le(0', z0) -> true
le(s(z0), 0') -> false
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))
10' -> s(s(s(s(s(s(s(s(s(s(0'))))))))))

Types:
TABLE :: c
c :: c1 -> c
GEN :: 0':s:c15 -> c1
s :: 0':s:c15 -> 0':s:c15
0' :: 0':s:c15
c1 :: c2:c3 -> c8:c9:c10 -> 0':s:c15 -> c1
IF1 :: false:true -> 0':s:c15 -> c2:c3
le :: 0':s:c15 -> 0':s:c15 -> false:true
10' :: 0':s:c15
LE :: 0':s:c15 -> 0':s:c15 -> c8:c9:c10
false :: false:true
c2 :: c2:c3
true :: false:true
c3 :: c4 -> c2:c3
IF2 :: 0':s:c15 -> 0':s:c15 -> c4
c4 :: c5:c6:c7 -> c8:c9:c10 -> 0':s:c15 -> c4
IF3 :: false:true -> 0':s:c15 -> 0':s:c15 -> c5:c6:c7
c5 :: c13:c14 -> c5:c6:c7
TIMES :: 0':s:c15 -> 0':s:c15 -> c13:c14
c6 :: c4 -> c5:c6:c7
c7 :: c1 -> c5:c6:c7
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
PLUS :: 0':s:c15 -> 0':s:c15 -> c11:c12
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
c13 :: c13:c14
c14 :: c11:c12 -> c13:c14 -> c13:c14
times :: 0':s:c15 -> 0':s:c15 -> 0':s:c15
c15 :: 0':s:c15
table :: nil:cons
gen :: 0':s:c15 -> nil:cons
if1 :: false:true -> 0':s:c15 -> nil:cons
nil :: nil:cons
if2 :: 0':s:c15 -> 0':s:c15 -> nil:cons
if3 :: false:true -> 0':s:c15 -> 0':s:c15 -> nil:cons
cons :: entry -> nil:cons -> nil:cons
entry :: 0':s:c15 -> 0':s:c15 -> 0':s:c15 -> entry
plus :: 0':s:c15 -> 0':s:c15 -> 0':s:c15
hole_c1_16 :: c
hole_c12_16 :: c1
hole_0':s:c153_16 :: 0':s:c15
hole_c2:c34_16 :: c2:c3
hole_c8:c9:c105_16 :: c8:c9:c10
hole_false:true6_16 :: false:true
hole_c47_16 :: c4
hole_c5:c6:c78_16 :: c5:c6:c7
hole_c13:c149_16 :: c13:c14
hole_c11:c1210_16 :: c11:c12
hole_nil:cons11_16 :: nil:cons
hole_entry12_16 :: entry
gen_0':s:c1513_16 :: Nat -> 0':s:c15
gen_c8:c9:c1014_16 :: Nat -> c8:c9:c10
gen_c13:c1415_16 :: Nat -> c13:c14
gen_c11:c1216_16 :: Nat -> c11:c12
gen_nil:cons17_16 :: Nat -> nil:cons


Lemmas:
le(gen_0':s:c1513_16(n19_16), gen_0':s:c1513_16(n19_16)) -> true, rt in Omega(0)


Generator Equations:
gen_0':s:c1513_16(0) <=> 0'
gen_0':s:c1513_16(+(x, 1)) <=> s(gen_0':s:c1513_16(x))
gen_c8:c9:c1014_16(0) <=> c8
gen_c8:c9:c1014_16(+(x, 1)) <=> c10(gen_c8:c9:c1014_16(x))
gen_c13:c1415_16(0) <=> c13
gen_c13:c1415_16(+(x, 1)) <=> c14(c11, gen_c13:c1415_16(x))
gen_c11:c1216_16(0) <=> c11
gen_c11:c1216_16(+(x, 1)) <=> c12(gen_c11:c1216_16(x))
gen_nil:cons17_16(0) <=> nil
gen_nil:cons17_16(+(x, 1)) <=> cons(entry(0', 0', 0'), gen_nil:cons17_16(x))


The following defined symbols remain to be analysed:
LE, GEN, IF2, TIMES, PLUS, times, gen, if2, plus

They will be analysed ascendingly in the following order:
LE < GEN
GEN = IF2
LE < IF2
TIMES < IF2
PLUS < TIMES
times < TIMES
times < if2
plus < times
gen = if2

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

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

(17)
BOUNDS(n^1, INF)

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

(18)
Obligation:
Innermost TRS:
Rules:
TABLE -> c(GEN(s(0')))
GEN(z0) -> c1(IF1(le(z0, 10'), z0), LE(z0, 10'), 10')
IF1(false, z0) -> c2
IF1(true, z0) -> c3(IF2(z0, z0))
IF2(z0, z1) -> c4(IF3(le(z1, 10'), z0, z1), LE(z1, 10'), 10')
IF3(true, z0, z1) -> c5(TIMES(z0, z1))
IF3(true, z0, z1) -> c6(IF2(z0, s(z1)))
IF3(false, z0, z1) -> c7(GEN(s(z0)))
LE(0', z0) -> c8
LE(s(z0), 0') -> c9
LE(s(z0), s(z1)) -> c10(LE(z0, z1))
PLUS(0', z0) -> c11
PLUS(s(z0), z1) -> c12(PLUS(z0, z1))
TIMES(0', z0) -> c13
TIMES(s(z0), z1) -> c14(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
10' -> c15
table -> gen(s(0'))
gen(z0) -> if1(le(z0, 10'), z0)
if1(false, z0) -> nil
if1(true, z0) -> if2(z0, z0)
if2(z0, z1) -> if3(le(z1, 10'), z0, z1)
if3(true, z0, z1) -> cons(entry(z0, z1, times(z0, z1)), if2(z0, s(z1)))
if3(false, z0, z1) -> gen(s(z0))
le(0', z0) -> true
le(s(z0), 0') -> false
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))
10' -> s(s(s(s(s(s(s(s(s(s(0'))))))))))

Types:
TABLE :: c
c :: c1 -> c
GEN :: 0':s:c15 -> c1
s :: 0':s:c15 -> 0':s:c15
0' :: 0':s:c15
c1 :: c2:c3 -> c8:c9:c10 -> 0':s:c15 -> c1
IF1 :: false:true -> 0':s:c15 -> c2:c3
le :: 0':s:c15 -> 0':s:c15 -> false:true
10' :: 0':s:c15
LE :: 0':s:c15 -> 0':s:c15 -> c8:c9:c10
false :: false:true
c2 :: c2:c3
true :: false:true
c3 :: c4 -> c2:c3
IF2 :: 0':s:c15 -> 0':s:c15 -> c4
c4 :: c5:c6:c7 -> c8:c9:c10 -> 0':s:c15 -> c4
IF3 :: false:true -> 0':s:c15 -> 0':s:c15 -> c5:c6:c7
c5 :: c13:c14 -> c5:c6:c7
TIMES :: 0':s:c15 -> 0':s:c15 -> c13:c14
c6 :: c4 -> c5:c6:c7
c7 :: c1 -> c5:c6:c7
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
PLUS :: 0':s:c15 -> 0':s:c15 -> c11:c12
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
c13 :: c13:c14
c14 :: c11:c12 -> c13:c14 -> c13:c14
times :: 0':s:c15 -> 0':s:c15 -> 0':s:c15
c15 :: 0':s:c15
table :: nil:cons
gen :: 0':s:c15 -> nil:cons
if1 :: false:true -> 0':s:c15 -> nil:cons
nil :: nil:cons
if2 :: 0':s:c15 -> 0':s:c15 -> nil:cons
if3 :: false:true -> 0':s:c15 -> 0':s:c15 -> nil:cons
cons :: entry -> nil:cons -> nil:cons
entry :: 0':s:c15 -> 0':s:c15 -> 0':s:c15 -> entry
plus :: 0':s:c15 -> 0':s:c15 -> 0':s:c15
hole_c1_16 :: c
hole_c12_16 :: c1
hole_0':s:c153_16 :: 0':s:c15
hole_c2:c34_16 :: c2:c3
hole_c8:c9:c105_16 :: c8:c9:c10
hole_false:true6_16 :: false:true
hole_c47_16 :: c4
hole_c5:c6:c78_16 :: c5:c6:c7
hole_c13:c149_16 :: c13:c14
hole_c11:c1210_16 :: c11:c12
hole_nil:cons11_16 :: nil:cons
hole_entry12_16 :: entry
gen_0':s:c1513_16 :: Nat -> 0':s:c15
gen_c8:c9:c1014_16 :: Nat -> c8:c9:c10
gen_c13:c1415_16 :: Nat -> c13:c14
gen_c11:c1216_16 :: Nat -> c11:c12
gen_nil:cons17_16 :: Nat -> nil:cons


Lemmas:
le(gen_0':s:c1513_16(n19_16), gen_0':s:c1513_16(n19_16)) -> true, rt in Omega(0)
LE(gen_0':s:c1513_16(n444_16), gen_0':s:c1513_16(n444_16)) -> gen_c8:c9:c1014_16(n444_16), rt in Omega(1 + n444_16)


Generator Equations:
gen_0':s:c1513_16(0) <=> 0'
gen_0':s:c1513_16(+(x, 1)) <=> s(gen_0':s:c1513_16(x))
gen_c8:c9:c1014_16(0) <=> c8
gen_c8:c9:c1014_16(+(x, 1)) <=> c10(gen_c8:c9:c1014_16(x))
gen_c13:c1415_16(0) <=> c13
gen_c13:c1415_16(+(x, 1)) <=> c14(c11, gen_c13:c1415_16(x))
gen_c11:c1216_16(0) <=> c11
gen_c11:c1216_16(+(x, 1)) <=> c12(gen_c11:c1216_16(x))
gen_nil:cons17_16(0) <=> nil
gen_nil:cons17_16(+(x, 1)) <=> cons(entry(0', 0', 0'), gen_nil:cons17_16(x))


The following defined symbols remain to be analysed:
PLUS, GEN, IF2, TIMES, times, gen, if2, plus

They will be analysed ascendingly in the following order:
GEN = IF2
TIMES < IF2
PLUS < TIMES
times < TIMES
times < if2
plus < times
gen = if2

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
PLUS(gen_0':s:c1513_16(n1154_16), gen_0':s:c1513_16(b)) -> gen_c11:c1216_16(n1154_16), rt in Omega(1 + n1154_16)

Induction Base:
PLUS(gen_0':s:c1513_16(0), gen_0':s:c1513_16(b)) ->_R^Omega(1)
c11

Induction Step:
PLUS(gen_0':s:c1513_16(+(n1154_16, 1)), gen_0':s:c1513_16(b)) ->_R^Omega(1)
c12(PLUS(gen_0':s:c1513_16(n1154_16), gen_0':s:c1513_16(b))) ->_IH
c12(gen_c11:c1216_16(c1155_16))

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:
TABLE -> c(GEN(s(0')))
GEN(z0) -> c1(IF1(le(z0, 10'), z0), LE(z0, 10'), 10')
IF1(false, z0) -> c2
IF1(true, z0) -> c3(IF2(z0, z0))
IF2(z0, z1) -> c4(IF3(le(z1, 10'), z0, z1), LE(z1, 10'), 10')
IF3(true, z0, z1) -> c5(TIMES(z0, z1))
IF3(true, z0, z1) -> c6(IF2(z0, s(z1)))
IF3(false, z0, z1) -> c7(GEN(s(z0)))
LE(0', z0) -> c8
LE(s(z0), 0') -> c9
LE(s(z0), s(z1)) -> c10(LE(z0, z1))
PLUS(0', z0) -> c11
PLUS(s(z0), z1) -> c12(PLUS(z0, z1))
TIMES(0', z0) -> c13
TIMES(s(z0), z1) -> c14(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
10' -> c15
table -> gen(s(0'))
gen(z0) -> if1(le(z0, 10'), z0)
if1(false, z0) -> nil
if1(true, z0) -> if2(z0, z0)
if2(z0, z1) -> if3(le(z1, 10'), z0, z1)
if3(true, z0, z1) -> cons(entry(z0, z1, times(z0, z1)), if2(z0, s(z1)))
if3(false, z0, z1) -> gen(s(z0))
le(0', z0) -> true
le(s(z0), 0') -> false
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))
10' -> s(s(s(s(s(s(s(s(s(s(0'))))))))))

Types:
TABLE :: c
c :: c1 -> c
GEN :: 0':s:c15 -> c1
s :: 0':s:c15 -> 0':s:c15
0' :: 0':s:c15
c1 :: c2:c3 -> c8:c9:c10 -> 0':s:c15 -> c1
IF1 :: false:true -> 0':s:c15 -> c2:c3
le :: 0':s:c15 -> 0':s:c15 -> false:true
10' :: 0':s:c15
LE :: 0':s:c15 -> 0':s:c15 -> c8:c9:c10
false :: false:true
c2 :: c2:c3
true :: false:true
c3 :: c4 -> c2:c3
IF2 :: 0':s:c15 -> 0':s:c15 -> c4
c4 :: c5:c6:c7 -> c8:c9:c10 -> 0':s:c15 -> c4
IF3 :: false:true -> 0':s:c15 -> 0':s:c15 -> c5:c6:c7
c5 :: c13:c14 -> c5:c6:c7
TIMES :: 0':s:c15 -> 0':s:c15 -> c13:c14
c6 :: c4 -> c5:c6:c7
c7 :: c1 -> c5:c6:c7
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
PLUS :: 0':s:c15 -> 0':s:c15 -> c11:c12
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
c13 :: c13:c14
c14 :: c11:c12 -> c13:c14 -> c13:c14
times :: 0':s:c15 -> 0':s:c15 -> 0':s:c15
c15 :: 0':s:c15
table :: nil:cons
gen :: 0':s:c15 -> nil:cons
if1 :: false:true -> 0':s:c15 -> nil:cons
nil :: nil:cons
if2 :: 0':s:c15 -> 0':s:c15 -> nil:cons
if3 :: false:true -> 0':s:c15 -> 0':s:c15 -> nil:cons
cons :: entry -> nil:cons -> nil:cons
entry :: 0':s:c15 -> 0':s:c15 -> 0':s:c15 -> entry
plus :: 0':s:c15 -> 0':s:c15 -> 0':s:c15
hole_c1_16 :: c
hole_c12_16 :: c1
hole_0':s:c153_16 :: 0':s:c15
hole_c2:c34_16 :: c2:c3
hole_c8:c9:c105_16 :: c8:c9:c10
hole_false:true6_16 :: false:true
hole_c47_16 :: c4
hole_c5:c6:c78_16 :: c5:c6:c7
hole_c13:c149_16 :: c13:c14
hole_c11:c1210_16 :: c11:c12
hole_nil:cons11_16 :: nil:cons
hole_entry12_16 :: entry
gen_0':s:c1513_16 :: Nat -> 0':s:c15
gen_c8:c9:c1014_16 :: Nat -> c8:c9:c10
gen_c13:c1415_16 :: Nat -> c13:c14
gen_c11:c1216_16 :: Nat -> c11:c12
gen_nil:cons17_16 :: Nat -> nil:cons


Lemmas:
le(gen_0':s:c1513_16(n19_16), gen_0':s:c1513_16(n19_16)) -> true, rt in Omega(0)
LE(gen_0':s:c1513_16(n444_16), gen_0':s:c1513_16(n444_16)) -> gen_c8:c9:c1014_16(n444_16), rt in Omega(1 + n444_16)
PLUS(gen_0':s:c1513_16(n1154_16), gen_0':s:c1513_16(b)) -> gen_c11:c1216_16(n1154_16), rt in Omega(1 + n1154_16)


Generator Equations:
gen_0':s:c1513_16(0) <=> 0'
gen_0':s:c1513_16(+(x, 1)) <=> s(gen_0':s:c1513_16(x))
gen_c8:c9:c1014_16(0) <=> c8
gen_c8:c9:c1014_16(+(x, 1)) <=> c10(gen_c8:c9:c1014_16(x))
gen_c13:c1415_16(0) <=> c13
gen_c13:c1415_16(+(x, 1)) <=> c14(c11, gen_c13:c1415_16(x))
gen_c11:c1216_16(0) <=> c11
gen_c11:c1216_16(+(x, 1)) <=> c12(gen_c11:c1216_16(x))
gen_nil:cons17_16(0) <=> nil
gen_nil:cons17_16(+(x, 1)) <=> cons(entry(0', 0', 0'), gen_nil:cons17_16(x))


The following defined symbols remain to be analysed:
plus, GEN, IF2, TIMES, times, gen, if2

They will be analysed ascendingly in the following order:
GEN = IF2
TIMES < IF2
times < TIMES
times < if2
plus < times
gen = if2

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

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

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

Induction Step:
plus(gen_0':s:c1513_16(+(n1974_16, 1)), gen_0':s:c1513_16(b)) ->_R^Omega(0)
s(plus(gen_0':s:c1513_16(n1974_16), gen_0':s:c1513_16(b))) ->_IH
s(gen_0':s:c1513_16(+(b, c1975_16)))

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:
TABLE -> c(GEN(s(0')))
GEN(z0) -> c1(IF1(le(z0, 10'), z0), LE(z0, 10'), 10')
IF1(false, z0) -> c2
IF1(true, z0) -> c3(IF2(z0, z0))
IF2(z0, z1) -> c4(IF3(le(z1, 10'), z0, z1), LE(z1, 10'), 10')
IF3(true, z0, z1) -> c5(TIMES(z0, z1))
IF3(true, z0, z1) -> c6(IF2(z0, s(z1)))
IF3(false, z0, z1) -> c7(GEN(s(z0)))
LE(0', z0) -> c8
LE(s(z0), 0') -> c9
LE(s(z0), s(z1)) -> c10(LE(z0, z1))
PLUS(0', z0) -> c11
PLUS(s(z0), z1) -> c12(PLUS(z0, z1))
TIMES(0', z0) -> c13
TIMES(s(z0), z1) -> c14(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
10' -> c15
table -> gen(s(0'))
gen(z0) -> if1(le(z0, 10'), z0)
if1(false, z0) -> nil
if1(true, z0) -> if2(z0, z0)
if2(z0, z1) -> if3(le(z1, 10'), z0, z1)
if3(true, z0, z1) -> cons(entry(z0, z1, times(z0, z1)), if2(z0, s(z1)))
if3(false, z0, z1) -> gen(s(z0))
le(0', z0) -> true
le(s(z0), 0') -> false
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))
10' -> s(s(s(s(s(s(s(s(s(s(0'))))))))))

Types:
TABLE :: c
c :: c1 -> c
GEN :: 0':s:c15 -> c1
s :: 0':s:c15 -> 0':s:c15
0' :: 0':s:c15
c1 :: c2:c3 -> c8:c9:c10 -> 0':s:c15 -> c1
IF1 :: false:true -> 0':s:c15 -> c2:c3
le :: 0':s:c15 -> 0':s:c15 -> false:true
10' :: 0':s:c15
LE :: 0':s:c15 -> 0':s:c15 -> c8:c9:c10
false :: false:true
c2 :: c2:c3
true :: false:true
c3 :: c4 -> c2:c3
IF2 :: 0':s:c15 -> 0':s:c15 -> c4
c4 :: c5:c6:c7 -> c8:c9:c10 -> 0':s:c15 -> c4
IF3 :: false:true -> 0':s:c15 -> 0':s:c15 -> c5:c6:c7
c5 :: c13:c14 -> c5:c6:c7
TIMES :: 0':s:c15 -> 0':s:c15 -> c13:c14
c6 :: c4 -> c5:c6:c7
c7 :: c1 -> c5:c6:c7
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
PLUS :: 0':s:c15 -> 0':s:c15 -> c11:c12
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
c13 :: c13:c14
c14 :: c11:c12 -> c13:c14 -> c13:c14
times :: 0':s:c15 -> 0':s:c15 -> 0':s:c15
c15 :: 0':s:c15
table :: nil:cons
gen :: 0':s:c15 -> nil:cons
if1 :: false:true -> 0':s:c15 -> nil:cons
nil :: nil:cons
if2 :: 0':s:c15 -> 0':s:c15 -> nil:cons
if3 :: false:true -> 0':s:c15 -> 0':s:c15 -> nil:cons
cons :: entry -> nil:cons -> nil:cons
entry :: 0':s:c15 -> 0':s:c15 -> 0':s:c15 -> entry
plus :: 0':s:c15 -> 0':s:c15 -> 0':s:c15
hole_c1_16 :: c
hole_c12_16 :: c1
hole_0':s:c153_16 :: 0':s:c15
hole_c2:c34_16 :: c2:c3
hole_c8:c9:c105_16 :: c8:c9:c10
hole_false:true6_16 :: false:true
hole_c47_16 :: c4
hole_c5:c6:c78_16 :: c5:c6:c7
hole_c13:c149_16 :: c13:c14
hole_c11:c1210_16 :: c11:c12
hole_nil:cons11_16 :: nil:cons
hole_entry12_16 :: entry
gen_0':s:c1513_16 :: Nat -> 0':s:c15
gen_c8:c9:c1014_16 :: Nat -> c8:c9:c10
gen_c13:c1415_16 :: Nat -> c13:c14
gen_c11:c1216_16 :: Nat -> c11:c12
gen_nil:cons17_16 :: Nat -> nil:cons


Lemmas:
le(gen_0':s:c1513_16(n19_16), gen_0':s:c1513_16(n19_16)) -> true, rt in Omega(0)
LE(gen_0':s:c1513_16(n444_16), gen_0':s:c1513_16(n444_16)) -> gen_c8:c9:c1014_16(n444_16), rt in Omega(1 + n444_16)
PLUS(gen_0':s:c1513_16(n1154_16), gen_0':s:c1513_16(b)) -> gen_c11:c1216_16(n1154_16), rt in Omega(1 + n1154_16)
plus(gen_0':s:c1513_16(n1974_16), gen_0':s:c1513_16(b)) -> gen_0':s:c1513_16(+(n1974_16, b)), rt in Omega(0)


Generator Equations:
gen_0':s:c1513_16(0) <=> 0'
gen_0':s:c1513_16(+(x, 1)) <=> s(gen_0':s:c1513_16(x))
gen_c8:c9:c1014_16(0) <=> c8
gen_c8:c9:c1014_16(+(x, 1)) <=> c10(gen_c8:c9:c1014_16(x))
gen_c13:c1415_16(0) <=> c13
gen_c13:c1415_16(+(x, 1)) <=> c14(c11, gen_c13:c1415_16(x))
gen_c11:c1216_16(0) <=> c11
gen_c11:c1216_16(+(x, 1)) <=> c12(gen_c11:c1216_16(x))
gen_nil:cons17_16(0) <=> nil
gen_nil:cons17_16(+(x, 1)) <=> cons(entry(0', 0', 0'), gen_nil:cons17_16(x))


The following defined symbols remain to be analysed:
times, GEN, IF2, TIMES, gen, if2

They will be analysed ascendingly in the following order:
GEN = IF2
TIMES < IF2
times < TIMES
times < if2
gen = if2

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

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

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

Induction Step:
times(gen_0':s:c1513_16(+(n3369_16, 1)), gen_0':s:c1513_16(b)) ->_R^Omega(0)
plus(gen_0':s:c1513_16(b), times(gen_0':s:c1513_16(n3369_16), gen_0':s:c1513_16(b))) ->_IH
plus(gen_0':s:c1513_16(b), gen_0':s:c1513_16(*(c3370_16, b))) ->_L^Omega(0)
gen_0':s:c1513_16(+(b, *(n3369_16, 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:
TABLE -> c(GEN(s(0')))
GEN(z0) -> c1(IF1(le(z0, 10'), z0), LE(z0, 10'), 10')
IF1(false, z0) -> c2
IF1(true, z0) -> c3(IF2(z0, z0))
IF2(z0, z1) -> c4(IF3(le(z1, 10'), z0, z1), LE(z1, 10'), 10')
IF3(true, z0, z1) -> c5(TIMES(z0, z1))
IF3(true, z0, z1) -> c6(IF2(z0, s(z1)))
IF3(false, z0, z1) -> c7(GEN(s(z0)))
LE(0', z0) -> c8
LE(s(z0), 0') -> c9
LE(s(z0), s(z1)) -> c10(LE(z0, z1))
PLUS(0', z0) -> c11
PLUS(s(z0), z1) -> c12(PLUS(z0, z1))
TIMES(0', z0) -> c13
TIMES(s(z0), z1) -> c14(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
10' -> c15
table -> gen(s(0'))
gen(z0) -> if1(le(z0, 10'), z0)
if1(false, z0) -> nil
if1(true, z0) -> if2(z0, z0)
if2(z0, z1) -> if3(le(z1, 10'), z0, z1)
if3(true, z0, z1) -> cons(entry(z0, z1, times(z0, z1)), if2(z0, s(z1)))
if3(false, z0, z1) -> gen(s(z0))
le(0', z0) -> true
le(s(z0), 0') -> false
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))
10' -> s(s(s(s(s(s(s(s(s(s(0'))))))))))

Types:
TABLE :: c
c :: c1 -> c
GEN :: 0':s:c15 -> c1
s :: 0':s:c15 -> 0':s:c15
0' :: 0':s:c15
c1 :: c2:c3 -> c8:c9:c10 -> 0':s:c15 -> c1
IF1 :: false:true -> 0':s:c15 -> c2:c3
le :: 0':s:c15 -> 0':s:c15 -> false:true
10' :: 0':s:c15
LE :: 0':s:c15 -> 0':s:c15 -> c8:c9:c10
false :: false:true
c2 :: c2:c3
true :: false:true
c3 :: c4 -> c2:c3
IF2 :: 0':s:c15 -> 0':s:c15 -> c4
c4 :: c5:c6:c7 -> c8:c9:c10 -> 0':s:c15 -> c4
IF3 :: false:true -> 0':s:c15 -> 0':s:c15 -> c5:c6:c7
c5 :: c13:c14 -> c5:c6:c7
TIMES :: 0':s:c15 -> 0':s:c15 -> c13:c14
c6 :: c4 -> c5:c6:c7
c7 :: c1 -> c5:c6:c7
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
PLUS :: 0':s:c15 -> 0':s:c15 -> c11:c12
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
c13 :: c13:c14
c14 :: c11:c12 -> c13:c14 -> c13:c14
times :: 0':s:c15 -> 0':s:c15 -> 0':s:c15
c15 :: 0':s:c15
table :: nil:cons
gen :: 0':s:c15 -> nil:cons
if1 :: false:true -> 0':s:c15 -> nil:cons
nil :: nil:cons
if2 :: 0':s:c15 -> 0':s:c15 -> nil:cons
if3 :: false:true -> 0':s:c15 -> 0':s:c15 -> nil:cons
cons :: entry -> nil:cons -> nil:cons
entry :: 0':s:c15 -> 0':s:c15 -> 0':s:c15 -> entry
plus :: 0':s:c15 -> 0':s:c15 -> 0':s:c15
hole_c1_16 :: c
hole_c12_16 :: c1
hole_0':s:c153_16 :: 0':s:c15
hole_c2:c34_16 :: c2:c3
hole_c8:c9:c105_16 :: c8:c9:c10
hole_false:true6_16 :: false:true
hole_c47_16 :: c4
hole_c5:c6:c78_16 :: c5:c6:c7
hole_c13:c149_16 :: c13:c14
hole_c11:c1210_16 :: c11:c12
hole_nil:cons11_16 :: nil:cons
hole_entry12_16 :: entry
gen_0':s:c1513_16 :: Nat -> 0':s:c15
gen_c8:c9:c1014_16 :: Nat -> c8:c9:c10
gen_c13:c1415_16 :: Nat -> c13:c14
gen_c11:c1216_16 :: Nat -> c11:c12
gen_nil:cons17_16 :: Nat -> nil:cons


Lemmas:
le(gen_0':s:c1513_16(n19_16), gen_0':s:c1513_16(n19_16)) -> true, rt in Omega(0)
LE(gen_0':s:c1513_16(n444_16), gen_0':s:c1513_16(n444_16)) -> gen_c8:c9:c1014_16(n444_16), rt in Omega(1 + n444_16)
PLUS(gen_0':s:c1513_16(n1154_16), gen_0':s:c1513_16(b)) -> gen_c11:c1216_16(n1154_16), rt in Omega(1 + n1154_16)
plus(gen_0':s:c1513_16(n1974_16), gen_0':s:c1513_16(b)) -> gen_0':s:c1513_16(+(n1974_16, b)), rt in Omega(0)
times(gen_0':s:c1513_16(n3369_16), gen_0':s:c1513_16(b)) -> gen_0':s:c1513_16(*(n3369_16, b)), rt in Omega(0)


Generator Equations:
gen_0':s:c1513_16(0) <=> 0'
gen_0':s:c1513_16(+(x, 1)) <=> s(gen_0':s:c1513_16(x))
gen_c8:c9:c1014_16(0) <=> c8
gen_c8:c9:c1014_16(+(x, 1)) <=> c10(gen_c8:c9:c1014_16(x))
gen_c13:c1415_16(0) <=> c13
gen_c13:c1415_16(+(x, 1)) <=> c14(c11, gen_c13:c1415_16(x))
gen_c11:c1216_16(0) <=> c11
gen_c11:c1216_16(+(x, 1)) <=> c12(gen_c11:c1216_16(x))
gen_nil:cons17_16(0) <=> nil
gen_nil:cons17_16(+(x, 1)) <=> cons(entry(0', 0', 0'), gen_nil:cons17_16(x))


The following defined symbols remain to be analysed:
TIMES, GEN, IF2, gen, if2

They will be analysed ascendingly in the following order:
GEN = IF2
TIMES < IF2
gen = if2

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
TIMES(gen_0':s:c1513_16(n5253_16), gen_0':s:c1513_16(b)) -> *18_16, rt in Omega(b*n5253_16 + n5253_16)

Induction Base:
TIMES(gen_0':s:c1513_16(0), gen_0':s:c1513_16(b))

Induction Step:
TIMES(gen_0':s:c1513_16(+(n5253_16, 1)), gen_0':s:c1513_16(b)) ->_R^Omega(1)
c14(PLUS(gen_0':s:c1513_16(b), times(gen_0':s:c1513_16(n5253_16), gen_0':s:c1513_16(b))), TIMES(gen_0':s:c1513_16(n5253_16), gen_0':s:c1513_16(b))) ->_L^Omega(0)
c14(PLUS(gen_0':s:c1513_16(b), gen_0':s:c1513_16(*(n5253_16, b))), TIMES(gen_0':s:c1513_16(n5253_16), gen_0':s:c1513_16(b))) ->_L^Omega(1 + b)
c14(gen_c11:c1216_16(b), TIMES(gen_0':s:c1513_16(n5253_16), gen_0':s:c1513_16(*(n5253_16, b)))) ->_IH
c14(gen_c11:c1216_16(*(n5253_16, b)), *18_16)

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:
TABLE -> c(GEN(s(0')))
GEN(z0) -> c1(IF1(le(z0, 10'), z0), LE(z0, 10'), 10')
IF1(false, z0) -> c2
IF1(true, z0) -> c3(IF2(z0, z0))
IF2(z0, z1) -> c4(IF3(le(z1, 10'), z0, z1), LE(z1, 10'), 10')
IF3(true, z0, z1) -> c5(TIMES(z0, z1))
IF3(true, z0, z1) -> c6(IF2(z0, s(z1)))
IF3(false, z0, z1) -> c7(GEN(s(z0)))
LE(0', z0) -> c8
LE(s(z0), 0') -> c9
LE(s(z0), s(z1)) -> c10(LE(z0, z1))
PLUS(0', z0) -> c11
PLUS(s(z0), z1) -> c12(PLUS(z0, z1))
TIMES(0', z0) -> c13
TIMES(s(z0), z1) -> c14(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
10' -> c15
table -> gen(s(0'))
gen(z0) -> if1(le(z0, 10'), z0)
if1(false, z0) -> nil
if1(true, z0) -> if2(z0, z0)
if2(z0, z1) -> if3(le(z1, 10'), z0, z1)
if3(true, z0, z1) -> cons(entry(z0, z1, times(z0, z1)), if2(z0, s(z1)))
if3(false, z0, z1) -> gen(s(z0))
le(0', z0) -> true
le(s(z0), 0') -> false
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))
10' -> s(s(s(s(s(s(s(s(s(s(0'))))))))))

Types:
TABLE :: c
c :: c1 -> c
GEN :: 0':s:c15 -> c1
s :: 0':s:c15 -> 0':s:c15
0' :: 0':s:c15
c1 :: c2:c3 -> c8:c9:c10 -> 0':s:c15 -> c1
IF1 :: false:true -> 0':s:c15 -> c2:c3
le :: 0':s:c15 -> 0':s:c15 -> false:true
10' :: 0':s:c15
LE :: 0':s:c15 -> 0':s:c15 -> c8:c9:c10
false :: false:true
c2 :: c2:c3
true :: false:true
c3 :: c4 -> c2:c3
IF2 :: 0':s:c15 -> 0':s:c15 -> c4
c4 :: c5:c6:c7 -> c8:c9:c10 -> 0':s:c15 -> c4
IF3 :: false:true -> 0':s:c15 -> 0':s:c15 -> c5:c6:c7
c5 :: c13:c14 -> c5:c6:c7
TIMES :: 0':s:c15 -> 0':s:c15 -> c13:c14
c6 :: c4 -> c5:c6:c7
c7 :: c1 -> c5:c6:c7
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
PLUS :: 0':s:c15 -> 0':s:c15 -> c11:c12
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
c13 :: c13:c14
c14 :: c11:c12 -> c13:c14 -> c13:c14
times :: 0':s:c15 -> 0':s:c15 -> 0':s:c15
c15 :: 0':s:c15
table :: nil:cons
gen :: 0':s:c15 -> nil:cons
if1 :: false:true -> 0':s:c15 -> nil:cons
nil :: nil:cons
if2 :: 0':s:c15 -> 0':s:c15 -> nil:cons
if3 :: false:true -> 0':s:c15 -> 0':s:c15 -> nil:cons
cons :: entry -> nil:cons -> nil:cons
entry :: 0':s:c15 -> 0':s:c15 -> 0':s:c15 -> entry
plus :: 0':s:c15 -> 0':s:c15 -> 0':s:c15
hole_c1_16 :: c
hole_c12_16 :: c1
hole_0':s:c153_16 :: 0':s:c15
hole_c2:c34_16 :: c2:c3
hole_c8:c9:c105_16 :: c8:c9:c10
hole_false:true6_16 :: false:true
hole_c47_16 :: c4
hole_c5:c6:c78_16 :: c5:c6:c7
hole_c13:c149_16 :: c13:c14
hole_c11:c1210_16 :: c11:c12
hole_nil:cons11_16 :: nil:cons
hole_entry12_16 :: entry
gen_0':s:c1513_16 :: Nat -> 0':s:c15
gen_c8:c9:c1014_16 :: Nat -> c8:c9:c10
gen_c13:c1415_16 :: Nat -> c13:c14
gen_c11:c1216_16 :: Nat -> c11:c12
gen_nil:cons17_16 :: Nat -> nil:cons


Lemmas:
le(gen_0':s:c1513_16(n19_16), gen_0':s:c1513_16(n19_16)) -> true, rt in Omega(0)
LE(gen_0':s:c1513_16(n444_16), gen_0':s:c1513_16(n444_16)) -> gen_c8:c9:c1014_16(n444_16), rt in Omega(1 + n444_16)
PLUS(gen_0':s:c1513_16(n1154_16), gen_0':s:c1513_16(b)) -> gen_c11:c1216_16(n1154_16), rt in Omega(1 + n1154_16)
plus(gen_0':s:c1513_16(n1974_16), gen_0':s:c1513_16(b)) -> gen_0':s:c1513_16(+(n1974_16, b)), rt in Omega(0)
times(gen_0':s:c1513_16(n3369_16), gen_0':s:c1513_16(b)) -> gen_0':s:c1513_16(*(n3369_16, b)), rt in Omega(0)


Generator Equations:
gen_0':s:c1513_16(0) <=> 0'
gen_0':s:c1513_16(+(x, 1)) <=> s(gen_0':s:c1513_16(x))
gen_c8:c9:c1014_16(0) <=> c8
gen_c8:c9:c1014_16(+(x, 1)) <=> c10(gen_c8:c9:c1014_16(x))
gen_c13:c1415_16(0) <=> c13
gen_c13:c1415_16(+(x, 1)) <=> c14(c11, gen_c13:c1415_16(x))
gen_c11:c1216_16(0) <=> c11
gen_c11:c1216_16(+(x, 1)) <=> c12(gen_c11:c1216_16(x))
gen_nil:cons17_16(0) <=> nil
gen_nil:cons17_16(+(x, 1)) <=> cons(entry(0', 0', 0'), gen_nil:cons17_16(x))


The following defined symbols remain to be analysed:
TIMES, GEN, IF2, gen, if2

They will be analysed ascendingly in the following order:
GEN = IF2
TIMES < IF2
gen = if2

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

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

(29)
BOUNDS(n^2, INF)

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

(30)
Obligation:
Innermost TRS:
Rules:
TABLE -> c(GEN(s(0')))
GEN(z0) -> c1(IF1(le(z0, 10'), z0), LE(z0, 10'), 10')
IF1(false, z0) -> c2
IF1(true, z0) -> c3(IF2(z0, z0))
IF2(z0, z1) -> c4(IF3(le(z1, 10'), z0, z1), LE(z1, 10'), 10')
IF3(true, z0, z1) -> c5(TIMES(z0, z1))
IF3(true, z0, z1) -> c6(IF2(z0, s(z1)))
IF3(false, z0, z1) -> c7(GEN(s(z0)))
LE(0', z0) -> c8
LE(s(z0), 0') -> c9
LE(s(z0), s(z1)) -> c10(LE(z0, z1))
PLUS(0', z0) -> c11
PLUS(s(z0), z1) -> c12(PLUS(z0, z1))
TIMES(0', z0) -> c13
TIMES(s(z0), z1) -> c14(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
10' -> c15
table -> gen(s(0'))
gen(z0) -> if1(le(z0, 10'), z0)
if1(false, z0) -> nil
if1(true, z0) -> if2(z0, z0)
if2(z0, z1) -> if3(le(z1, 10'), z0, z1)
if3(true, z0, z1) -> cons(entry(z0, z1, times(z0, z1)), if2(z0, s(z1)))
if3(false, z0, z1) -> gen(s(z0))
le(0', z0) -> true
le(s(z0), 0') -> false
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))
10' -> s(s(s(s(s(s(s(s(s(s(0'))))))))))

Types:
TABLE :: c
c :: c1 -> c
GEN :: 0':s:c15 -> c1
s :: 0':s:c15 -> 0':s:c15
0' :: 0':s:c15
c1 :: c2:c3 -> c8:c9:c10 -> 0':s:c15 -> c1
IF1 :: false:true -> 0':s:c15 -> c2:c3
le :: 0':s:c15 -> 0':s:c15 -> false:true
10' :: 0':s:c15
LE :: 0':s:c15 -> 0':s:c15 -> c8:c9:c10
false :: false:true
c2 :: c2:c3
true :: false:true
c3 :: c4 -> c2:c3
IF2 :: 0':s:c15 -> 0':s:c15 -> c4
c4 :: c5:c6:c7 -> c8:c9:c10 -> 0':s:c15 -> c4
IF3 :: false:true -> 0':s:c15 -> 0':s:c15 -> c5:c6:c7
c5 :: c13:c14 -> c5:c6:c7
TIMES :: 0':s:c15 -> 0':s:c15 -> c13:c14
c6 :: c4 -> c5:c6:c7
c7 :: c1 -> c5:c6:c7
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
PLUS :: 0':s:c15 -> 0':s:c15 -> c11:c12
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
c13 :: c13:c14
c14 :: c11:c12 -> c13:c14 -> c13:c14
times :: 0':s:c15 -> 0':s:c15 -> 0':s:c15
c15 :: 0':s:c15
table :: nil:cons
gen :: 0':s:c15 -> nil:cons
if1 :: false:true -> 0':s:c15 -> nil:cons
nil :: nil:cons
if2 :: 0':s:c15 -> 0':s:c15 -> nil:cons
if3 :: false:true -> 0':s:c15 -> 0':s:c15 -> nil:cons
cons :: entry -> nil:cons -> nil:cons
entry :: 0':s:c15 -> 0':s:c15 -> 0':s:c15 -> entry
plus :: 0':s:c15 -> 0':s:c15 -> 0':s:c15
hole_c1_16 :: c
hole_c12_16 :: c1
hole_0':s:c153_16 :: 0':s:c15
hole_c2:c34_16 :: c2:c3
hole_c8:c9:c105_16 :: c8:c9:c10
hole_false:true6_16 :: false:true
hole_c47_16 :: c4
hole_c5:c6:c78_16 :: c5:c6:c7
hole_c13:c149_16 :: c13:c14
hole_c11:c1210_16 :: c11:c12
hole_nil:cons11_16 :: nil:cons
hole_entry12_16 :: entry
gen_0':s:c1513_16 :: Nat -> 0':s:c15
gen_c8:c9:c1014_16 :: Nat -> c8:c9:c10
gen_c13:c1415_16 :: Nat -> c13:c14
gen_c11:c1216_16 :: Nat -> c11:c12
gen_nil:cons17_16 :: Nat -> nil:cons


Lemmas:
le(gen_0':s:c1513_16(n19_16), gen_0':s:c1513_16(n19_16)) -> true, rt in Omega(0)
LE(gen_0':s:c1513_16(n444_16), gen_0':s:c1513_16(n444_16)) -> gen_c8:c9:c1014_16(n444_16), rt in Omega(1 + n444_16)
PLUS(gen_0':s:c1513_16(n1154_16), gen_0':s:c1513_16(b)) -> gen_c11:c1216_16(n1154_16), rt in Omega(1 + n1154_16)
plus(gen_0':s:c1513_16(n1974_16), gen_0':s:c1513_16(b)) -> gen_0':s:c1513_16(+(n1974_16, b)), rt in Omega(0)
times(gen_0':s:c1513_16(n3369_16), gen_0':s:c1513_16(b)) -> gen_0':s:c1513_16(*(n3369_16, b)), rt in Omega(0)
TIMES(gen_0':s:c1513_16(n5253_16), gen_0':s:c1513_16(b)) -> *18_16, rt in Omega(b*n5253_16 + n5253_16)


Generator Equations:
gen_0':s:c1513_16(0) <=> 0'
gen_0':s:c1513_16(+(x, 1)) <=> s(gen_0':s:c1513_16(x))
gen_c8:c9:c1014_16(0) <=> c8
gen_c8:c9:c1014_16(+(x, 1)) <=> c10(gen_c8:c9:c1014_16(x))
gen_c13:c1415_16(0) <=> c13
gen_c13:c1415_16(+(x, 1)) <=> c14(c11, gen_c13:c1415_16(x))
gen_c11:c1216_16(0) <=> c11
gen_c11:c1216_16(+(x, 1)) <=> c12(gen_c11:c1216_16(x))
gen_nil:cons17_16(0) <=> nil
gen_nil:cons17_16(+(x, 1)) <=> cons(entry(0', 0', 0'), gen_nil:cons17_16(x))


The following defined symbols remain to be analysed:
if2, GEN, IF2, gen

They will be analysed ascendingly in the following order:
GEN = IF2
gen = if2