WORST_CASE(Omega(n^1),O(n^1))
proof of /export/starexec/sandbox2/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, n^1).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 324 ms]
(2) CpxRelTRS
(3) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxWeightedTrs
    (5) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CpxTypedWeightedTrs
    (7) CompletionProof [UPPER BOUND(ID), 0 ms]
    (8) CpxTypedWeightedCompleteTrs
    (9) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 3 ms]
    (10) CpxRNTS
    (11) CompleteCoflocoProof [FINISHED, 774 ms]
    (12) BOUNDS(1, n^1)
(13) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
(14) TRS for Loop Detection
    (15) DecreasingLoopProof [LOWER BOUND(ID), 0 ms]
    (16) BEST
        (17) proven lower bound
            (18) LowerBoundPropagationProof [FINISHED, 0 ms]
            (19) BOUNDS(n^1, INF)
        (20) TRS for Loop Detection


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

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


The TRS R consists of the following rules:

   HALF(0) -> c
   HALF(s(0)) -> c1
   HALF(s(s(z0))) -> c2(HALF(z0))
   LASTBIT(0) -> c3
   LASTBIT(s(0)) -> c4
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
   CONV(0) -> c6
   CONV(s(z0)) -> c7(CONV(half(s(z0))), HALF(s(z0)))
   CONV(s(z0)) -> c8(LASTBIT(s(z0)))

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

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   lastbit(0) -> 0
   lastbit(s(0)) -> s(0)
   lastbit(s(s(z0))) -> lastbit(z0)
   conv(0) -> cons(nil, 0)
   conv(s(z0)) -> cons(conv(half(s(z0))), lastbit(s(z0)))

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, n^1).


The TRS R consists of the following rules:

   HALF(0) -> c
   HALF(s(0)) -> c1
   HALF(s(s(z0))) -> c2(HALF(z0))
   LASTBIT(0) -> c3
   LASTBIT(s(0)) -> c4
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
   CONV(0) -> c6
   CONV(s(z0)) -> c7(CONV(half(s(z0))), HALF(s(z0)))
   CONV(s(z0)) -> c8(LASTBIT(s(z0)))

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

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   lastbit(0) -> 0
   lastbit(s(0)) -> s(0)
   lastbit(s(s(z0))) -> lastbit(z0)
   conv(0) -> cons(nil, 0)
   conv(s(z0)) -> cons(conv(half(s(z0))), lastbit(s(z0)))

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

(3) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID))
Transformed relative TRS to weighted TRS
----------------------------------------

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


The TRS R consists of the following rules:

   HALF(0) -> c [1]
   HALF(s(0)) -> c1 [1]
   HALF(s(s(z0))) -> c2(HALF(z0)) [1]
   LASTBIT(0) -> c3 [1]
   LASTBIT(s(0)) -> c4 [1]
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0)) [1]
   CONV(0) -> c6 [1]
   CONV(s(z0)) -> c7(CONV(half(s(z0))), HALF(s(z0))) [1]
   CONV(s(z0)) -> c8(LASTBIT(s(z0))) [1]
   half(0) -> 0 [0]
   half(s(0)) -> 0 [0]
   half(s(s(z0))) -> s(half(z0)) [0]
   lastbit(0) -> 0 [0]
   lastbit(s(0)) -> s(0) [0]
   lastbit(s(s(z0))) -> lastbit(z0) [0]
   conv(0) -> cons(nil, 0) [0]
   conv(s(z0)) -> cons(conv(half(s(z0))), lastbit(s(z0))) [0]

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

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

(6)
Obligation:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   HALF(0) -> c [1]
   HALF(s(0)) -> c1 [1]
   HALF(s(s(z0))) -> c2(HALF(z0)) [1]
   LASTBIT(0) -> c3 [1]
   LASTBIT(s(0)) -> c4 [1]
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0)) [1]
   CONV(0) -> c6 [1]
   CONV(s(z0)) -> c7(CONV(half(s(z0))), HALF(s(z0))) [1]
   CONV(s(z0)) -> c8(LASTBIT(s(z0))) [1]
   half(0) -> 0 [0]
   half(s(0)) -> 0 [0]
   half(s(s(z0))) -> s(half(z0)) [0]
   lastbit(0) -> 0 [0]
   lastbit(s(0)) -> s(0) [0]
   lastbit(s(s(z0))) -> lastbit(z0) [0]
   conv(0) -> cons(nil, 0) [0]
   conv(s(z0)) -> cons(conv(half(s(z0))), lastbit(s(z0))) [0]

