WORST_CASE(Omega(n^1),?)
proof of /export/starexec/sandbox/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 2756 ms]
(2) CpxRelTRS
(3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) SlicingProof [LOWER BOUND(ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 6 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 257 ms]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 88 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 107 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 1225 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 87 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 106 ms]
        (26) BOUNDS(1, INF)


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

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


The TRS R consists of the following rules:

   DOUBLE(0) -> c
   DOUBLE(s(z0)) -> c1(DOUBLE(z0))
   DEL(z0, nil) -> c2
   DEL(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
   IF(true, z0, z1, z2) -> c4
   IF(false, z0, z1, z2) -> c5(DEL(z0, z2))
   EQ(0, 0) -> c6
   EQ(0, s(z0)) -> c7
   EQ(s(z0), 0) -> c8
   EQ(s(z0), s(z1)) -> c9(EQ(z0, z1))
   FIRST(nil) -> c10
   FIRST(cons(z0, z1)) -> c11
   DOUBLELIST(nil) -> c12
   DOUBLELIST(cons(z0, z1)) -> c13(DOUBLE(z0))
   DOUBLELIST(cons(z0, z1)) -> c14(DOUBLELIST(del(first(cons(z0, z1)), cons(z0, z1))), DEL(first(cons(z0, z1)), cons(z0, z1)), FIRST(cons(z0, z1)))

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

   double(0) -> 0
   double(s(z0)) -> s(s(double(z0)))
   del(z0, nil) -> nil
   del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
   if(true, z0, z1, z2) -> z2
   if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
   eq(0, 0) -> true
   eq(0, s(z0)) -> false
   eq(s(z0), 0) -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   first(nil) -> 0
   first(cons(z0, z1)) -> z0
   doublelist(nil) -> nil
   doublelist(cons(z0, z1)) -> cons(double(z0), doublelist(del(first(cons(z0, z1)), cons(z0, z1))))

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

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

(2)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   DOUBLE(0) -> c
   DOUBLE(s(z0)) -> c1(DOUBLE(z0))
   DEL(z0, nil) -> c2
   DEL(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
   IF(true, z0, z1, z2) -> c4
   IF(false, z0, z1, z2) -> c5(DEL(z0, z2))
   EQ(0, 0) -> c6
   EQ(0, s(z0)) -> c7
   EQ(s(z0), 0) -> c8
   EQ(s(z0), s(z1)) -> c9(EQ(z0, z1))
   FIRST(nil) -> c10
   FIRST(cons(z0, z1)) -> c11
   DOUBLELIST(nil) -> c12
   DOUBLELIST(cons(z0, z1)) -> c13(DOUBLE(z0))
   DOUBLELIST(cons(z0, z1)) -> c14(DOUBLELIST(del(first(cons(z0, z1)), cons(z0, z1))), DEL(first(cons(z0, z1)), cons(z0, z1)), FIRST(cons(z0, z1)))

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

   double(0) -> 0
   double(s(z0)) -> s(s(double(z0)))
   del(z0, nil) -> nil
   del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
   if(true, z0, z1, z2) -> z2
   if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
   eq(0, 0) -> true
   eq(0, s(z0)) -> false
   eq(s(z0), 0) -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   first(nil) -> 0
   first(cons(z0, z1)) -> z0
   doublelist(nil) -> nil
   doublelist(cons(z0, z1)) -> cons(double(z0), doublelist(del(first(cons(z0, z1)), cons(z0, z1))))

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

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

(4)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   DOUBLE(0') -> c
   DOUBLE(s(z0)) -> c1(DOUBLE(z0))
   DEL(z0, nil) -> c2
   DEL(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), z0, z1, z2), EQ(z0, z1))
   IF(true, z0, z1, z2) -> c4
   IF(false, z0, z1, z2) -> c5(DEL(z0, z2))
   EQ(0', 0') -> c6
   EQ(0', s(z0)) -> c7
   EQ(s(z0), 0') -> c8
   EQ(s(z0), s(z1)) -> c9(EQ(z0, z1))
   FIRST(nil) -> c10
   FIRST(cons(z0, z1)) -> c11
   DOUBLELIST(nil) -> c12
   DOUBLELIST(cons(z0, z1)) -> c13(DOUBLE(z0))
   DOUBLELIST(cons(z0, z1)) -> c14(DOUBLELIST(del(first(cons(z0, z1)), cons(z0, z1))), DEL(first(cons(z0, z1)), cons(z0, z1)), FIRST(cons(z0, z1)))

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

   double(0') -> 0'
   double(s(z0)) -> s(s(double(z0)))
   del(z0, nil) -> nil
   del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
   if(true, z0, z1, z2) -> z2
   if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
   eq(0', 0') -> true
   eq(0', s(z0)) -> false
   eq(s(z0), 0') -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   first(nil) -> 0'
   first(cons(z0, z1)) -> z0
   doublelist(nil) -> nil
   doublelist(cons(z0, z1)) -> cons(double(z0), doublelist(del(first(cons(z0, z1)), cons(z0, z1))))

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

(5) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
IF/2

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

(6)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   DOUBLE(0') -> c
   DOUBLE(s(z0)) -> c1(DOUBLE(z0))
   DEL(z0, nil) -> c2
   DEL(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), z0, z2), EQ(z0, z1))
   IF(true, z0, z2) -> c4
   IF(false, z0, z2) -> c5(DEL(z0, z2))
   EQ(0', 0') -> c6
   EQ(0', s(z0)) -> c7
   EQ(s(z0), 0') -> c8
   EQ(s(z0), s(z1)) -> c9(EQ(z0, z1))
   FIRST(nil) -> c10
   FIRST(cons(z0, z1)) -> c11
   DOUBLELIST(nil) -> c12
   DOUBLELIST(cons(z0, z1)) -> c13(DOUBLE(z0))
   DOUBLELIST(cons(z0, z1)) -> c14(DOUBLELIST(del(first(cons(z0, z1)), cons(z0, z1))), DEL(first(cons(z0, z1)), cons(z0, z1)), FIRST(cons(z0, z1)))

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

   double(0') -> 0'
   double(s(z0)) -> s(s(double(z0)))
   del(z0, nil) -> nil
   del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
   if(true, z0, z1, z2) -> z2
   if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
   eq(0', 0') -> true
   eq(0', s(z0)) -> false
   eq(s(z0), 0') -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   first(nil) -> 0'
   first(cons(z0, z1)) -> z0
   doublelist(nil) -> nil
   doublelist(cons(z0, z1)) -> cons(double(z0), doublelist(del(first(cons(z0, z1)), cons(z0, z1))))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
DOUBLE(0') -> c
DOUBLE(s(z0)) -> c1(DOUBLE(z0))
DEL(z0, nil) -> c2
DEL(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), z0, z2), EQ(z0, z1))
IF(true, z0, z2) -> c4
IF(false, z0, z2) -> c5(DEL(z0, z2))
EQ(0', 0') -> c6
EQ(0', s(z0)) -> c7
EQ(s(z0), 0') -> c8
EQ(s(z0), s(z1)) -> c9(EQ(z0, z1))
FIRST(nil) -> c10
FIRST(cons(z0, z1)) -> c11
DOUBLELIST(nil) -> c12
DOUBLELIST(cons(z0, z1)) -> c13(DOUBLE(z0))
DOUBLELIST(cons(z0, z1)) -> c14(DOUBLELIST(del(first(cons(z0, z1)), cons(z0, z1))), DEL(first(cons(z0, z1)), cons(z0, z1)), FIRST(cons(z0, z1)))
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
first(nil) -> 0'
first(cons(z0, z1)) -> z0
doublelist(nil) -> nil
doublelist(cons(z0, z1)) -> cons(double(z0), doublelist(del(first(cons(z0, z1)), cons(z0, z1))))

Types:
DOUBLE :: 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
DEL :: 0':s -> nil:cons -> c2:c3
nil :: nil:cons
c2 :: c2:c3
cons :: 0':s -> nil:cons -> nil:cons
c3 :: c4:c5 -> c6:c7:c8:c9 -> c2:c3
IF :: true:false -> 0':s -> nil:cons -> c4:c5
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c6:c7:c8:c9
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c2:c3 -> c4:c5
c6 :: c6:c7:c8:c9
c7 :: c6:c7:c8:c9
c8 :: c6:c7:c8:c9
c9 :: c6:c7:c8:c9 -> c6:c7:c8:c9
FIRST :: nil:cons -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
DOUBLELIST :: nil:cons -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c:c1 -> c12:c13:c14
c14 :: c12:c13:c14 -> c2:c3 -> c10:c11 -> c12:c13:c14
del :: 0':s -> nil:cons -> nil:cons
first :: nil:cons -> 0':s
double :: 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
doublelist :: nil:cons -> nil:cons
hole_c:c11_15 :: c:c1
hole_0':s2_15 :: 0':s
hole_c2:c33_15 :: c2:c3
hole_nil:cons4_15 :: nil:cons
hole_c4:c55_15 :: c4:c5
hole_c6:c7:c8:c96_15 :: c6:c7:c8:c9
hole_true:false7_15 :: true:false
hole_c10:c118_15 :: c10:c11
hole_c12:c13:c149_15 :: c12:c13:c14
gen_c:c110_15 :: Nat -> c:c1
gen_0':s11_15 :: Nat -> 0':s
gen_nil:cons12_15 :: Nat -> nil:cons
gen_c6:c7:c8:c913_15 :: Nat -> c6:c7:c8:c9
gen_c12:c13:c1414_15 :: Nat -> c12:c13:c14

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
DOUBLE, DEL, eq, EQ, DOUBLELIST, del, double, doublelist

They will be analysed ascendingly in the following order:
DOUBLE < DOUBLELIST
eq < DEL
EQ < DEL
DEL < DOUBLELIST
eq < del
del < DOUBLELIST
del < doublelist
double < doublelist

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

(10)
Obligation:
Innermost TRS:
Rules:
DOUBLE(0') -> c
DOUBLE(s(z0)) -> c1(DOUBLE(z0))
DEL(z0, nil) -> c2
DEL(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), z0, z2), EQ(z0, z1))
IF(true, z0, z2) -> c4
IF(false, z0, z2) -> c5(DEL(z0, z2))
EQ(0', 0') -> c6
EQ(0', s(z0)) -> c7
EQ(s(z0), 0') -> c8
EQ(s(z0), s(z1)) -> c9(EQ(z0, z1))
FIRST(nil) -> c10
FIRST(cons(z0, z1)) -> c11
DOUBLELIST(nil) -> c12
DOUBLELIST(cons(z0, z1)) -> c13(DOUBLE(z0))
DOUBLELIST(cons(z0, z1)) -> c14(DOUBLELIST(del(first(cons(z0, z1)), cons(z0, z1))), DEL(first(cons(z0, z1)), cons(z0, z1)), FIRST(cons(z0, z1)))
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
first(nil) -> 0'
first(cons(z0, z1)) -> z0
doublelist(nil) -> nil
doublelist(cons(z0, z1)) -> cons(double(z0), doublelist(del(first(cons(z0, z1)), cons(z0, z1))))

Types:
DOUBLE :: 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
DEL :: 0':s -> nil:cons -> c2:c3
nil :: nil:cons
c2 :: c2:c3
cons :: 0':s -> nil:cons -> nil:cons
c3 :: c4:c5 -> c6:c7:c8:c9 -> c2:c3
IF :: true:false -> 0':s -> nil:cons -> c4:c5
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c6:c7:c8:c9
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c2:c3 -> c4:c5
c6 :: c6:c7:c8:c9
c7 :: c6:c7:c8:c9
c8 :: c6:c7:c8:c9
c9 :: c6:c7:c8:c9 -> c6:c7:c8:c9
FIRST :: nil:cons -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
DOUBLELIST :: nil:cons -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c:c1 -> c12:c13:c14
c14 :: c12:c13:c14 -> c2:c3 -> c10:c11 -> c12:c13:c14
del :: 0':s -> nil:cons -> nil:cons
first :: nil:cons -> 0':s
double :: 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
doublelist :: nil:cons -> nil:cons
hole_c:c11_15 :: c:c1
hole_0':s2_15 :: 0':s
hole_c2:c33_15 :: c2:c3
hole_nil:cons4_15 :: nil:cons
hole_c4:c55_15 :: c4:c5
hole_c6:c7:c8:c96_15 :: c6:c7:c8:c9
hole_true:false7_15 :: true:false
hole_c10:c118_15 :: c10:c11
hole_c12:c13:c149_15 :: c12:c13:c14
gen_c:c110_15 :: Nat -> c:c1
gen_0':s11_15 :: Nat -> 0':s
gen_nil:cons12_15 :: Nat -> nil:cons
gen_c6:c7:c8:c913_15 :: Nat -> c6:c7:c8:c9
gen_c12:c13:c1414_15 :: Nat -> c12:c13:c14


Generator Equations:
gen_c:c110_15(0) <=> c
gen_c:c110_15(+(x, 1)) <=> c1(gen_c:c110_15(x))
gen_0':s11_15(0) <=> 0'
gen_0':s11_15(+(x, 1)) <=> s(gen_0':s11_15(x))
gen_nil:cons12_15(0) <=> nil
gen_nil:cons12_15(+(x, 1)) <=> cons(0', gen_nil:cons12_15(x))
gen_c6:c7:c8:c913_15(0) <=> c6
gen_c6:c7:c8:c913_15(+(x, 1)) <=> c9(gen_c6:c7:c8:c913_15(x))
gen_c12:c13:c1414_15(0) <=> c12
gen_c12:c13:c1414_15(+(x, 1)) <=> c14(gen_c12:c13:c1414_15(x), c2, c10)


The following defined symbols remain to be analysed:
DOUBLE, DEL, eq, EQ, DOUBLELIST, del, double, doublelist

They will be analysed ascendingly in the following order:
DOUBLE < DOUBLELIST
eq < DEL
EQ < DEL
DEL < DOUBLELIST
eq < del
del < DOUBLELIST
del < doublelist
double < doublelist

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
DOUBLE(gen_0':s11_15(n16_15)) -> gen_c:c110_15(n16_15), rt in Omega(1 + n16_15)

Induction Base:
DOUBLE(gen_0':s11_15(0)) ->_R^Omega(1)
c

Induction Step:
DOUBLE(gen_0':s11_15(+(n16_15, 1))) ->_R^Omega(1)
c1(DOUBLE(gen_0':s11_15(n16_15))) ->_IH
c1(gen_c:c110_15(c17_15))

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

(12)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
DOUBLE(0') -> c
DOUBLE(s(z0)) -> c1(DOUBLE(z0))
DEL(z0, nil) -> c2
DEL(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), z0, z2), EQ(z0, z1))
IF(true, z0, z2) -> c4
IF(false, z0, z2) -> c5(DEL(z0, z2))
EQ(0', 0') -> c6
EQ(0', s(z0)) -> c7
EQ(s(z0), 0') -> c8
EQ(s(z0), s(z1)) -> c9(EQ(z0, z1))
FIRST(nil) -> c10
FIRST(cons(z0, z1)) -> c11
DOUBLELIST(nil) -> c12
DOUBLELIST(cons(z0, z1)) -> c13(DOUBLE(z0))
DOUBLELIST(cons(z0, z1)) -> c14(DOUBLELIST(del(first(cons(z0, z1)), cons(z0, z1))), DEL(first(cons(z0, z1)), cons(z0, z1)), FIRST(cons(z0, z1)))
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
first(nil) -> 0'
first(cons(z0, z1)) -> z0
doublelist(nil) -> nil
doublelist(cons(z0, z1)) -> cons(double(z0), doublelist(del(first(cons(z0, z1)), cons(z0, z1))))

Types:
DOUBLE :: 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
DEL :: 0':s -> nil:cons -> c2:c3
nil :: nil:cons
c2 :: c2:c3
cons :: 0':s -> nil:cons -> nil:cons
c3 :: c4:c5 -> c6:c7:c8:c9 -> c2:c3
IF :: true:false -> 0':s -> nil:cons -> c4:c5
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c6:c7:c8:c9
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c2:c3 -> c4:c5
c6 :: c6:c7:c8:c9
c7 :: c6:c7:c8:c9
c8 :: c6:c7:c8:c9
c9 :: c6:c7:c8:c9 -> c6:c7:c8:c9
FIRST :: nil:cons -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
DOUBLELIST :: nil:cons -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c:c1 -> c12:c13:c14
c14 :: c12:c13:c14 -> c2:c3 -> c10:c11 -> c12:c13:c14
del :: 0':s -> nil:cons -> nil:cons
first :: nil:cons -> 0':s
double :: 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
doublelist :: nil:cons -> nil:cons
hole_c:c11_15 :: c:c1
hole_0':s2_15 :: 0':s
hole_c2:c33_15 :: c2:c3
hole_nil:cons4_15 :: nil:cons
hole_c4:c55_15 :: c4:c5
hole_c6:c7:c8:c96_15 :: c6:c7:c8:c9
hole_true:false7_15 :: true:false
hole_c10:c118_15 :: c10:c11
hole_c12:c13:c149_15 :: c12:c13:c14
gen_c:c110_15 :: Nat -> c:c1
gen_0':s11_15 :: Nat -> 0':s
gen_nil:cons12_15 :: Nat -> nil:cons
gen_c6:c7:c8:c913_15 :: Nat -> c6:c7:c8:c9
gen_c12:c13:c1414_15 :: Nat -> c12:c13:c14


Generator Equations:
gen_c:c110_15(0) <=> c
gen_c:c110_15(+(x, 1)) <=> c1(gen_c:c110_15(x))
gen_0':s11_15(0) <=> 0'
gen_0':s11_15(+(x, 1)) <=> s(gen_0':s11_15(x))
gen_nil:cons12_15(0) <=> nil
gen_nil:cons12_15(+(x, 1)) <=> cons(0', gen_nil:cons12_15(x))
gen_c6:c7:c8:c913_15(0) <=> c6
gen_c6:c7:c8:c913_15(+(x, 1)) <=> c9(gen_c6:c7:c8:c913_15(x))
gen_c12:c13:c1414_15(0) <=> c12
gen_c12:c13:c1414_15(+(x, 1)) <=> c14(gen_c12:c13:c1414_15(x), c2, c10)


The following defined symbols remain to be analysed:
DOUBLE, DEL, eq, EQ, DOUBLELIST, del, double, doublelist

They will be analysed ascendingly in the following order:
DOUBLE < DOUBLELIST
eq < DEL
EQ < DEL
DEL < DOUBLELIST
eq < del
del < DOUBLELIST
del < doublelist
double < doublelist

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
DOUBLE(0') -> c
DOUBLE(s(z0)) -> c1(DOUBLE(z0))
DEL(z0, nil) -> c2
DEL(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), z0, z2), EQ(z0, z1))
IF(true, z0, z2) -> c4
IF(false, z0, z2) -> c5(DEL(z0, z2))
EQ(0', 0') -> c6
EQ(0', s(z0)) -> c7
EQ(s(z0), 0') -> c8
EQ(s(z0), s(z1)) -> c9(EQ(z0, z1))
FIRST(nil) -> c10
FIRST(cons(z0, z1)) -> c11
DOUBLELIST(nil) -> c12
DOUBLELIST(cons(z0, z1)) -> c13(DOUBLE(z0))
DOUBLELIST(cons(z0, z1)) -> c14(DOUBLELIST(del(first(cons(z0, z1)), cons(z0, z1))), DEL(first(cons(z0, z1)), cons(z0, z1)), FIRST(cons(z0, z1)))
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
first(nil) -> 0'
first(cons(z0, z1)) -> z0
doublelist(nil) -> nil
doublelist(cons(z0, z1)) -> cons(double(z0), doublelist(del(first(cons(z0, z1)), cons(z0, z1))))

Types:
DOUBLE :: 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
DEL :: 0':s -> nil:cons -> c2:c3
nil :: nil:cons
c2 :: c2:c3
cons :: 0':s -> nil:cons -> nil:cons
c3 :: c4:c5 -> c6:c7:c8:c9 -> c2:c3
IF :: true:false -> 0':s -> nil:cons -> c4:c5
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c6:c7:c8:c9
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c2:c3 -> c4:c5
c6 :: c6:c7:c8:c9
c7 :: c6:c7:c8:c9
c8 :: c6:c7:c8:c9
c9 :: c6:c7:c8:c9 -> c6:c7:c8:c9
FIRST :: nil:cons -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
DOUBLELIST :: nil:cons -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c:c1 -> c12:c13:c14
c14 :: c12:c13:c14 -> c2:c3 -> c10:c11 -> c12:c13:c14
del :: 0':s -> nil:cons -> nil:cons
first :: nil:cons -> 0':s
double :: 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
doublelist :: nil:cons -> nil:cons
hole_c:c11_15 :: c:c1
hole_0':s2_15 :: 0':s
hole_c2:c33_15 :: c2:c3
hole_nil:cons4_15 :: nil:cons
hole_c4:c55_15 :: c4:c5
hole_c6:c7:c8:c96_15 :: c6:c7:c8:c9
hole_true:false7_15 :: true:false
hole_c10:c118_15 :: c10:c11
hole_c12:c13:c149_15 :: c12:c13:c14
gen_c:c110_15 :: Nat -> c:c1
gen_0':s11_15 :: Nat -> 0':s
gen_nil:cons12_15 :: Nat -> nil:cons
gen_c6:c7:c8:c913_15 :: Nat -> c6:c7:c8:c9
gen_c12:c13:c1414_15 :: Nat -> c12:c13:c14


Lemmas:
DOUBLE(gen_0':s11_15(n16_15)) -> gen_c:c110_15(n16_15), rt in Omega(1 + n16_15)


Generator Equations:
gen_c:c110_15(0) <=> c
gen_c:c110_15(+(x, 1)) <=> c1(gen_c:c110_15(x))
gen_0':s11_15(0) <=> 0'
gen_0':s11_15(+(x, 1)) <=> s(gen_0':s11_15(x))
gen_nil:cons12_15(0) <=> nil
gen_nil:cons12_15(+(x, 1)) <=> cons(0', gen_nil:cons12_15(x))
gen_c6:c7:c8:c913_15(0) <=> c6
gen_c6:c7:c8:c913_15(+(x, 1)) <=> c9(gen_c6:c7:c8:c913_15(x))
gen_c12:c13:c1414_15(0) <=> c12
gen_c12:c13:c1414_15(+(x, 1)) <=> c14(gen_c12:c13:c1414_15(x), c2, c10)


The following defined symbols remain to be analysed:
eq, DEL, EQ, DOUBLELIST, del, double, doublelist

They will be analysed ascendingly in the following order:
eq < DEL
EQ < DEL
DEL < DOUBLELIST
eq < del
del < DOUBLELIST
del < doublelist
double < doublelist

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
eq(gen_0':s11_15(n324_15), gen_0':s11_15(n324_15)) -> true, rt in Omega(0)

Induction Base:
eq(gen_0':s11_15(0), gen_0':s11_15(0)) ->_R^Omega(0)
true

Induction Step:
eq(gen_0':s11_15(+(n324_15, 1)), gen_0':s11_15(+(n324_15, 1))) ->_R^Omega(0)
eq(gen_0':s11_15(n324_15), gen_0':s11_15(n324_15)) ->_IH
true

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

(18)
Obligation:
Innermost TRS:
Rules:
DOUBLE(0') -> c
DOUBLE(s(z0)) -> c1(DOUBLE(z0))
DEL(z0, nil) -> c2
DEL(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), z0, z2), EQ(z0, z1))
IF(true, z0, z2) -> c4
IF(false, z0, z2) -> c5(DEL(z0, z2))
EQ(0', 0') -> c6
EQ(0', s(z0)) -> c7
EQ(s(z0), 0') -> c8
EQ(s(z0), s(z1)) -> c9(EQ(z0, z1))
FIRST(nil) -> c10
FIRST(cons(z0, z1)) -> c11
DOUBLELIST(nil) -> c12
DOUBLELIST(cons(z0, z1)) -> c13(DOUBLE(z0))
DOUBLELIST(cons(z0, z1)) -> c14(DOUBLELIST(del(first(cons(z0, z1)), cons(z0, z1))), DEL(first(cons(z0, z1)), cons(z0, z1)), FIRST(cons(z0, z1)))
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
first(nil) -> 0'
first(cons(z0, z1)) -> z0
doublelist(nil) -> nil
doublelist(cons(z0, z1)) -> cons(double(z0), doublelist(del(first(cons(z0, z1)), cons(z0, z1))))

Types:
DOUBLE :: 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
DEL :: 0':s -> nil:cons -> c2:c3
nil :: nil:cons
c2 :: c2:c3
cons :: 0':s -> nil:cons -> nil:cons
c3 :: c4:c5 -> c6:c7:c8:c9 -> c2:c3
IF :: true:false -> 0':s -> nil:cons -> c4:c5
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c6:c7:c8:c9
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c2:c3 -> c4:c5
c6 :: c6:c7:c8:c9
c7 :: c6:c7:c8:c9
c8 :: c6:c7:c8:c9
c9 :: c6:c7:c8:c9 -> c6:c7:c8:c9
FIRST :: nil:cons -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
DOUBLELIST :: nil:cons -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c:c1 -> c12:c13:c14
c14 :: c12:c13:c14 -> c2:c3 -> c10:c11 -> c12:c13:c14
del :: 0':s -> nil:cons -> nil:cons
first :: nil:cons -> 0':s
double :: 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
doublelist :: nil:cons -> nil:cons
hole_c:c11_15 :: c:c1
hole_0':s2_15 :: 0':s
hole_c2:c33_15 :: c2:c3
hole_nil:cons4_15 :: nil:cons
hole_c4:c55_15 :: c4:c5
hole_c6:c7:c8:c96_15 :: c6:c7:c8:c9
hole_true:false7_15 :: true:false
hole_c10:c118_15 :: c10:c11
hole_c12:c13:c149_15 :: c12:c13:c14
gen_c:c110_15 :: Nat -> c:c1
gen_0':s11_15 :: Nat -> 0':s
gen_nil:cons12_15 :: Nat -> nil:cons
gen_c6:c7:c8:c913_15 :: Nat -> c6:c7:c8:c9
gen_c12:c13:c1414_15 :: Nat -> c12:c13:c14


Lemmas:
DOUBLE(gen_0':s11_15(n16_15)) -> gen_c:c110_15(n16_15), rt in Omega(1 + n16_15)
eq(gen_0':s11_15(n324_15), gen_0':s11_15(n324_15)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c110_15(0) <=> c
gen_c:c110_15(+(x, 1)) <=> c1(gen_c:c110_15(x))
gen_0':s11_15(0) <=> 0'
gen_0':s11_15(+(x, 1)) <=> s(gen_0':s11_15(x))
gen_nil:cons12_15(0) <=> nil
gen_nil:cons12_15(+(x, 1)) <=> cons(0', gen_nil:cons12_15(x))
gen_c6:c7:c8:c913_15(0) <=> c6
gen_c6:c7:c8:c913_15(+(x, 1)) <=> c9(gen_c6:c7:c8:c913_15(x))
gen_c12:c13:c1414_15(0) <=> c12
gen_c12:c13:c1414_15(+(x, 1)) <=> c14(gen_c12:c13:c1414_15(x), c2, c10)


The following defined symbols remain to be analysed:
EQ, DEL, DOUBLELIST, del, double, doublelist

They will be analysed ascendingly in the following order:
EQ < DEL
DEL < DOUBLELIST
del < DOUBLELIST
del < doublelist
double < doublelist

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
EQ(gen_0':s11_15(n943_15), gen_0':s11_15(n943_15)) -> gen_c6:c7:c8:c913_15(n943_15), rt in Omega(1 + n943_15)

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

Induction Step:
EQ(gen_0':s11_15(+(n943_15, 1)), gen_0':s11_15(+(n943_15, 1))) ->_R^Omega(1)
c9(EQ(gen_0':s11_15(n943_15), gen_0':s11_15(n943_15))) ->_IH
c9(gen_c6:c7:c8:c913_15(c944_15))

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:
DOUBLE(0') -> c
DOUBLE(s(z0)) -> c1(DOUBLE(z0))
DEL(z0, nil) -> c2
DEL(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), z0, z2), EQ(z0, z1))
IF(true, z0, z2) -> c4
IF(false, z0, z2) -> c5(DEL(z0, z2))
EQ(0', 0') -> c6
EQ(0', s(z0)) -> c7
EQ(s(z0), 0') -> c8
EQ(s(z0), s(z1)) -> c9(EQ(z0, z1))
FIRST(nil) -> c10
FIRST(cons(z0, z1)) -> c11
DOUBLELIST(nil) -> c12
DOUBLELIST(cons(z0, z1)) -> c13(DOUBLE(z0))
DOUBLELIST(cons(z0, z1)) -> c14(DOUBLELIST(del(first(cons(z0, z1)), cons(z0, z1))), DEL(first(cons(z0, z1)), cons(z0, z1)), FIRST(cons(z0, z1)))
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
first(nil) -> 0'
first(cons(z0, z1)) -> z0
doublelist(nil) -> nil
doublelist(cons(z0, z1)) -> cons(double(z0), doublelist(del(first(cons(z0, z1)), cons(z0, z1))))

Types:
DOUBLE :: 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
DEL :: 0':s -> nil:cons -> c2:c3
nil :: nil:cons
c2 :: c2:c3
cons :: 0':s -> nil:cons -> nil:cons
c3 :: c4:c5 -> c6:c7:c8:c9 -> c2:c3
IF :: true:false -> 0':s -> nil:cons -> c4:c5
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c6:c7:c8:c9
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c2:c3 -> c4:c5
c6 :: c6:c7:c8:c9
c7 :: c6:c7:c8:c9
c8 :: c6:c7:c8:c9
c9 :: c6:c7:c8:c9 -> c6:c7:c8:c9
FIRST :: nil:cons -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
DOUBLELIST :: nil:cons -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c:c1 -> c12:c13:c14
c14 :: c12:c13:c14 -> c2:c3 -> c10:c11 -> c12:c13:c14
del :: 0':s -> nil:cons -> nil:cons
first :: nil:cons -> 0':s
double :: 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
doublelist :: nil:cons -> nil:cons
hole_c:c11_15 :: c:c1
hole_0':s2_15 :: 0':s
hole_c2:c33_15 :: c2:c3
hole_nil:cons4_15 :: nil:cons
hole_c4:c55_15 :: c4:c5
hole_c6:c7:c8:c96_15 :: c6:c7:c8:c9
hole_true:false7_15 :: true:false
hole_c10:c118_15 :: c10:c11
hole_c12:c13:c149_15 :: c12:c13:c14
gen_c:c110_15 :: Nat -> c:c1
gen_0':s11_15 :: Nat -> 0':s
gen_nil:cons12_15 :: Nat -> nil:cons
gen_c6:c7:c8:c913_15 :: Nat -> c6:c7:c8:c9
gen_c12:c13:c1414_15 :: Nat -> c12:c13:c14


Lemmas:
DOUBLE(gen_0':s11_15(n16_15)) -> gen_c:c110_15(n16_15), rt in Omega(1 + n16_15)
eq(gen_0':s11_15(n324_15), gen_0':s11_15(n324_15)) -> true, rt in Omega(0)
EQ(gen_0':s11_15(n943_15), gen_0':s11_15(n943_15)) -> gen_c6:c7:c8:c913_15(n943_15), rt in Omega(1 + n943_15)


Generator Equations:
gen_c:c110_15(0) <=> c
gen_c:c110_15(+(x, 1)) <=> c1(gen_c:c110_15(x))
gen_0':s11_15(0) <=> 0'
gen_0':s11_15(+(x, 1)) <=> s(gen_0':s11_15(x))
gen_nil:cons12_15(0) <=> nil
gen_nil:cons12_15(+(x, 1)) <=> cons(0', gen_nil:cons12_15(x))
gen_c6:c7:c8:c913_15(0) <=> c6
gen_c6:c7:c8:c913_15(+(x, 1)) <=> c9(gen_c6:c7:c8:c913_15(x))
gen_c12:c13:c1414_15(0) <=> c12
gen_c12:c13:c1414_15(+(x, 1)) <=> c14(gen_c12:c13:c1414_15(x), c2, c10)


The following defined symbols remain to be analysed:
DEL, DOUBLELIST, del, double, doublelist

They will be analysed ascendingly in the following order:
DEL < DOUBLELIST
del < DOUBLELIST
del < doublelist
double < doublelist

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
DOUBLELIST(gen_nil:cons12_15(n2806_15)) -> *15_15, rt in Omega(n2806_15)

Induction Base:
DOUBLELIST(gen_nil:cons12_15(0))

Induction Step:
DOUBLELIST(gen_nil:cons12_15(+(n2806_15, 1))) ->_R^Omega(1)
c14(DOUBLELIST(del(first(cons(0', gen_nil:cons12_15(n2806_15))), cons(0', gen_nil:cons12_15(n2806_15)))), DEL(first(cons(0', gen_nil:cons12_15(n2806_15))), cons(0', gen_nil:cons12_15(n2806_15))), FIRST(cons(0', gen_nil:cons12_15(n2806_15)))) ->_R^Omega(0)
c14(DOUBLELIST(del(0', cons(0', gen_nil:cons12_15(n2806_15)))), DEL(first(cons(0', gen_nil:cons12_15(n2806_15))), cons(0', gen_nil:cons12_15(n2806_15))), FIRST(cons(0', gen_nil:cons12_15(n2806_15)))) ->_R^Omega(0)
c14(DOUBLELIST(if(eq(0', 0'), 0', 0', gen_nil:cons12_15(n2806_15))), DEL(first(cons(0', gen_nil:cons12_15(n2806_15))), cons(0', gen_nil:cons12_15(n2806_15))), FIRST(cons(0', gen_nil:cons12_15(n2806_15)))) ->_L^Omega(0)
c14(DOUBLELIST(if(true, 0', 0', gen_nil:cons12_15(n2806_15))), DEL(first(cons(0', gen_nil:cons12_15(n2806_15))), cons(0', gen_nil:cons12_15(n2806_15))), FIRST(cons(0', gen_nil:cons12_15(n2806_15)))) ->_R^Omega(0)
c14(DOUBLELIST(gen_nil:cons12_15(n2806_15)), DEL(first(cons(0', gen_nil:cons12_15(n2806_15))), cons(0', gen_nil:cons12_15(n2806_15))), FIRST(cons(0', gen_nil:cons12_15(n2806_15)))) ->_IH
c14(*15_15, DEL(first(cons(0', gen_nil:cons12_15(n2806_15))), cons(0', gen_nil:cons12_15(n2806_15))), FIRST(cons(0', gen_nil:cons12_15(n2806_15)))) ->_R^Omega(0)
c14(*15_15, DEL(0', cons(0', gen_nil:cons12_15(n2806_15))), FIRST(cons(0', gen_nil:cons12_15(n2806_15)))) ->_R^Omega(1)
c14(*15_15, c3(IF(eq(0', 0'), 0', gen_nil:cons12_15(n2806_15)), EQ(0', 0')), FIRST(cons(0', gen_nil:cons12_15(n2806_15)))) ->_L^Omega(0)
c14(*15_15, c3(IF(true, 0', gen_nil:cons12_15(n2806_15)), EQ(0', 0')), FIRST(cons(0', gen_nil:cons12_15(n2806_15)))) ->_R^Omega(1)
c14(*15_15, c3(c4, EQ(0', 0')), FIRST(cons(0', gen_nil:cons12_15(n2806_15)))) ->_L^Omega(1)
c14(*15_15, c3(c4, gen_c6:c7:c8:c913_15(0)), FIRST(cons(0', gen_nil:cons12_15(n2806_15)))) ->_R^Omega(1)
c14(*15_15, c3(c4, gen_c6:c7:c8:c913_15(0)), c11)

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:
DOUBLE(0') -> c
DOUBLE(s(z0)) -> c1(DOUBLE(z0))
DEL(z0, nil) -> c2
DEL(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), z0, z2), EQ(z0, z1))
IF(true, z0, z2) -> c4
IF(false, z0, z2) -> c5(DEL(z0, z2))
EQ(0', 0') -> c6
EQ(0', s(z0)) -> c7
EQ(s(z0), 0') -> c8
EQ(s(z0), s(z1)) -> c9(EQ(z0, z1))
FIRST(nil) -> c10
FIRST(cons(z0, z1)) -> c11
DOUBLELIST(nil) -> c12
DOUBLELIST(cons(z0, z1)) -> c13(DOUBLE(z0))
DOUBLELIST(cons(z0, z1)) -> c14(DOUBLELIST(del(first(cons(z0, z1)), cons(z0, z1))), DEL(first(cons(z0, z1)), cons(z0, z1)), FIRST(cons(z0, z1)))
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
first(nil) -> 0'
first(cons(z0, z1)) -> z0
doublelist(nil) -> nil
doublelist(cons(z0, z1)) -> cons(double(z0), doublelist(del(first(cons(z0, z1)), cons(z0, z1))))

Types:
DOUBLE :: 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
DEL :: 0':s -> nil:cons -> c2:c3
nil :: nil:cons
c2 :: c2:c3
cons :: 0':s -> nil:cons -> nil:cons
c3 :: c4:c5 -> c6:c7:c8:c9 -> c2:c3
IF :: true:false -> 0':s -> nil:cons -> c4:c5
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c6:c7:c8:c9
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c2:c3 -> c4:c5
c6 :: c6:c7:c8:c9
c7 :: c6:c7:c8:c9
c8 :: c6:c7:c8:c9
c9 :: c6:c7:c8:c9 -> c6:c7:c8:c9
FIRST :: nil:cons -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
DOUBLELIST :: nil:cons -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c:c1 -> c12:c13:c14
c14 :: c12:c13:c14 -> c2:c3 -> c10:c11 -> c12:c13:c14
del :: 0':s -> nil:cons -> nil:cons
first :: nil:cons -> 0':s
double :: 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
doublelist :: nil:cons -> nil:cons
hole_c:c11_15 :: c:c1
hole_0':s2_15 :: 0':s
hole_c2:c33_15 :: c2:c3
hole_nil:cons4_15 :: nil:cons
hole_c4:c55_15 :: c4:c5
hole_c6:c7:c8:c96_15 :: c6:c7:c8:c9
hole_true:false7_15 :: true:false
hole_c10:c118_15 :: c10:c11
hole_c12:c13:c149_15 :: c12:c13:c14
gen_c:c110_15 :: Nat -> c:c1
gen_0':s11_15 :: Nat -> 0':s
gen_nil:cons12_15 :: Nat -> nil:cons
gen_c6:c7:c8:c913_15 :: Nat -> c6:c7:c8:c9
gen_c12:c13:c1414_15 :: Nat -> c12:c13:c14


Lemmas:
DOUBLE(gen_0':s11_15(n16_15)) -> gen_c:c110_15(n16_15), rt in Omega(1 + n16_15)
eq(gen_0':s11_15(n324_15), gen_0':s11_15(n324_15)) -> true, rt in Omega(0)
EQ(gen_0':s11_15(n943_15), gen_0':s11_15(n943_15)) -> gen_c6:c7:c8:c913_15(n943_15), rt in Omega(1 + n943_15)
DOUBLELIST(gen_nil:cons12_15(n2806_15)) -> *15_15, rt in Omega(n2806_15)


Generator Equations:
gen_c:c110_15(0) <=> c
gen_c:c110_15(+(x, 1)) <=> c1(gen_c:c110_15(x))
gen_0':s11_15(0) <=> 0'
gen_0':s11_15(+(x, 1)) <=> s(gen_0':s11_15(x))
gen_nil:cons12_15(0) <=> nil
gen_nil:cons12_15(+(x, 1)) <=> cons(0', gen_nil:cons12_15(x))
gen_c6:c7:c8:c913_15(0) <=> c6
gen_c6:c7:c8:c913_15(+(x, 1)) <=> c9(gen_c6:c7:c8:c913_15(x))
gen_c12:c13:c1414_15(0) <=> c12
gen_c12:c13:c1414_15(+(x, 1)) <=> c14(gen_c12:c13:c1414_15(x), c2, c10)


The following defined symbols remain to be analysed:
double, doublelist

They will be analysed ascendingly in the following order:
double < doublelist

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

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

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

Induction Step:
double(gen_0':s11_15(+(n8692_15, 1))) ->_R^Omega(0)
s(s(double(gen_0':s11_15(n8692_15)))) ->_IH
s(s(gen_0':s11_15(*(2, c8693_15))))

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:
DOUBLE(0') -> c
DOUBLE(s(z0)) -> c1(DOUBLE(z0))
DEL(z0, nil) -> c2
DEL(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), z0, z2), EQ(z0, z1))
IF(true, z0, z2) -> c4
IF(false, z0, z2) -> c5(DEL(z0, z2))
EQ(0', 0') -> c6
EQ(0', s(z0)) -> c7
EQ(s(z0), 0') -> c8
EQ(s(z0), s(z1)) -> c9(EQ(z0, z1))
FIRST(nil) -> c10
FIRST(cons(z0, z1)) -> c11
DOUBLELIST(nil) -> c12
DOUBLELIST(cons(z0, z1)) -> c13(DOUBLE(z0))
DOUBLELIST(cons(z0, z1)) -> c14(DOUBLELIST(del(first(cons(z0, z1)), cons(z0, z1))), DEL(first(cons(z0, z1)), cons(z0, z1)), FIRST(cons(z0, z1)))
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
del(z0, nil) -> nil
del(z0, cons(z1, z2)) -> if(eq(z0, z1), z0, z1, z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> cons(z1, del(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
first(nil) -> 0'
first(cons(z0, z1)) -> z0
doublelist(nil) -> nil
doublelist(cons(z0, z1)) -> cons(double(z0), doublelist(del(first(cons(z0, z1)), cons(z0, z1))))

Types:
DOUBLE :: 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
DEL :: 0':s -> nil:cons -> c2:c3
nil :: nil:cons
c2 :: c2:c3
cons :: 0':s -> nil:cons -> nil:cons
c3 :: c4:c5 -> c6:c7:c8:c9 -> c2:c3
IF :: true:false -> 0':s -> nil:cons -> c4:c5
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c6:c7:c8:c9
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c2:c3 -> c4:c5
c6 :: c6:c7:c8:c9
c7 :: c6:c7:c8:c9
c8 :: c6:c7:c8:c9
c9 :: c6:c7:c8:c9 -> c6:c7:c8:c9
FIRST :: nil:cons -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
DOUBLELIST :: nil:cons -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c:c1 -> c12:c13:c14
c14 :: c12:c13:c14 -> c2:c3 -> c10:c11 -> c12:c13:c14
del :: 0':s -> nil:cons -> nil:cons
first :: nil:cons -> 0':s
double :: 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons
doublelist :: nil:cons -> nil:cons
hole_c:c11_15 :: c:c1
hole_0':s2_15 :: 0':s
hole_c2:c33_15 :: c2:c3
hole_nil:cons4_15 :: nil:cons
hole_c4:c55_15 :: c4:c5
hole_c6:c7:c8:c96_15 :: c6:c7:c8:c9
hole_true:false7_15 :: true:false
hole_c10:c118_15 :: c10:c11
hole_c12:c13:c149_15 :: c12:c13:c14
gen_c:c110_15 :: Nat -> c:c1
gen_0':s11_15 :: Nat -> 0':s
gen_nil:cons12_15 :: Nat -> nil:cons
gen_c6:c7:c8:c913_15 :: Nat -> c6:c7:c8:c9
gen_c12:c13:c1414_15 :: Nat -> c12:c13:c14


Lemmas:
DOUBLE(gen_0':s11_15(n16_15)) -> gen_c:c110_15(n16_15), rt in Omega(1 + n16_15)
eq(gen_0':s11_15(n324_15), gen_0':s11_15(n324_15)) -> true, rt in Omega(0)
EQ(gen_0':s11_15(n943_15), gen_0':s11_15(n943_15)) -> gen_c6:c7:c8:c913_15(n943_15), rt in Omega(1 + n943_15)
DOUBLELIST(gen_nil:cons12_15(n2806_15)) -> *15_15, rt in Omega(n2806_15)
double(gen_0':s11_15(n8692_15)) -> gen_0':s11_15(*(2, n8692_15)), rt in Omega(0)


Generator Equations:
gen_c:c110_15(0) <=> c
gen_c:c110_15(+(x, 1)) <=> c1(gen_c:c110_15(x))
gen_0':s11_15(0) <=> 0'
gen_0':s11_15(+(x, 1)) <=> s(gen_0':s11_15(x))
gen_nil:cons12_15(0) <=> nil
gen_nil:cons12_15(+(x, 1)) <=> cons(0', gen_nil:cons12_15(x))
gen_c6:c7:c8:c913_15(0) <=> c6
gen_c6:c7:c8:c913_15(+(x, 1)) <=> c9(gen_c6:c7:c8:c913_15(x))
gen_c12:c13:c1414_15(0) <=> c12
gen_c12:c13:c1414_15(+(x, 1)) <=> c14(gen_c12:c13:c1414_15(x), c2, c10)


The following defined symbols remain to be analysed:
doublelist
----------------------------------------

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
doublelist(gen_nil:cons12_15(n9192_15)) -> gen_nil:cons12_15(n9192_15), rt in Omega(0)

Induction Base:
doublelist(gen_nil:cons12_15(0)) ->_R^Omega(0)
nil

Induction Step:
doublelist(gen_nil:cons12_15(+(n9192_15, 1))) ->_R^Omega(0)
cons(double(0'), doublelist(del(first(cons(0', gen_nil:cons12_15(n9192_15))), cons(0', gen_nil:cons12_15(n9192_15))))) ->_L^Omega(0)
cons(gen_0':s11_15(*(2, 0)), doublelist(del(first(cons(0', gen_nil:cons12_15(n9192_15))), cons(0', gen_nil:cons12_15(n9192_15))))) ->_R^Omega(0)
cons(gen_0':s11_15(0), doublelist(del(0', cons(0', gen_nil:cons12_15(n9192_15))))) ->_R^Omega(0)
cons(gen_0':s11_15(0), doublelist(if(eq(0', 0'), 0', 0', gen_nil:cons12_15(n9192_15)))) ->_L^Omega(0)
cons(gen_0':s11_15(0), doublelist(if(true, 0', 0', gen_nil:cons12_15(n9192_15)))) ->_R^Omega(0)
cons(gen_0':s11_15(0), doublelist(gen_nil:cons12_15(n9192_15))) ->_IH
cons(gen_0':s11_15(0), gen_nil:cons12_15(c9193_15))

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

(26)
BOUNDS(1, INF)