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


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

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 9 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 290 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 144 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), 370 ms]
        (20) typed CpxTrs


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

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


The TRS R consists of the following rules:

   numbers -> d(0)
   d(x) -> if(le(x, nr), x)
   if(true, x) -> cons(x, d(s(x)))
   if(false, x) -> nil
   le(0, y) -> true
   le(s(x), 0) -> false
   le(s(x), s(y)) -> le(x, y)
   nr -> ack(s(s(s(s(s(s(0)))))), 0)
   ack(0, x) -> s(x)
   ack(s(x), 0) -> ack(x, s(0))
   ack(s(x), s(y)) -> ack(x, ack(s(x), y))

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:
   numbers -> d(0)
   d(z0) -> if(le(z0, nr), z0)
   if(true, z0) -> cons(z0, d(s(z0)))
   if(false, z0) -> nil
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   nr -> ack(s(s(s(s(s(s(0)))))), 0)
   ack(0, z0) -> s(z0)
   ack(s(z0), 0) -> ack(z0, s(0))
   ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1))
Tuples:
   NUMBERS -> c(D(0))
   D(z0) -> c1(IF(le(z0, nr), z0), LE(z0, nr), NR)
   IF(true, z0) -> c2(D(s(z0)))
   IF(false, z0) -> c3
   LE(0, z0) -> c4
   LE(s(z0), 0) -> c5
   LE(s(z0), s(z1)) -> c6(LE(z0, z1))
   NR -> c7(ACK(s(s(s(s(s(s(0)))))), 0))
   ACK(0, z0) -> c8
   ACK(s(z0), 0) -> c9(ACK(z0, s(0)))
   ACK(s(z0), s(z1)) -> c10(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1))
S tuples:
   NUMBERS -> c(D(0))
   D(z0) -> c1(IF(le(z0, nr), z0), LE(z0, nr), NR)
   IF(true, z0) -> c2(D(s(z0)))
   IF(false, z0) -> c3
   LE(0, z0) -> c4
   LE(s(z0), 0) -> c5
   LE(s(z0), s(z1)) -> c6(LE(z0, z1))
   NR -> c7(ACK(s(s(s(s(s(s(0)))))), 0))
   ACK(0, z0) -> c8
   ACK(s(z0), 0) -> c9(ACK(z0, s(0)))
   ACK(s(z0), s(z1)) -> c10(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1))
K tuples:none
Defined Rule Symbols:   numbers, d_1, if_2, le_2, nr, ack_2

Defined Pair Symbols:   NUMBERS, D_1, IF_2, LE_2, NR, ACK_2

Compound Symbols:   c_1, c1_3, c2_1, c3, c4, c5, c6_1, c7_1, c8, c9_1, c10_2


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

(3) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

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