The TRS has the following type information:
HALF :: 0:s -> c:c1:c2
0 :: 0:s
c :: c:c1:c2
s :: 0:s -> 0:s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LASTBIT :: 0:s -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
CONV :: 0:s -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8 -> c:c1:c2 -> c6:c7:c8
half :: 0:s -> 0:s
c8 :: c3:c4:c5 -> c6:c7:c8
lastbit :: 0:s -> 0:s
conv :: 0:s -> nil:cons
cons :: nil:cons -> 0:s -> nil:cons
nil :: nil:cons

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

(7) CompletionProof (UPPER BOUND(ID))
The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

   half(v0) -> null_half [0]
   lastbit(v0) -> null_lastbit [0]
   conv(v0) -> null_conv [0]
   HALF(v0) -> null_HALF [0]
   LASTBIT(v0) -> null_LASTBIT [0]
   CONV(v0) -> null_CONV [0]

And the following fresh constants:    null_half, null_lastbit, null_conv, null_HALF, null_LASTBIT, null_CONV

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

(8)
Obligation:
Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   HALF(0) -> c [1]
   HALF(s(0)) -> c1 [1]
   HALF(s(s(z0))) -> c2(HALF(z0)) [1]
   LASTBIT(0) -> c3 [1]
   LASTBIT(s(0)) -> c4 [1]
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0)) [1]
   CONV(0) -> c6 [1]
   CONV(s(z0)) -> c7(CONV(half(s(z0))), HALF(s(z0))) [1]
   CONV(s(z0)) -> c8(LASTBIT(s(z0))) [1]
   half(0) -> 0 [0]
   half(s(0)) -> 0 [0]
   half(s(s(z0))) -> s(half(z0)) [0]
   lastbit(0) -> 0 [0]
   lastbit(s(0)) -> s(0) [0]
   lastbit(s(s(z0))) -> lastbit(z0) [0]
   conv(0) -> cons(nil, 0) [0]
   conv(s(z0)) -> cons(conv(half(s(z0))), lastbit(s(z0))) [0]
   half(v0) -> null_half [0]
   lastbit(v0) -> null_lastbit [0]
   conv(v0) -> null_conv [0]
   HALF(v0) -> null_HALF [0]
   LASTBIT(v0) -> null_LASTBIT [0]
   CONV(v0) -> null_CONV [0]

The TRS has the following type information:
HALF :: 0:s:null_half:null_lastbit -> c:c1:c2:null_HALF
0 :: 0:s:null_half:null_lastbit
c :: c:c1:c2:null_HALF
s :: 0:s:null_half:null_lastbit -> 0:s:null_half:null_lastbit
c1 :: c:c1:c2:null_HALF
c2 :: c:c1:c2:null_HALF -> c:c1:c2:null_HALF
LASTBIT :: 0:s:null_half:null_lastbit -> c3:c4:c5:null_LASTBIT
c3 :: c3:c4:c5:null_LASTBIT
c4 :: c3:c4:c5:null_LASTBIT
c5 :: c3:c4:c5:null_LASTBIT -> c3:c4:c5:null_LASTBIT
CONV :: 0:s:null_half:null_lastbit -> c6:c7:c8:null_CONV
c6 :: c6:c7:c8:null_CONV
c7 :: c6:c7:c8:null_CONV -> c:c1:c2:null_HALF -> c6:c7:c8:null_CONV
half :: 0:s:null_half:null_lastbit -> 0:s:null_half:null_lastbit
c8 :: c3:c4:c5:null_LASTBIT -> c6:c7:c8:null_CONV
lastbit :: 0:s:null_half:null_lastbit -> 0:s:null_half:null_lastbit
conv :: 0:s:null_half:null_lastbit -> nil:cons:null_conv
cons :: nil:cons:null_conv -> 0:s:null_half:null_lastbit -> nil:cons:null_conv
nil :: nil:cons:null_conv
null_half :: 0:s:null_half:null_lastbit
null_lastbit :: 0:s:null_half:null_lastbit
null_conv :: nil:cons:null_conv
null_HALF :: c:c1:c2:null_HALF
null_LASTBIT :: c3:c4:c5:null_LASTBIT
null_CONV :: c6:c7:c8:null_CONV

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

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID))
Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

   0 => 0
   c => 0
   c1 => 1
   c3 => 0
   c4 => 1
   c6 => 0
   nil => 0
   null_half => 0
   null_lastbit => 0
   null_conv => 0
   null_HALF => 0
   null_LASTBIT => 0
   null_CONV => 0

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

(10)
Obligation:
Complexity RNTS consisting of the following rules:

   CONV(z) -{ 1 }-> 0 :|: z = 0
   CONV(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   CONV(z) -{ 1 }-> 1 + LASTBIT(1 + z0) :|: z = 1 + z0, z0 >= 0
   CONV(z) -{ 1 }-> 1 + CONV(half(1 + z0)) + HALF(1 + z0) :|: z = 1 + z0, z0 >= 0
   HALF(z) -{ 1 }-> 1 :|: z = 1 + 0
   HALF(z) -{ 1 }-> 0 :|: z = 0
   HALF(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   HALF(z) -{ 1 }-> 1 + HALF(z0) :|: z0 >= 0, z = 1 + (1 + z0)
   LASTBIT(z) -{ 1 }-> 1 :|: z = 1 + 0
   LASTBIT(z) -{ 1 }-> 0 :|: z = 0
   LASTBIT(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   LASTBIT(z) -{ 1 }-> 1 + LASTBIT(z0) :|: z0 >= 0, z = 1 + (1 + z0)
   conv(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   conv(z) -{ 0 }-> 1 + conv(half(1 + z0)) + lastbit(1 + z0) :|: z = 1 + z0, z0 >= 0
   conv(z) -{ 0 }-> 1 + 0 + 0 :|: z = 0
   half(z) -{ 0 }-> 0 :|: z = 0
   half(z) -{ 0 }-> 0 :|: z = 1 + 0
   half(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   half(z) -{ 0 }-> 1 + half(z0) :|: z0 >= 0, z = 1 + (1 + z0)
   lastbit(z) -{ 0 }-> lastbit(z0) :|: z0 >= 0, z = 1 + (1 + z0)
   lastbit(z) -{ 0 }-> 0 :|: z = 0
   lastbit(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   lastbit(z) -{ 0 }-> 1 + 0 :|: z = 1 + 0

Only complete derivations are relevant for the runtime complexity.

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

(11) CompleteCoflocoProof (FINISHED)
Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V),0,[fun(V, Out)],[V >= 0]).
eq(start(V),0,[fun1(V, Out)],[V >= 0]).
eq(start(V),0,[fun2(V, Out)],[V >= 0]).
eq(start(V),0,[half(V, Out)],[V >= 0]).
eq(start(V),0,[lastbit(V, Out)],[V >= 0]).
eq(start(V),0,[conv(V, Out)],[V >= 0]).
eq(fun(V, Out),1,[],[Out = 0,V = 0]).
eq(fun(V, Out),1,[],[Out = 1,V = 1]).
eq(fun(V, Out),1,[fun(V1, Ret1)],[Out = 1 + Ret1,V1 >= 0,V = 2 + V1]).
eq(fun1(V, Out),1,[],[Out = 0,V = 0]).
eq(fun1(V, Out),1,[],[Out = 1,V = 1]).
eq(fun1(V, Out),1,[fun1(V2, Ret11)],[Out = 1 + Ret11,V2 >= 0,V = 2 + V2]).
eq(fun2(V, Out),1,[],[Out = 0,V = 0]).
eq(fun2(V, Out),1,[half(1 + V3, Ret010),fun2(Ret010, Ret01),fun(1 + V3, Ret12)],[Out = 1 + Ret01 + Ret12,V = 1 + V3,V3 >= 0]).
eq(fun2(V, Out),1,[fun1(1 + V4, Ret13)],[Out = 1 + Ret13,V = 1 + V4,V4 >= 0]).
eq(half(V, Out),0,[],[Out = 0,V = 0]).
eq(half(V, Out),0,[],[Out = 0,V = 1]).
eq(half(V, Out),0,[half(V5, Ret14)],[Out = 1 + Ret14,V5 >= 0,V = 2 + V5]).
eq(lastbit(V, Out),0,[],[Out = 0,V = 0]).
eq(lastbit(V, Out),0,[],[Out = 1,V = 1]).
eq(lastbit(V, Out),0,[lastbit(V6, Ret)],[Out = Ret,V6 >= 0,V = 2 + V6]).
eq(conv(V, Out),0,[],[Out = 1,V = 0]).
eq(conv(V, Out),0,[half(1 + V7, Ret0101),conv(Ret0101, Ret011),lastbit(1 + V7, Ret15)],[Out = 1 + Ret011 + Ret15,V = 1 + V7,V7 >= 0]).
eq(half(V, Out),0,[],[Out = 0,V8 >= 0,V = V8]).
eq(lastbit(V, Out),0,[],[Out = 0,V9 >= 0,V = V9]).
eq(conv(V, Out),0,[],[Out = 0,V10 >= 0,V = V10]).
eq(fun(V, Out),0,[],[Out = 0,V11 >= 0,V = V11]).
eq(fun1(V, Out),0,[],[Out = 0,V12 >= 0,V = V12]).
eq(fun2(V, Out),0,[],[Out = 0,V13 >= 0,V = V13]).
input_output_vars(fun(V,Out),[V],[Out]).
input_output_vars(fun1(V,Out),[V],[Out]).
input_output_vars(fun2(V,Out),[V],[Out]).
input_output_vars(half(V,Out),[V],[Out]).
input_output_vars(lastbit(V,Out),[V],[Out]).
input_output_vars(conv(V,Out),[V],[Out]).


CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components 
0. recursive  : [half/2]
1. recursive  : [lastbit/2]
2. recursive [non_tail] : [conv/2]
3. recursive  : [fun/2]
4. recursive  : [fun1/2]
5. recursive [non_tail] : [fun2/2]
6. non_recursive  : [start/1]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into half/2
1. SCC is partially evaluated into lastbit/2
2. SCC is partially evaluated into conv/2
3. SCC is partially evaluated into fun/2
4. SCC is partially evaluated into fun1/2
5. SCC is partially evaluated into fun2/2
6. SCC is partially evaluated into start/1

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations half/2 
* CE 19 is refined into CE [28] 
* CE 20 is refined into CE [29] 
* CE 21 is refined into CE [30] 


### Cost equations --> "Loop" of half/2 
* CEs [30] --> Loop 19 
* CEs [28,29] --> Loop 20 

### Ranking functions of CR half(V,Out) 
* RF of phase [19]: [V-1]

#### Partial ranking functions of CR half(V,Out) 
* Partial RF of phase [19]:
  - RF of loop [19:1]:
    V-1


### Specialization of cost equations lastbit/2 
* CE 22 is refined into CE [31] 
* CE 23 is refined into CE [32] 
* CE 24 is refined into CE [33] 


### Cost equations --> "Loop" of lastbit/2 
* CEs [33] --> Loop 21 
* CEs [31] --> Loop 22 
* CEs [32] --> Loop 23 

### Ranking functions of CR lastbit(V,Out) 
* RF of phase [21]: [V-1]

#### Partial ranking functions of CR lastbit(V,Out) 
* Partial RF of phase [21]:
  - RF of loop [21:1]:
    V-1


### Specialization of cost equations conv/2 
* CE 27 is refined into CE [34] 
* CE 25 is refined into CE [35] 
* CE 26 is refined into CE [36,37,38,39,40] 


### Cost equations --> "Loop" of conv/2 
* CEs [40] --> Loop 24 
* CEs [39] --> Loop 25 
* CEs [38] --> Loop 26 
* CEs [37] --> Loop 27 
* CEs [36] --> Loop 28 
* CEs [34] --> Loop 29 
* CEs [35] --> Loop 30 

### Ranking functions of CR conv(V,Out) 
* RF of phase [24,25]: [V-1]

#### Partial ranking functions of CR conv(V,Out) 
* Partial RF of phase [24,25]:
  - RF of loop [24:1]:
    V-2
    2/3*V-5/3
  - RF of loop [25:1]:
    V-1


### Specialization of cost equations fun/2 
* CE 8 is refined into CE [41] 
* CE 7 is refined into CE [42] 
* CE 10 is refined into CE [43] 
* CE 9 is refined into CE [44] 


### Cost equations --> "Loop" of fun/2 
* CEs [44] --> Loop 31 
* CEs [41] --> Loop 32 
* CEs [42,43] --> Loop 33 

### Ranking functions of CR fun(V,Out) 
* RF of phase [31]: [V-1]

#### Partial ranking functions of CR fun(V,Out) 
* Partial RF of phase [31]:
  - RF of loop [31:1]:
    V-1


### Specialization of cost equations fun1/2 
* CE 12 is refined into CE [45] 
* CE 11 is refined into CE [46] 
* CE 14 is refined into CE [47] 
* CE 13 is refined into CE [48] 


### Cost equations --> "Loop" of fun1/2 
* CEs [48] --> Loop 34 
* CEs [45] --> Loop 35 
* CEs [46,47] --> Loop 36 

### Ranking functions of CR fun1(V,Out) 
* RF of phase [34]: [V-1]

#### Partial ranking functions of CR fun1(V,Out) 
* Partial RF of phase [34]:
  - RF of loop [34:1]:
    V-1


### Specialization of cost equations fun2/2 
* CE 17 is refined into CE [49,50,51,52] 
* CE 15 is refined into CE [53] 
* CE 18 is refined into CE [54] 
* CE 16 is refined into CE [55,56,57,58,59,60,61] 


### Cost equations --> "Loop" of fun2/2 
* CEs [61] --> Loop 37 
* CEs [60] --> Loop 38 
* CEs [59] --> Loop 39 
* CEs [58] --> Loop 40 
* CEs [57] --> Loop 41 
* CEs [56] --> Loop 42 
* CEs [55] --> Loop 43 
* CEs [52] --> Loop 44 
* CEs [51] --> Loop 45 
* CEs [50] --> Loop 46 
* CEs [49] --> Loop 47 
* CEs [53,54] --> Loop 48 

### Ranking functions of CR fun2(V,Out) 
* RF of phase [37,38,39]: [V-1]

#### Partial ranking functions of CR fun2(V,Out) 
* Partial RF of phase [37,38,39]:
  - RF of loop [37:1,39:1]:
    V-1
  - RF of loop [38:1]:
    V-2
    2/3*V-5/3


### Specialization of cost equations start/1 
* CE 1 is refined into CE [62,63,64,65] 
* CE 2 is refined into CE [66,67,68,69] 
* CE 3 is refined into CE [70,71,72,73,74,75] 
* CE 4 is refined into CE [76,77] 
* CE 5 is refined into CE [78,79,80] 
* CE 6 is refined into CE [81,82,83,84,85,86,87,88,89] 


### Cost equations --> "Loop" of start/1 
* CEs [62,66,70,78,83] --> Loop 49 
* CEs [63,64,65,67,68,69,71,72,73,74,75,76,77,79,80,81,82,84,85,86,87,88,89] --> Loop 50 

### Ranking functions of CR start(V) 

#### Partial ranking functions of CR start(V) 


Computing Bounds
=====================================

#### Cost of chains of half(V,Out):
* Chain [[19],20]: 0
  with precondition: [Out>=1,V>=2*Out] 

* Chain [20]: 0
  with precondition: [Out=0,V>=0] 


#### Cost of chains of lastbit(V,Out):
* Chain [[21],23]: 0
  with precondition: [Out=1,V>=3] 

* Chain [[21],22]: 0
  with precondition: [Out=0,V>=2] 

* Chain [23]: 0
  with precondition: [V=1,Out=1] 

* Chain [22]: 0
  with precondition: [Out=0,V>=0] 


#### Cost of chains of conv(V,Out):
* Chain [[24,25],29]: 0
  with precondition: [Out>=1,V+2>=2*Out,V>=Out+1] 

* Chain [[24,25],28,30]: 0
  with precondition: [Out>=4,V+8>=2*Out,V+2>=Out] 

* Chain [[24,25],28,29]: 0
  with precondition: [Out>=3,V+6>=2*Out,V+1>=Out] 

* Chain [[24,25],27,30]: 0
  with precondition: [Out>=3,V+6>=2*Out,V+1>=Out] 

* Chain [[24,25],27,29]: 0
  with precondition: [Out>=2,V+4>=2*Out,V>=Out] 

* Chain [[24,25],26,30]: 0
  with precondition: [V>=6,Out>=4,V+9>=3*Out] 

* Chain [[24,25],26,29]: 0
  with precondition: [V>=6,Out>=3,V+6>=3*Out] 

* Chain [30]: 0
  with precondition: [V=0,Out=1] 

* Chain [29]: 0
  with precondition: [Out=0,V>=0] 

* Chain [28,30]: 0
  with precondition: [V=1,Out=3] 

* Chain [28,29]: 0
  with precondition: [V=1,Out=2] 

* Chain [27,30]: 0
  with precondition: [Out=2,V>=1] 

* Chain [27,29]: 0
  with precondition: [Out=1,V>=1] 

* Chain [26,30]: 0
  with precondition: [Out=3,V>=3] 

* Chain [26,29]: 0
  with precondition: [Out=2,V>=3] 


#### Cost of chains of fun(V,Out):
* Chain [[31],33]: 1*it(31)+1
  Such that:it(31) =< 2*Out

  with precondition: [Out>=1,V>=2*Out] 

* Chain [[31],32]: 1*it(31)+1
  Such that:it(31) =< 2*Out

  with precondition: [V+1=2*Out,V>=3] 

* Chain [33]: 1
  with precondition: [Out=0,V>=0] 

* Chain [32]: 1
  with precondition: [V=1,Out=1] 


#### Cost of chains of fun1(V,Out):
* Chain [[34],36]: 1*it(34)+1
  Such that:it(34) =< 2*Out

  with precondition: [Out>=1,V>=2*Out] 

* Chain [[34],35]: 1*it(34)+1
  Such that:it(34) =< 2*Out

  with precondition: [V+1=2*Out,V>=3] 

* Chain [36]: 1
  with precondition: [Out=0,V>=0] 

* Chain [35]: 1
  with precondition: [V=1,Out=1] 


#### Cost of chains of fun2(V,Out):
* Chain [[37,38,39],48]: 2*it(37)+2*it(38)+2*it(39)+1*s(5)+1*s(6)+1
  Such that:aux(6) =< 2*V
aux(5) =< 2*V+4/7
it(38) =< 2/3*V
aux(9) =< V
aux(10) =< 3*V
it(37) =< aux(9)
it(38) =< aux(9)
it(39) =< aux(9)
it(38) =< aux(5)
it(39) =< aux(5)
s(5) =< aux(5)
it(38) =< aux(6)
it(39) =< aux(6)
s(5) =< aux(6)
it(39) =< aux(10)
s(6) =< aux(10)

  with precondition: [V>=2,Out>=1,7*V>=4*Out+6] 

* Chain [[37,38,39],47]: 2*it(37)+2*it(38)+2*it(39)+1*s(5)+1*s(6)+2
  Such that:aux(6) =< 2*V
aux(5) =< 2*V+4/7
it(38) =< 2/3*V
aux(11) =< V
aux(12) =< 3*V
it(37) =< aux(11)
it(38) =< aux(11)
it(39) =< aux(11)
it(38) =< aux(5)
it(39) =< aux(5)
s(5) =< aux(5)
it(38) =< aux(6)
it(39) =< aux(6)
s(5) =< aux(6)
it(39) =< aux(12)
s(6) =< aux(12)

  with precondition: [V>=2,Out>=3,7*V+2>=4*Out] 

* Chain [[37,38,39],46]: 2*it(37)+2*it(38)+2*it(39)+1*s(5)+1*s(6)+2
  Such that:aux(6) =< 2*V
aux(5) =< 2*V+4/7
it(38) =< 2/3*V
aux(13) =< V
aux(14) =< 3*V
it(37) =< aux(13)
it(38) =< aux(13)
it(39) =< aux(13)
it(38) =< aux(5)
it(39) =< aux(5)
s(5) =< aux(5)
it(38) =< aux(6)
it(39) =< aux(6)
s(5) =< aux(6)
it(39) =< aux(14)
s(6) =< aux(14)

  with precondition: [V>=2,Out>=2,7*V>=4*Out+2] 

* Chain [[37,38,39],45]: 2*it(37)+2*it(38)+2*it(39)+1*s(5)+1*s(6)+1*s(7)+2
  Such that:aux(3) =< V
aux(5) =< 2*V+4/7
aux(7) =< 3*V
aux(8) =< 3*V+3
aux(15) =< V+1
aux(16) =< 2*V+2
s(7) =< aux(15)
it(38) =< aux(16)
it(37) =< aux(3)
it(38) =< aux(3)
it(39) =< aux(3)
it(37) =< aux(15)
it(38) =< aux(15)
it(39) =< aux(15)
it(38) =< aux(5)
it(39) =< aux(5)
s(5) =< aux(5)
it(39) =< aux(16)
s(5) =< aux(16)
it(39) =< aux(7)
s(6) =< aux(7)
it(39) =< aux(8)
s(6) =< aux(8)

  with precondition: [V>=6,Out>=4,5*V>=4*Out] 

* Chain [[37,38,39],44]: 2*it(37)+2*it(38)+2*it(39)+1*s(5)+1*s(6)+1*s(8)+2
  Such that:aux(5) =< 2*V+4/7
aux(17) =< V
aux(18) =< 2*V
aux(19) =< 3*V
it(38) =< aux(18)
s(8) =< aux(18)
it(37) =< aux(17)
it(38) =< aux(17)
it(39) =< aux(17)
it(38) =< aux(5)
it(39) =< aux(5)
s(5) =< aux(5)
it(39) =< aux(18)
s(5) =< aux(18)
it(39) =< aux(19)
s(6) =< aux(19)

  with precondition: [V>=4,Out>=3,11*V>=8*Out] 

* Chain [[37,38,39],43,48]: 2*it(37)+2*it(38)+2*it(39)+1*s(5)+1*s(6)+3
  Such that:aux(6) =< 2*V
aux(5) =< 2*V+4/7
it(38) =< 2/3*V
aux(20) =< V
aux(21) =< 3*V
it(37) =< aux(20)
it(38) =< aux(20)
it(39) =< aux(20)
it(38) =< aux(5)
it(39) =< aux(5)
s(5) =< aux(5)
it(38) =< aux(6)
it(39) =< aux(6)
s(5) =< aux(6)
it(39) =< aux(21)
s(6) =< aux(21)

  with precondition: [V>=2,Out>=3,7*V+2>=4*Out] 

* Chain [[37,38,39],42,48]: 2*it(37)+2*it(38)+2*it(39)+1*s(5)+1*s(6)+3
  Such that:aux(6) =< 2*V
aux(5) =< 2*V+4/7
it(38) =< 2/3*V
aux(22) =< V
aux(23) =< 3*V
it(37) =< aux(22)
it(38) =< aux(22)
it(39) =< aux(22)
it(38) =< aux(5)
it(39) =< aux(5)
s(5) =< aux(5)
it(38) =< aux(6)
it(39) =< aux(6)
s(5) =< aux(6)
it(39) =< aux(23)
s(6) =< aux(23)

  with precondition: [V>=2,Out>=2,7*V>=4*Out+2] 

* Chain [[37,38,39],41,48]: 2*it(37)+2*it(38)+2*it(39)+1*s(5)+1*s(6)+1*s(9)+3
  Such that:aux(3) =< V
aux(5) =< 2*V+4/7
aux(7) =< 3*V
aux(8) =< 3*V+9
aux(24) =< V+3
aux(25) =< 2*V+6
s(9) =< aux(24)
it(38) =< aux(25)
it(37) =< aux(3)
it(38) =< aux(3)
it(39) =< aux(3)
it(37) =< aux(24)
it(38) =< aux(24)
it(39) =< aux(24)
it(38) =< aux(5)
it(39) =< aux(5)
s(5) =< aux(5)
it(39) =< aux(25)
s(5) =< aux(25)
it(39) =< aux(7)
s(6) =< aux(7)
it(39) =< aux(8)
s(6) =< aux(8)

  with precondition: [V>=6,Out>=4,5*V>=4*Out] 

* Chain [[37,38,39],40,48]: 2*it(37)+2*it(38)+2*it(39)+1*s(5)+1*s(6)+1*s(10)+3
  Such that:aux(5) =< 2*V+4/7
aux(26) =< V
aux(27) =< 2*V
aux(28) =< 3*V
it(38) =< aux(27)
s(10) =< aux(27)
it(37) =< aux(26)
it(38) =< aux(26)
it(39) =< aux(26)
it(38) =< aux(5)
it(39) =< aux(5)
s(5) =< aux(5)
it(39) =< aux(27)
s(5) =< aux(27)
it(39) =< aux(28)
s(6) =< aux(28)

  with precondition: [V>=4,Out>=3,11*V>=8*Out] 

* Chain [48]: 1
  with precondition: [Out=0,V>=0] 

* Chain [47]: 2
  with precondition: [V=1,Out=2] 

* Chain [46]: 2
  with precondition: [Out=1,V>=1] 

* Chain [45]: 1*s(7)+2
  Such that:s(7) =< V+1

  with precondition: [V+3=2*Out,V>=3] 

* Chain [44]: 1*s(8)+2
  Such that:s(8) =< V

  with precondition: [Out>=2,V+2>=2*Out] 

* Chain [43,48]: 3
  with precondition: [V=1,Out=2] 

* Chain [42,48]: 3
  with precondition: [Out=1,V>=1] 

* Chain [41,48]: 1*s(9)+3
  Such that:s(9) =< 2*Out

  with precondition: [V+3=2*Out,V>=3] 

* Chain [40,48]: 1*s(10)+3
  Such that:s(10) =< V

  with precondition: [Out>=2,V+2>=2*Out] 


#### Cost of chains of start(V):
* Chain [50]: 4*s(104)+18*s(105)+10*s(113)+1*s(114)+1*s(122)+2*s(123)+2*s(124)+2*s(125)+1*s(126)+1*s(127)+2*s(128)+2*s(129)+2*s(130)+1*s(131)+1*s(132)+14*s(133)+7*s(134)+7*s(135)+4*s(136)+2*s(137)+3
  Such that:s(108) =< V+3
s(109) =< 2*V+2
s(110) =< 2*V+6
s(111) =< 3*V+3
s(112) =< 3*V+9
s(114) =< 7/2*V
aux(44) =< V
aux(45) =< V+1
aux(46) =< 2*V
aux(47) =< 2*V+4/7
aux(48) =< 3*V
aux(49) =< 2/3*V
s(105) =< aux(44)
s(104) =< aux(45)
s(113) =< aux(49)
s(122) =< s(108)
s(123) =< s(110)
s(124) =< aux(44)
s(123) =< aux(44)
s(125) =< aux(44)
s(124) =< s(108)
s(123) =< s(108)
s(125) =< s(108)
s(123) =< aux(47)
s(125) =< aux(47)
s(126) =< aux(47)
s(125) =< s(110)
s(126) =< s(110)
s(125) =< aux(48)
s(127) =< aux(48)
s(125) =< s(112)
s(127) =< s(112)
s(128) =< s(109)
s(129) =< aux(44)
s(128) =< aux(44)
s(130) =< aux(44)
s(129) =< aux(45)
s(128) =< aux(45)
s(130) =< aux(45)
s(128) =< aux(47)
s(130) =< aux(47)
s(131) =< aux(47)
s(130) =< s(109)
s(131) =< s(109)
s(130) =< aux(48)
s(132) =< aux(48)
s(130) =< s(111)
s(132) =< s(111)
s(113) =< aux(44)
s(133) =< aux(44)
s(113) =< aux(47)
s(133) =< aux(47)
s(134) =< aux(47)
s(113) =< aux(46)
s(133) =< aux(46)
s(134) =< aux(46)
s(133) =< aux(48)
s(135) =< aux(48)
s(136) =< aux(46)
s(137) =< aux(46)
s(136) =< aux(44)
s(136) =< aux(47)

  with precondition: [V>=0] 

* Chain [49]: 3
  with precondition: [V=1] 


Closed-form bounds of start(V): 
-------------------------------------
* Chain [50] with precondition: [V>=0] 
    - Upper bound: 721/6*V+218/7 
    - Complexity: n 
* Chain [49] with precondition: [V=1] 
    - Upper bound: 3 
    - Complexity: constant 

### Maximum cost of start(V): 721/6*V+218/7 
Asymptotic class: n 
* Total analysis performed in 657 ms.


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

(12)
BOUNDS(1, n^1)

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

(13) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID))
Transformed a relative TRS into a decreasing-loop problem.
----------------------------------------

(14)
Obligation:
Analyzing the following TRS for decreasing loops:

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


The TRS R consists of the following rules:

   HALF(0) -> c
   HALF(s(0)) -> c1
   HALF(s(s(z0))) -> c2(HALF(z0))
   LASTBIT(0) -> c3
   LASTBIT(s(0)) -> c4
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
   CONV(0) -> c6
   CONV(s(z0)) -> c7(CONV(half(s(z0))), HALF(s(z0)))
   CONV(s(z0)) -> c8(LASTBIT(s(z0)))

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

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   lastbit(0) -> 0
   lastbit(s(0)) -> s(0)
   lastbit(s(s(z0))) -> lastbit(z0)
   conv(0) -> cons(nil, 0)
   conv(s(z0)) -> cons(conv(half(s(z0))), lastbit(s(z0)))

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

(15) DecreasingLoopProof (LOWER BOUND(ID))
The following loop(s) give(s) rise to the lower bound Omega(n^1):

The rewrite sequence

LASTBIT(s(s(z0))) ->^+ c5(LASTBIT(z0))

gives rise to a decreasing loop by considering the right hand sides subterm at position [0].

The pumping substitution is [z0 / s(s(z0))].

The result substitution is [ ].




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

(16)
Complex Obligation (BEST)

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

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

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


The TRS R consists of the following rules:

   HALF(0) -> c
   HALF(s(0)) -> c1
   HALF(s(s(z0))) -> c2(HALF(z0))
   LASTBIT(0) -> c3
   LASTBIT(s(0)) -> c4
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
   CONV(0) -> c6
   CONV(s(z0)) -> c7(CONV(half(s(z0))), HALF(s(z0)))
   CONV(s(z0)) -> c8(LASTBIT(s(z0)))

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

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   lastbit(0) -> 0
   lastbit(s(0)) -> s(0)
   lastbit(s(s(z0))) -> lastbit(z0)
   conv(0) -> cons(nil, 0)
   conv(s(z0)) -> cons(conv(half(s(z0))), lastbit(s(z0)))

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

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

(19)
BOUNDS(n^1, INF)

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

(20)
Obligation:
Analyzing the following TRS for decreasing loops:

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


The TRS R consists of the following rules:

   HALF(0) -> c
   HALF(s(0)) -> c1
   HALF(s(s(z0))) -> c2(HALF(z0))
   LASTBIT(0) -> c3
   LASTBIT(s(0)) -> c4
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
   CONV(0) -> c6
   CONV(s(z0)) -> c7(CONV(half(s(z0))), HALF(s(z0)))
   CONV(s(z0)) -> c8(LASTBIT(s(z0)))

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

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   lastbit(0) -> 0
   lastbit(s(0)) -> s(0)
   lastbit(s(s(z0))) -> lastbit(z0)
   conv(0) -> cons(nil, 0)
   conv(s(z0)) -> cons(conv(half(s(z0))), lastbit(s(z0)))

Rewrite Strategy: INNERMOST