The TRS R consists of the following rules:

   NUMBERS -> c(D(0))
   D(z0) -> c1(IF(le(z0, nr), z0), LE(z0, nr), NR)
   IF(true, z0) -> c2(D(s(z0)))
   IF(false, z0) -> c3
   LE(0, z0) -> c4
   LE(s(z0), 0) -> c5
   LE(s(z0), s(z1)) -> c6(LE(z0, z1))
   NR -> c7(ACK(s(s(s(s(s(s(0)))))), 0))
   ACK(0, z0) -> c8
   ACK(s(z0), 0) -> c9(ACK(z0, s(0)))
   ACK(s(z0), s(z1)) -> c10(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1))

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

   numbers -> d(0)
   d(z0) -> if(le(z0, nr), z0)
   if(true, z0) -> cons(z0, d(s(z0)))
   if(false, z0) -> nil
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   nr -> ack(s(s(s(s(s(s(0)))))), 0)
   ack(0, z0) -> s(z0)
   ack(s(z0), 0) -> ack(z0, s(0))
   ack(s(z0), s(z1)) -> ack(z0, ack(s(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^1, INF).


The TRS R consists of the following rules:

   NUMBERS -> c(D(0'))
   D(z0) -> c1(IF(le(z0, nr), z0), LE(z0, nr), NR)
   IF(true, z0) -> c2(D(s(z0)))
   IF(false, z0) -> c3
   LE(0', z0) -> c4
   LE(s(z0), 0') -> c5
   LE(s(z0), s(z1)) -> c6(LE(z0, z1))
   NR -> c7(ACK(s(s(s(s(s(s(0')))))), 0'))
   ACK(0', z0) -> c8
   ACK(s(z0), 0') -> c9(ACK(z0, s(0')))
   ACK(s(z0), s(z1)) -> c10(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1))

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

   numbers -> d(0')
   d(z0) -> if(le(z0, nr), z0)
   if(true, z0) -> cons(z0, d(s(z0)))
   if(false, z0) -> nil
   le(0', z0) -> true
   le(s(z0), 0') -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   nr -> ack(s(s(s(s(s(s(0')))))), 0')
   ack(0', z0) -> s(z0)
   ack(s(z0), 0') -> ack(z0, s(0'))
   ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
NUMBERS -> c(D(0'))
D(z0) -> c1(IF(le(z0, nr), z0), LE(z0, nr), NR)
IF(true, z0) -> c2(D(s(z0)))
IF(false, z0) -> c3
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
NR -> c7(ACK(s(s(s(s(s(s(0')))))), 0'))
ACK(0', z0) -> c8
ACK(s(z0), 0') -> c9(ACK(z0, s(0')))
ACK(s(z0), s(z1)) -> c10(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1))
numbers -> d(0')
d(z0) -> if(le(z0, nr), z0)
if(true, z0) -> cons(z0, d(s(z0)))
if(false, z0) -> nil
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
nr -> ack(s(s(s(s(s(s(0')))))), 0')
ack(0', z0) -> s(z0)
ack(s(z0), 0') -> ack(z0, s(0'))
ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1))

Types:
NUMBERS :: c
c :: c1 -> c
D :: 0':s -> c1
0' :: 0':s
c1 :: c2:c3 -> c4:c5:c6 -> c7 -> c1
IF :: true:false -> 0':s -> c2:c3
le :: 0':s -> 0':s -> true:false
nr :: 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
NR :: c7
true :: true:false
c2 :: c1 -> c2:c3
s :: 0':s -> 0':s
false :: true:false
c3 :: c2:c3
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
c7 :: c8:c9:c10 -> c7
ACK :: 0':s -> 0':s -> c8:c9:c10
c8 :: c8:c9:c10
c9 :: c8:c9:c10 -> c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10 -> c8:c9:c10
ack :: 0':s -> 0':s -> 0':s
numbers :: cons:nil
d :: 0':s -> cons:nil
if :: true:false -> 0':s -> cons:nil
cons :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
hole_c1_11 :: c
hole_c12_11 :: c1
hole_0':s3_11 :: 0':s
hole_c2:c34_11 :: c2:c3
hole_c4:c5:c65_11 :: c4:c5:c6
hole_c76_11 :: c7
hole_true:false7_11 :: true:false
hole_c8:c9:c108_11 :: c8:c9:c10
hole_cons:nil9_11 :: cons:nil
gen_0':s10_11 :: Nat -> 0':s
gen_c4:c5:c611_11 :: Nat -> c4:c5:c6
gen_c8:c9:c1012_11 :: Nat -> c8:c9:c10
gen_cons:nil13_11 :: Nat -> cons:nil

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
D, le, LE, ACK, ack, d

They will be analysed ascendingly in the following order:
le < D
LE < D
le < d
ack < ACK

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

(10)
Obligation:
Innermost TRS:
Rules:
NUMBERS -> c(D(0'))
D(z0) -> c1(IF(le(z0, nr), z0), LE(z0, nr), NR)
IF(true, z0) -> c2(D(s(z0)))
IF(false, z0) -> c3
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
NR -> c7(ACK(s(s(s(s(s(s(0')))))), 0'))
ACK(0', z0) -> c8
ACK(s(z0), 0') -> c9(ACK(z0, s(0')))
ACK(s(z0), s(z1)) -> c10(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1))
numbers -> d(0')
d(z0) -> if(le(z0, nr), z0)
if(true, z0) -> cons(z0, d(s(z0)))
if(false, z0) -> nil
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
nr -> ack(s(s(s(s(s(s(0')))))), 0')
ack(0', z0) -> s(z0)
ack(s(z0), 0') -> ack(z0, s(0'))
ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1))

Types:
NUMBERS :: c
c :: c1 -> c
D :: 0':s -> c1
0' :: 0':s
c1 :: c2:c3 -> c4:c5:c6 -> c7 -> c1
IF :: true:false -> 0':s -> c2:c3
le :: 0':s -> 0':s -> true:false
nr :: 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
NR :: c7
true :: true:false
c2 :: c1 -> c2:c3
s :: 0':s -> 0':s
false :: true:false
c3 :: c2:c3
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
c7 :: c8:c9:c10 -> c7
ACK :: 0':s -> 0':s -> c8:c9:c10
c8 :: c8:c9:c10
c9 :: c8:c9:c10 -> c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10 -> c8:c9:c10
ack :: 0':s -> 0':s -> 0':s
numbers :: cons:nil
d :: 0':s -> cons:nil
if :: true:false -> 0':s -> cons:nil
cons :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
hole_c1_11 :: c
hole_c12_11 :: c1
hole_0':s3_11 :: 0':s
hole_c2:c34_11 :: c2:c3
hole_c4:c5:c65_11 :: c4:c5:c6
hole_c76_11 :: c7
hole_true:false7_11 :: true:false
hole_c8:c9:c108_11 :: c8:c9:c10
hole_cons:nil9_11 :: cons:nil
gen_0':s10_11 :: Nat -> 0':s
gen_c4:c5:c611_11 :: Nat -> c4:c5:c6
gen_c8:c9:c1012_11 :: Nat -> c8:c9:c10
gen_cons:nil13_11 :: Nat -> cons:nil


Generator Equations:
gen_0':s10_11(0) <=> 0'
gen_0':s10_11(+(x, 1)) <=> s(gen_0':s10_11(x))
gen_c4:c5:c611_11(0) <=> c4
gen_c4:c5:c611_11(+(x, 1)) <=> c6(gen_c4:c5:c611_11(x))
gen_c8:c9:c1012_11(0) <=> c8
gen_c8:c9:c1012_11(+(x, 1)) <=> c9(gen_c8:c9:c1012_11(x))
gen_cons:nil13_11(0) <=> nil
gen_cons:nil13_11(+(x, 1)) <=> cons(0', gen_cons:nil13_11(x))


The following defined symbols remain to be analysed:
le, D, LE, ACK, ack, d

They will be analysed ascendingly in the following order:
le < D
LE < D
le < d
ack < ACK

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

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

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

Induction Step:
le(gen_0':s10_11(+(n15_11, 1)), gen_0':s10_11(+(n15_11, 1))) ->_R^Omega(0)
le(gen_0':s10_11(n15_11), gen_0':s10_11(n15_11)) ->_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:
NUMBERS -> c(D(0'))
D(z0) -> c1(IF(le(z0, nr), z0), LE(z0, nr), NR)
IF(true, z0) -> c2(D(s(z0)))
IF(false, z0) -> c3
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
NR -> c7(ACK(s(s(s(s(s(s(0')))))), 0'))
ACK(0', z0) -> c8
ACK(s(z0), 0') -> c9(ACK(z0, s(0')))
ACK(s(z0), s(z1)) -> c10(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1))
numbers -> d(0')
d(z0) -> if(le(z0, nr), z0)
if(true, z0) -> cons(z0, d(s(z0)))
if(false, z0) -> nil
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
nr -> ack(s(s(s(s(s(s(0')))))), 0')
ack(0', z0) -> s(z0)
ack(s(z0), 0') -> ack(z0, s(0'))
ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1))

Types:
NUMBERS :: c
c :: c1 -> c
D :: 0':s -> c1
0' :: 0':s
c1 :: c2:c3 -> c4:c5:c6 -> c7 -> c1
IF :: true:false -> 0':s -> c2:c3
le :: 0':s -> 0':s -> true:false
nr :: 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
NR :: c7
true :: true:false
c2 :: c1 -> c2:c3
s :: 0':s -> 0':s
false :: true:false
c3 :: c2:c3
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
c7 :: c8:c9:c10 -> c7
ACK :: 0':s -> 0':s -> c8:c9:c10
c8 :: c8:c9:c10
c9 :: c8:c9:c10 -> c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10 -> c8:c9:c10
ack :: 0':s -> 0':s -> 0':s
numbers :: cons:nil
d :: 0':s -> cons:nil
if :: true:false -> 0':s -> cons:nil
cons :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
hole_c1_11 :: c
hole_c12_11 :: c1
hole_0':s3_11 :: 0':s
hole_c2:c34_11 :: c2:c3
hole_c4:c5:c65_11 :: c4:c5:c6
hole_c76_11 :: c7
hole_true:false7_11 :: true:false
hole_c8:c9:c108_11 :: c8:c9:c10
hole_cons:nil9_11 :: cons:nil
gen_0':s10_11 :: Nat -> 0':s
gen_c4:c5:c611_11 :: Nat -> c4:c5:c6
gen_c8:c9:c1012_11 :: Nat -> c8:c9:c10
gen_cons:nil13_11 :: Nat -> cons:nil


Lemmas:
le(gen_0':s10_11(n15_11), gen_0':s10_11(n15_11)) -> true, rt in Omega(0)


Generator Equations:
gen_0':s10_11(0) <=> 0'
gen_0':s10_11(+(x, 1)) <=> s(gen_0':s10_11(x))
gen_c4:c5:c611_11(0) <=> c4
gen_c4:c5:c611_11(+(x, 1)) <=> c6(gen_c4:c5:c611_11(x))
gen_c8:c9:c1012_11(0) <=> c8
gen_c8:c9:c1012_11(+(x, 1)) <=> c9(gen_c8:c9:c1012_11(x))
gen_cons:nil13_11(0) <=> nil
gen_cons:nil13_11(+(x, 1)) <=> cons(0', gen_cons:nil13_11(x))


The following defined symbols remain to be analysed:
LE, D, ACK, ack, d

They will be analysed ascendingly in the following order:
LE < D
ack < ACK

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LE(gen_0':s10_11(n370_11), gen_0':s10_11(n370_11)) -> gen_c4:c5:c611_11(n370_11), rt in Omega(1 + n370_11)

Induction Base:
LE(gen_0':s10_11(0), gen_0':s10_11(0)) ->_R^Omega(1)
c4

Induction Step:
LE(gen_0':s10_11(+(n370_11, 1)), gen_0':s10_11(+(n370_11, 1))) ->_R^Omega(1)
c6(LE(gen_0':s10_11(n370_11), gen_0':s10_11(n370_11))) ->_IH
c6(gen_c4:c5:c611_11(c371_11))

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:
NUMBERS -> c(D(0'))
D(z0) -> c1(IF(le(z0, nr), z0), LE(z0, nr), NR)
IF(true, z0) -> c2(D(s(z0)))
IF(false, z0) -> c3
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
NR -> c7(ACK(s(s(s(s(s(s(0')))))), 0'))
ACK(0', z0) -> c8
ACK(s(z0), 0') -> c9(ACK(z0, s(0')))
ACK(s(z0), s(z1)) -> c10(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1))
numbers -> d(0')
d(z0) -> if(le(z0, nr), z0)
if(true, z0) -> cons(z0, d(s(z0)))
if(false, z0) -> nil
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
nr -> ack(s(s(s(s(s(s(0')))))), 0')
ack(0', z0) -> s(z0)
ack(s(z0), 0') -> ack(z0, s(0'))
ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1))

Types:
NUMBERS :: c
c :: c1 -> c
D :: 0':s -> c1
0' :: 0':s
c1 :: c2:c3 -> c4:c5:c6 -> c7 -> c1
IF :: true:false -> 0':s -> c2:c3
le :: 0':s -> 0':s -> true:false
nr :: 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
NR :: c7
true :: true:false
c2 :: c1 -> c2:c3
s :: 0':s -> 0':s
false :: true:false
c3 :: c2:c3
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
c7 :: c8:c9:c10 -> c7
ACK :: 0':s -> 0':s -> c8:c9:c10
c8 :: c8:c9:c10
c9 :: c8:c9:c10 -> c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10 -> c8:c9:c10
ack :: 0':s -> 0':s -> 0':s
numbers :: cons:nil
d :: 0':s -> cons:nil
if :: true:false -> 0':s -> cons:nil
cons :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
hole_c1_11 :: c
hole_c12_11 :: c1
hole_0':s3_11 :: 0':s
hole_c2:c34_11 :: c2:c3
hole_c4:c5:c65_11 :: c4:c5:c6
hole_c76_11 :: c7
hole_true:false7_11 :: true:false
hole_c8:c9:c108_11 :: c8:c9:c10
hole_cons:nil9_11 :: cons:nil
gen_0':s10_11 :: Nat -> 0':s
gen_c4:c5:c611_11 :: Nat -> c4:c5:c6
gen_c8:c9:c1012_11 :: Nat -> c8:c9:c10
gen_cons:nil13_11 :: Nat -> cons:nil


Lemmas:
le(gen_0':s10_11(n15_11), gen_0':s10_11(n15_11)) -> true, rt in Omega(0)


Generator Equations:
gen_0':s10_11(0) <=> 0'
gen_0':s10_11(+(x, 1)) <=> s(gen_0':s10_11(x))
gen_c4:c5:c611_11(0) <=> c4
gen_c4:c5:c611_11(+(x, 1)) <=> c6(gen_c4:c5:c611_11(x))
gen_c8:c9:c1012_11(0) <=> c8
gen_c8:c9:c1012_11(+(x, 1)) <=> c9(gen_c8:c9:c1012_11(x))
gen_cons:nil13_11(0) <=> nil
gen_cons:nil13_11(+(x, 1)) <=> cons(0', gen_cons:nil13_11(x))


The following defined symbols remain to be analysed:
LE, D, ACK, ack, d

They will be analysed ascendingly in the following order:
LE < D
ack < ACK

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

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

(17)
BOUNDS(n^1, INF)

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

(18)
Obligation:
Innermost TRS:
Rules:
NUMBERS -> c(D(0'))
D(z0) -> c1(IF(le(z0, nr), z0), LE(z0, nr), NR)
IF(true, z0) -> c2(D(s(z0)))
IF(false, z0) -> c3
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
NR -> c7(ACK(s(s(s(s(s(s(0')))))), 0'))
ACK(0', z0) -> c8
ACK(s(z0), 0') -> c9(ACK(z0, s(0')))
ACK(s(z0), s(z1)) -> c10(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1))
numbers -> d(0')
d(z0) -> if(le(z0, nr), z0)
if(true, z0) -> cons(z0, d(s(z0)))
if(false, z0) -> nil
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
nr -> ack(s(s(s(s(s(s(0')))))), 0')
ack(0', z0) -> s(z0)
ack(s(z0), 0') -> ack(z0, s(0'))
ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1))

Types:
NUMBERS :: c
c :: c1 -> c
D :: 0':s -> c1
0' :: 0':s
c1 :: c2:c3 -> c4:c5:c6 -> c7 -> c1
IF :: true:false -> 0':s -> c2:c3
le :: 0':s -> 0':s -> true:false
nr :: 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
NR :: c7
true :: true:false
c2 :: c1 -> c2:c3
s :: 0':s -> 0':s
false :: true:false
c3 :: c2:c3
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
c7 :: c8:c9:c10 -> c7
ACK :: 0':s -> 0':s -> c8:c9:c10
c8 :: c8:c9:c10
c9 :: c8:c9:c10 -> c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10 -> c8:c9:c10
ack :: 0':s -> 0':s -> 0':s
numbers :: cons:nil
d :: 0':s -> cons:nil
if :: true:false -> 0':s -> cons:nil
cons :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
hole_c1_11 :: c
hole_c12_11 :: c1
hole_0':s3_11 :: 0':s
hole_c2:c34_11 :: c2:c3
hole_c4:c5:c65_11 :: c4:c5:c6
hole_c76_11 :: c7
hole_true:false7_11 :: true:false
hole_c8:c9:c108_11 :: c8:c9:c10
hole_cons:nil9_11 :: cons:nil
gen_0':s10_11 :: Nat -> 0':s
gen_c4:c5:c611_11 :: Nat -> c4:c5:c6
gen_c8:c9:c1012_11 :: Nat -> c8:c9:c10
gen_cons:nil13_11 :: Nat -> cons:nil


Lemmas:
le(gen_0':s10_11(n15_11), gen_0':s10_11(n15_11)) -> true, rt in Omega(0)
LE(gen_0':s10_11(n370_11), gen_0':s10_11(n370_11)) -> gen_c4:c5:c611_11(n370_11), rt in Omega(1 + n370_11)


Generator Equations:
gen_0':s10_11(0) <=> 0'
gen_0':s10_11(+(x, 1)) <=> s(gen_0':s10_11(x))
gen_c4:c5:c611_11(0) <=> c4
gen_c4:c5:c611_11(+(x, 1)) <=> c6(gen_c4:c5:c611_11(x))
gen_c8:c9:c1012_11(0) <=> c8
gen_c8:c9:c1012_11(+(x, 1)) <=> c9(gen_c8:c9:c1012_11(x))
gen_cons:nil13_11(0) <=> nil
gen_cons:nil13_11(+(x, 1)) <=> cons(0', gen_cons:nil13_11(x))


The following defined symbols remain to be analysed:
D, ACK, ack, d

They will be analysed ascendingly in the following order:
ack < ACK

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ack(gen_0':s10_11(1), gen_0':s10_11(+(1, n1713_11))) -> *14_11, rt in Omega(0)

Induction Base:
ack(gen_0':s10_11(1), gen_0':s10_11(+(1, 0)))

Induction Step:
ack(gen_0':s10_11(1), gen_0':s10_11(+(1, +(n1713_11, 1)))) ->_R^Omega(0)
ack(gen_0':s10_11(0), ack(s(gen_0':s10_11(0)), gen_0':s10_11(+(1, n1713_11)))) ->_IH
ack(gen_0':s10_11(0), *14_11)

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

(20)
Obligation:
Innermost TRS:
Rules:
NUMBERS -> c(D(0'))
D(z0) -> c1(IF(le(z0, nr), z0), LE(z0, nr), NR)
IF(true, z0) -> c2(D(s(z0)))
IF(false, z0) -> c3
LE(0', z0) -> c4
LE(s(z0), 0') -> c5
LE(s(z0), s(z1)) -> c6(LE(z0, z1))
NR -> c7(ACK(s(s(s(s(s(s(0')))))), 0'))
ACK(0', z0) -> c8
ACK(s(z0), 0') -> c9(ACK(z0, s(0')))
ACK(s(z0), s(z1)) -> c10(ACK(z0, ack(s(z0), z1)), ACK(s(z0), z1))
numbers -> d(0')
d(z0) -> if(le(z0, nr), z0)
if(true, z0) -> cons(z0, d(s(z0)))
if(false, z0) -> nil
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
nr -> ack(s(s(s(s(s(s(0')))))), 0')
ack(0', z0) -> s(z0)
ack(s(z0), 0') -> ack(z0, s(0'))
ack(s(z0), s(z1)) -> ack(z0, ack(s(z0), z1))

Types:
NUMBERS :: c
c :: c1 -> c
D :: 0':s -> c1
0' :: 0':s
c1 :: c2:c3 -> c4:c5:c6 -> c7 -> c1
IF :: true:false -> 0':s -> c2:c3
le :: 0':s -> 0':s -> true:false
nr :: 0':s
LE :: 0':s -> 0':s -> c4:c5:c6
NR :: c7
true :: true:false
c2 :: c1 -> c2:c3
s :: 0':s -> 0':s
false :: true:false
c3 :: c2:c3
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
c7 :: c8:c9:c10 -> c7
ACK :: 0':s -> 0':s -> c8:c9:c10
c8 :: c8:c9:c10
c9 :: c8:c9:c10 -> c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10 -> c8:c9:c10
ack :: 0':s -> 0':s -> 0':s
numbers :: cons:nil
d :: 0':s -> cons:nil
if :: true:false -> 0':s -> cons:nil
cons :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
hole_c1_11 :: c
hole_c12_11 :: c1
hole_0':s3_11 :: 0':s
hole_c2:c34_11 :: c2:c3
hole_c4:c5:c65_11 :: c4:c5:c6
hole_c76_11 :: c7
hole_true:false7_11 :: true:false
hole_c8:c9:c108_11 :: c8:c9:c10
hole_cons:nil9_11 :: cons:nil
gen_0':s10_11 :: Nat -> 0':s
gen_c4:c5:c611_11 :: Nat -> c4:c5:c6
gen_c8:c9:c1012_11 :: Nat -> c8:c9:c10
gen_cons:nil13_11 :: Nat -> cons:nil


Lemmas:
le(gen_0':s10_11(n15_11), gen_0':s10_11(n15_11)) -> true, rt in Omega(0)
LE(gen_0':s10_11(n370_11), gen_0':s10_11(n370_11)) -> gen_c4:c5:c611_11(n370_11), rt in Omega(1 + n370_11)
ack(gen_0':s10_11(1), gen_0':s10_11(+(1, n1713_11))) -> *14_11, rt in Omega(0)


Generator Equations:
gen_0':s10_11(0) <=> 0'
gen_0':s10_11(+(x, 1)) <=> s(gen_0':s10_11(x))
gen_c4:c5:c611_11(0) <=> c4
gen_c4:c5:c611_11(+(x, 1)) <=> c6(gen_c4:c5:c611_11(x))
gen_c8:c9:c1012_11(0) <=> c8
gen_c8:c9:c1012_11(+(x, 1)) <=> c9(gen_c8:c9:c1012_11(x))
gen_cons:nil13_11(0) <=> nil
gen_cons:nil13_11(+(x, 1)) <=> cons(0', gen_cons:nil13_11(x))


The following defined symbols remain to be analysed:
ACK, d