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), 453 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), 0 ms]
    (10) CpxRNTS
    (11) CompleteCoflocoProof [FINISHED, 1335 ms]
    (12) BOUNDS(1, n^1)
(13) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
(14) TRS for Loop Detection
    (15) DecreasingLoopProof [LOWER BOUND(ID), 5 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:

   MINUS(z0, 0) -> c
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
   DOUBLE(0) -> c2
   DOUBLE(s(z0)) -> c3(DOUBLE(z0))
   PLUS(0, z0) -> c4
   PLUS(s(z0), z1) -> c5(PLUS(z0, z1))
   PLUS(s(z0), z1) -> c6(PLUS(z0, s(z1)))
   PLUS(s(z0), z1) -> c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1))
   PLUS(s(z0), z1) -> c8(PLUS(minus(z0, z1), double(z1)), DOUBLE(z1))

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

   minus(z0, 0) -> z0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   double(0) -> 0
   double(s(z0)) -> s(s(double(z0)))
   plus(0, z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   plus(s(z0), z1) -> plus(z0, s(z1))
   plus(s(z0), z1) -> s(plus(minus(z0, z1), double(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, n^1).


The TRS R consists of the following rules:

   MINUS(z0, 0) -> c
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
   DOUBLE(0) -> c2
   DOUBLE(s(z0)) -> c3(DOUBLE(z0))
   PLUS(0, z0) -> c4
   PLUS(s(z0), z1) -> c5(PLUS(z0, z1))
   PLUS(s(z0), z1) -> c6(PLUS(z0, s(z1)))
   PLUS(s(z0), z1) -> c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1))
   PLUS(s(z0), z1) -> c8(PLUS(minus(z0, z1), double(z1)), DOUBLE(z1))

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

   minus(z0, 0) -> z0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   double(0) -> 0
   double(s(z0)) -> s(s(double(z0)))
   plus(0, z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   plus(s(z0), z1) -> plus(z0, s(z1))
   plus(s(z0), z1) -> s(plus(minus(z0, z1), double(z1)))

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:

   MINUS(z0, 0) -> c [1]
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1)) [1]
   DOUBLE(0) -> c2 [1]
   DOUBLE(s(z0)) -> c3(DOUBLE(z0)) [1]
   PLUS(0, z0) -> c4 [1]
   PLUS(s(z0), z1) -> c5(PLUS(z0, z1)) [1]
   PLUS(s(z0), z1) -> c6(PLUS(z0, s(z1))) [1]
   PLUS(s(z0), z1) -> c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1)) [1]
   PLUS(s(z0), z1) -> c8(PLUS(minus(z0, z1), double(z1)), DOUBLE(z1)) [1]
   minus(z0, 0) -> z0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   double(0) -> 0 [0]
   double(s(z0)) -> s(s(double(z0))) [0]
   plus(0, z0) -> z0 [0]
   plus(s(z0), z1) -> s(plus(z0, z1)) [0]
   plus(s(z0), z1) -> plus(z0, s(z1)) [0]
   plus(s(z0), z1) -> s(plus(minus(z0, z1), double(z1))) [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:

   MINUS(z0, 0) -> c [1]
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1)) [1]
   DOUBLE(0) -> c2 [1]
   DOUBLE(s(z0)) -> c3(DOUBLE(z0)) [1]
   PLUS(0, z0) -> c4 [1]
   PLUS(s(z0), z1) -> c5(PLUS(z0, z1)) [1]
   PLUS(s(z0), z1) -> c6(PLUS(z0, s(z1))) [1]
   PLUS(s(z0), z1) -> c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1)) [1]
   PLUS(s(z0), z1) -> c8(PLUS(minus(z0, z1), double(z1)), DOUBLE(z1)) [1]
   minus(z0, 0) -> z0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   double(0) -> 0 [0]
   double(s(z0)) -> s(s(double(z0))) [0]
   plus(0, z0) -> z0 [0]
   plus(s(z0), z1) -> s(plus(z0, z1)) [0]
   plus(s(z0), z1) -> plus(z0, s(z1)) [0]
   plus(s(z0), z1) -> s(plus(minus(z0, z1), double(z1))) [0]

The TRS has the following type information:
MINUS :: 0:s -> 0:s -> c:c1
0 :: 0:s
c :: c:c1
s :: 0:s -> 0:s
c1 :: c:c1 -> c:c1
DOUBLE :: 0:s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
PLUS :: 0:s -> 0:s -> c4:c5:c6:c7:c8
c4 :: c4:c5:c6:c7:c8
c5 :: c4:c5:c6:c7:c8 -> c4:c5:c6:c7:c8
c6 :: c4:c5:c6:c7:c8 -> c4:c5:c6:c7:c8
c7 :: c4:c5:c6:c7:c8 -> c:c1 -> c4:c5:c6:c7:c8
minus :: 0:s -> 0:s -> 0:s
double :: 0:s -> 0:s
c8 :: c4:c5:c6:c7:c8 -> c2:c3 -> c4:c5:c6:c7:c8
plus :: 0:s -> 0:s -> 0:s

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:

   minus(v0, v1) -> null_minus [0]
   double(v0) -> null_double [0]
   plus(v0, v1) -> null_plus [0]
   MINUS(v0, v1) -> null_MINUS [0]
   DOUBLE(v0) -> null_DOUBLE [0]
   PLUS(v0, v1) -> null_PLUS [0]

And the following fresh constants:    null_minus, null_double, null_plus, null_MINUS, null_DOUBLE, null_PLUS

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

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

   MINUS(z0, 0) -> c [1]
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1)) [1]
   DOUBLE(0) -> c2 [1]
   DOUBLE(s(z0)) -> c3(DOUBLE(z0)) [1]
   PLUS(0, z0) -> c4 [1]
   PLUS(s(z0), z1) -> c5(PLUS(z0, z1)) [1]
   PLUS(s(z0), z1) -> c6(PLUS(z0, s(z1))) [1]
   PLUS(s(z0), z1) -> c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1)) [1]
   PLUS(s(z0), z1) -> c8(PLUS(minus(z0, z1), double(z1)), DOUBLE(z1)) [1]
   minus(z0, 0) -> z0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   double(0) -> 0 [0]
   double(s(z0)) -> s(s(double(z0))) [0]
   plus(0, z0) -> z0 [0]
   plus(s(z0), z1) -> s(plus(z0, z1)) [0]
   plus(s(z0), z1) -> plus(z0, s(z1)) [0]
   plus(s(z0), z1) -> s(plus(minus(z0, z1), double(z1))) [0]
   minus(v0, v1) -> null_minus [0]
   double(v0) -> null_double [0]
   plus(v0, v1) -> null_plus [0]
   MINUS(v0, v1) -> null_MINUS [0]
   DOUBLE(v0) -> null_DOUBLE [0]
   PLUS(v0, v1) -> null_PLUS [0]

The TRS has the following type information:
MINUS :: 0:s:null_minus:null_double:null_plus -> 0:s:null_minus:null_double:null_plus -> c:c1:null_MINUS
0 :: 0:s:null_minus:null_double:null_plus
c :: c:c1:null_MINUS
s :: 0:s:null_minus:null_double:null_plus -> 0:s:null_minus:null_double:null_plus
c1 :: c:c1:null_MINUS -> c:c1:null_MINUS
DOUBLE :: 0:s:null_minus:null_double:null_plus -> c2:c3:null_DOUBLE
c2 :: c2:c3:null_DOUBLE
c3 :: c2:c3:null_DOUBLE -> c2:c3:null_DOUBLE
PLUS :: 0:s:null_minus:null_double:null_plus -> 0:s:null_minus:null_double:null_plus -> c4:c5:c6:c7:c8:null_PLUS
c4 :: c4:c5:c6:c7:c8:null_PLUS
c5 :: c4:c5:c6:c7:c8:null_PLUS -> c4:c5:c6:c7:c8:null_PLUS
c6 :: c4:c5:c6:c7:c8:null_PLUS -> c4:c5:c6:c7:c8:null_PLUS
c7 :: c4:c5:c6:c7:c8:null_PLUS -> c:c1:null_MINUS -> c4:c5:c6:c7:c8:null_PLUS
minus :: 0:s:null_minus:null_double:null_plus -> 0:s:null_minus:null_double:null_plus -> 0:s:null_minus:null_double:null_plus
double :: 0:s:null_minus:null_double:null_plus -> 0:s:null_minus:null_double:null_plus
c8 :: c4:c5:c6:c7:c8:null_PLUS -> c2:c3:null_DOUBLE -> c4:c5:c6:c7:c8:null_PLUS
plus :: 0:s:null_minus:null_double:null_plus -> 0:s:null_minus:null_double:null_plus -> 0:s:null_minus:null_double:null_plus
null_minus :: 0:s:null_minus:null_double:null_plus
null_double :: 0:s:null_minus:null_double:null_plus
null_plus :: 0:s:null_minus:null_double:null_plus
null_MINUS :: c:c1:null_MINUS
null_DOUBLE :: c2:c3:null_DOUBLE
null_PLUS :: c4:c5:c6:c7:c8:null_PLUS

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
   c2 => 0
   c4 => 0
   null_minus => 0
   null_double => 0
   null_plus => 0
   null_MINUS => 0
   null_DOUBLE => 0
   null_PLUS => 0

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

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

   DOUBLE(z) -{ 1 }-> 0 :|: z = 0
   DOUBLE(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   DOUBLE(z) -{ 1 }-> 1 + DOUBLE(z0) :|: z = 1 + z0, z0 >= 0
   MINUS(z, z') -{ 1 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   MINUS(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   MINUS(z, z') -{ 1 }-> 1 + MINUS(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   PLUS(z, z') -{ 1 }-> 0 :|: z0 >= 0, z = 0, z' = z0
   PLUS(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   PLUS(z, z') -{ 1 }-> 1 + PLUS(z0, z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   PLUS(z, z') -{ 1 }-> 1 + PLUS(z0, 1 + z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   PLUS(z, z') -{ 1 }-> 1 + PLUS(minus(z0, z1), double(z1)) + MINUS(z0, z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   PLUS(z, z') -{ 1 }-> 1 + PLUS(minus(z0, z1), double(z1)) + DOUBLE(z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   double(z) -{ 0 }-> 0 :|: z = 0
   double(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   double(z) -{ 0 }-> 1 + (1 + double(z0)) :|: z = 1 + z0, z0 >= 0
   minus(z, z') -{ 0 }-> z0 :|: z = z0, z0 >= 0, z' = 0
   minus(z, z') -{ 0 }-> minus(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   minus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   plus(z, z') -{ 0 }-> z0 :|: z0 >= 0, z = 0, z' = z0
   plus(z, z') -{ 0 }-> plus(z0, 1 + z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   plus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   plus(z, z') -{ 0 }-> 1 + plus(z0, z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   plus(z, z') -{ 0 }-> 1 + plus(minus(z0, z1), double(z1)) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 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(V1, V),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun1(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[fun2(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[minus(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[double(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[plus(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(fun(V1, V, Out),1,[],[Out = 0,V1 = V2,V2 >= 0,V = 0]).
eq(fun(V1, V, Out),1,[fun(V4, V3, Ret1)],[Out = 1 + Ret1,V3 >= 0,V1 = 1 + V4,V4 >= 0,V = 1 + V3]).
eq(fun1(V1, Out),1,[],[Out = 0,V1 = 0]).
eq(fun1(V1, Out),1,[fun1(V5, Ret11)],[Out = 1 + Ret11,V1 = 1 + V5,V5 >= 0]).
eq(fun2(V1, V, Out),1,[],[Out = 0,V6 >= 0,V1 = 0,V = V6]).
eq(fun2(V1, V, Out),1,[fun2(V7, V8, Ret12)],[Out = 1 + Ret12,V8 >= 0,V1 = 1 + V7,V = V8,V7 >= 0]).
eq(fun2(V1, V, Out),1,[fun2(V9, 1 + V10, Ret13)],[Out = 1 + Ret13,V10 >= 0,V1 = 1 + V9,V = V10,V9 >= 0]).
eq(fun2(V1, V, Out),1,[minus(V11, V12, Ret010),double(V12, Ret011),fun2(Ret010, Ret011, Ret01),fun(V11, V12, Ret14)],[Out = 1 + Ret01 + Ret14,V12 >= 0,V1 = 1 + V11,V = V12,V11 >= 0]).
eq(fun2(V1, V, Out),1,[minus(V14, V13, Ret0101),double(V13, Ret0111),fun2(Ret0101, Ret0111, Ret012),fun1(V13, Ret15)],[Out = 1 + Ret012 + Ret15,V13 >= 0,V1 = 1 + V14,V = V13,V14 >= 0]).
eq(minus(V1, V, Out),0,[],[Out = V15,V1 = V15,V15 >= 0,V = 0]).
eq(minus(V1, V, Out),0,[minus(V16, V17, Ret)],[Out = Ret,V17 >= 0,V1 = 1 + V16,V16 >= 0,V = 1 + V17]).
eq(double(V1, Out),0,[],[Out = 0,V1 = 0]).
eq(double(V1, Out),0,[double(V18, Ret111)],[Out = 2 + Ret111,V1 = 1 + V18,V18 >= 0]).
eq(plus(V1, V, Out),0,[],[Out = V19,V19 >= 0,V1 = 0,V = V19]).
eq(plus(V1, V, Out),0,[plus(V21, V20, Ret16)],[Out = 1 + Ret16,V20 >= 0,V1 = 1 + V21,V = V20,V21 >= 0]).
eq(plus(V1, V, Out),0,[plus(V23, 1 + V22, Ret2)],[Out = Ret2,V22 >= 0,V1 = 1 + V23,V = V22,V23 >= 0]).
eq(plus(V1, V, Out),0,[minus(V24, V25, Ret10),double(V25, Ret112),plus(Ret10, Ret112, Ret17)],[Out = 1 + Ret17,V25 >= 0,V1 = 1 + V24,V = V25,V24 >= 0]).
eq(minus(V1, V, Out),0,[],[Out = 0,V27 >= 0,V26 >= 0,V1 = V27,V = V26]).
eq(double(V1, Out),0,[],[Out = 0,V28 >= 0,V1 = V28]).
eq(plus(V1, V, Out),0,[],[Out = 0,V30 >= 0,V29 >= 0,V1 = V30,V = V29]).
eq(fun(V1, V, Out),0,[],[Out = 0,V31 >= 0,V32 >= 0,V1 = V31,V = V32]).
eq(fun1(V1, Out),0,[],[Out = 0,V33 >= 0,V1 = V33]).
eq(fun2(V1, V, Out),0,[],[Out = 0,V34 >= 0,V35 >= 0,V1 = V34,V = V35]).
input_output_vars(fun(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun1(V1,Out),[V1],[Out]).
input_output_vars(fun2(V1,V,Out),[V1,V],[Out]).
input_output_vars(minus(V1,V,Out),[V1,V],[Out]).
input_output_vars(double(V1,Out),[V1],[Out]).
input_output_vars(plus(V1,V,Out),[V1,V],[Out]).


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

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

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

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

### Specialization of cost equations double/2 
* CE 22 is refined into CE [29] 
* CE 23 is refined into CE [30] 


### Cost equations --> "Loop" of double/2 
* CEs [30] --> Loop 18 
* CEs [29] --> Loop 19 

### Ranking functions of CR double(V1,Out) 
* RF of phase [18]: [V1]

#### Partial ranking functions of CR double(V1,Out) 
* Partial RF of phase [18]:
  - RF of loop [18:1]:
    V1


### Specialization of cost equations fun/3 
* CE 7 is refined into CE [31] 
* CE 9 is refined into CE [32] 
* CE 8 is refined into CE [33] 


### Cost equations --> "Loop" of fun/3 
* CEs [33] --> Loop 20 
* CEs [31,32] --> Loop 21 

### Ranking functions of CR fun(V1,V,Out) 
* RF of phase [20]: [V,V1]

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


### Specialization of cost equations fun1/2 
* CE 10 is refined into CE [34] 
* CE 12 is refined into CE [35] 
* CE 11 is refined into CE [36] 


### Cost equations --> "Loop" of fun1/2 
* CEs [36] --> Loop 22 
* CEs [34,35] --> Loop 23 

### Ranking functions of CR fun1(V1,Out) 
* RF of phase [22]: [V1]

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


### Specialization of cost equations minus/3 
* CE 21 is refined into CE [37] 
* CE 19 is refined into CE [38] 
* CE 20 is refined into CE [39] 


### Cost equations --> "Loop" of minus/3 
* CEs [39] --> Loop 24 
* CEs [37] --> Loop 25 
* CEs [38] --> Loop 26 

### Ranking functions of CR minus(V1,V,Out) 
* RF of phase [24]: [V,V1]

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


### Specialization of cost equations fun2/3 
* CE 13 is refined into CE [40] 
* CE 18 is refined into CE [41] 
* CE 14 is refined into CE [42] 
* CE 15 is refined into CE [43] 
* CE 16 is refined into CE [44,45,46,47,48,49,50,51,52] 
* CE 17 is refined into CE [53,54,55,56,57,58,59,60,61] 


### Cost equations --> "Loop" of fun2/3 
* CEs [52,61] --> Loop 27 
* CEs [51,60] --> Loop 28 
* CEs [43] --> Loop 29 
* CEs [50,59] --> Loop 30 
* CEs [49,58] --> Loop 31 
* CEs [48,57] --> Loop 32 
* CEs [47,56] --> Loop 33 
* CEs [46,55] --> Loop 34 
* CEs [45,54] --> Loop 35 
* CEs [42,44,53] --> Loop 36 
* CEs [40,41] --> Loop 37 

### Ranking functions of CR fun2(V1,V,Out) 
* RF of phase [27,28,29,30,31,36]: [V1,2*V1-1]

#### Partial ranking functions of CR fun2(V1,V,Out) 
* Partial RF of phase [27,28,29,30,31,36]:
  - RF of loop [27:1,28:1]:
    V1+V-2
    V1/3-V/3
  - RF of loop [27:1,28:1,30:1,31:1]:
    V1/2-1/2
  - RF of loop [29:1,36:1]:
    V1
  - RF of loop [30:1,31:1]:
    V depends on loops [27:1,28:1,29:1] 
    V1-V


### Specialization of cost equations plus/3 
* CE 28 is refined into CE [62] 
* CE 24 is refined into CE [63] 
* CE 25 is refined into CE [64] 
* CE 27 is refined into CE [65,66,67,68,69] 
* CE 26 is refined into CE [70] 


### Cost equations --> "Loop" of plus/3 
* CEs [69] --> Loop 38 
* CEs [70] --> Loop 39 
* CEs [68] --> Loop 40 
* CEs [67] --> Loop 41 
* CEs [66] --> Loop 42 
* CEs [64,65] --> Loop 43 
* CEs [62] --> Loop 44 
* CEs [63] --> Loop 45 

### Ranking functions of CR plus(V1,V,Out) 
* RF of phase [38,39,40,43]: [V1,2*V1-1]

#### Partial ranking functions of CR plus(V1,V,Out) 
* Partial RF of phase [38,39,40,43]:
  - RF of loop [38:1]:
    V1+V-2
    V1/3-V/3
  - RF of loop [38:1,40:1]:
    V1/2-1/2
  - RF of loop [39:1,43:1]:
    V1
  - RF of loop [40:1]:
    V depends on loops [38:1,39:1] 
    V1-V


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


### Cost equations --> "Loop" of start/2 
* CEs [79] --> Loop 46 
* CEs [71,72,73,74,75,76,77,78,80,81,82,83,84,85,86,87,88,89] --> Loop 47 

### Ranking functions of CR start(V1,V) 

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


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

#### Cost of chains of double(V1,Out):
* Chain [[18],19]: 0
  with precondition: [Out>=2,2*V1>=Out] 

* Chain [19]: 0
  with precondition: [Out=0,V1>=0] 


#### Cost of chains of fun(V1,V,Out):
* Chain [[20],21]: 1*it(20)+1
  Such that:it(20) =< Out

  with precondition: [Out>=1,V1>=Out,V>=Out] 

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


#### Cost of chains of fun1(V1,Out):
* Chain [[22],23]: 1*it(22)+1
  Such that:it(22) =< Out

  with precondition: [Out>=1,V1>=Out] 

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


#### Cost of chains of minus(V1,V,Out):
* Chain [[24],26]: 0
  with precondition: [V1=Out+V,V>=1,V1>=V] 

* Chain [[24],25]: 0
  with precondition: [Out=0,V1>=1,V>=1] 

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

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


#### Cost of chains of fun2(V1,V,Out):
* Chain [[27,28,29,30,31,36],37]: 2*it(27)+2*it(28)+3*it(29)+2*it(30)+2*it(31)+2*s(9)+2*s(11)+1
  Such that:aux(25) =< V1-V
aux(27) =< V1+V
aux(31) =< 2*V1+V
aux(36) =< V1/3-V/3
aux(40) =< V1
aux(41) =< 2*V1
aux(42) =< 3*V1
aux(43) =< V1/2
aux(44) =< V
aux(45) =< 2*V
it(27) =< aux(40)
it(28) =< aux(40)
it(29) =< aux(40)
it(30) =< aux(40)
it(31) =< aux(40)
it(30) =< aux(25)
it(31) =< aux(25)
it(30) =< aux(42)
it(31) =< aux(42)
it(29) =< aux(42)
it(27) =< aux(27)
it(28) =< aux(27)
it(30) =< aux(27)
it(31) =< aux(27)
it(27) =< aux(41)
it(28) =< aux(41)
it(30) =< aux(41)
it(31) =< aux(41)
it(29) =< aux(41)
aux(3) =< aux(31)
it(28) =< aux(31)
it(29) =< aux(31)
it(30) =< aux(31)
it(31) =< aux(31)
s(12) =< aux(31)
aux(3) =< aux(42)
it(28) =< aux(42)
s(12) =< aux(42)
it(27) =< aux(43)
it(28) =< aux(43)
it(30) =< aux(43)
it(31) =< aux(43)
it(27) =< aux(36)
it(28) =< aux(36)
it(27) =< aux(42)
it(30) =< it(29)+aux(3)+aux(3)+aux(44)
it(31) =< it(29)+aux(3)+aux(3)+aux(44)
aux(11) =< aux(3)*2
it(31) =< it(29)*2+aux(11)+aux(11)+aux(45)
s(12) =< it(29)*2+aux(11)+aux(11)+aux(45)
s(12) =< it(30)*aux(27)
s(11) =< s(12)
s(9) =< aux(3)

  with precondition: [V>=0,Out>=1,V1>=Out] 

* Chain [[27,28,29,30,31,36],35,37]: 2*it(27)+2*it(28)+3*it(29)+2*it(30)+2*it(31)+2*s(9)+2*s(11)+3
  Such that:aux(25) =< V1-V
aux(27) =< V1+V
aux(31) =< 2*V1+V
aux(36) =< V1/3-V/3
aux(46) =< V1
aux(47) =< 2*V1
aux(48) =< 3*V1
aux(49) =< V1/2
aux(50) =< V
aux(51) =< 2*V
it(27) =< aux(46)
it(28) =< aux(46)
it(29) =< aux(46)
it(30) =< aux(46)
it(31) =< aux(46)
it(30) =< aux(25)
it(31) =< aux(25)
it(30) =< aux(48)
it(31) =< aux(48)
it(29) =< aux(48)
it(27) =< aux(27)
it(28) =< aux(27)
it(30) =< aux(27)
it(31) =< aux(27)
it(27) =< aux(47)
it(28) =< aux(47)
it(30) =< aux(47)
it(31) =< aux(47)
it(29) =< aux(47)
aux(3) =< aux(31)
it(28) =< aux(31)
it(29) =< aux(31)
it(30) =< aux(31)
it(31) =< aux(31)
s(12) =< aux(31)
aux(3) =< aux(48)
it(28) =< aux(48)
s(12) =< aux(48)
it(27) =< aux(49)
it(28) =< aux(49)
it(30) =< aux(49)
it(31) =< aux(49)
it(27) =< aux(36)
it(28) =< aux(36)
it(27) =< aux(48)
it(30) =< it(29)+aux(3)+aux(3)+aux(50)
it(31) =< it(29)+aux(3)+aux(3)+aux(50)
aux(11) =< aux(3)*2
it(31) =< it(29)*2+aux(11)+aux(11)+aux(51)
s(12) =< it(29)*2+aux(11)+aux(11)+aux(51)
s(12) =< it(30)*aux(27)
s(11) =< s(12)
s(9) =< aux(3)

  with precondition: [V>=0,Out>=2,V1>=Out] 

* Chain [[27,28,29,30,31,36],34,37]: 2*it(27)+2*it(28)+1*it(29)+2*it(30)+2*it(31)+2*it(36)+4*s(9)+2*s(11)+3
  Such that:aux(25) =< V1-V
aux(36) =< V1/3-V/3
aux(38) =< V
aux(13) =< 2*V
aux(53) =< V1
aux(54) =< V1+V
aux(55) =< 2*V1
aux(56) =< 2*V1+V
aux(57) =< 3*V1
aux(58) =< V1/2
s(9) =< aux(56)
it(27) =< aux(53)
it(28) =< aux(53)
it(29) =< aux(53)
it(30) =< aux(53)
it(31) =< aux(53)
it(36) =< aux(53)
it(30) =< aux(25)
it(31) =< aux(25)
it(30) =< aux(57)
it(31) =< aux(57)
it(36) =< aux(57)
it(27) =< aux(54)
it(28) =< aux(54)
it(30) =< aux(54)
it(31) =< aux(54)
it(36) =< aux(54)
it(27) =< aux(55)
it(28) =< aux(55)
it(29) =< aux(55)
it(30) =< aux(55)
it(31) =< aux(55)
it(36) =< aux(55)
it(28) =< aux(56)
it(29) =< aux(56)
it(30) =< aux(56)
it(31) =< aux(56)
it(36) =< aux(56)
s(12) =< aux(56)
it(27) =< aux(58)
it(28) =< aux(58)
it(30) =< aux(58)
it(31) =< aux(58)
it(27) =< aux(36)
it(28) =< aux(36)
it(27) =< aux(57)
it(28) =< aux(57)
it(30) =< it(29)+aux(56)+aux(56)+aux(38)
it(31) =< it(29)+aux(56)+aux(56)+aux(38)
aux(11) =< aux(56)*2
it(30) =< it(29)+aux(56)+aux(56)+aux(53)
it(31) =< it(29)+aux(56)+aux(56)+aux(53)
it(31) =< it(29)*2+aux(11)+aux(11)+aux(55)
s(12) =< it(29)*2+aux(11)+aux(11)+aux(55)
it(31) =< it(29)*2+aux(11)+aux(11)+aux(13)
s(12) =< it(29)*2+aux(11)+aux(11)+aux(13)
s(12) =< it(30)*aux(54)
s(11) =< s(12)

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

* Chain [[27,28,29,30,31,36],33,37]: 2*it(27)+2*it(28)+3*it(29)+2*it(30)+2*it(31)+2*s(9)+2*s(11)+3
  Such that:aux(25) =< V1-V
aux(27) =< V1+V
aux(31) =< 2*V1+V
aux(36) =< V1/3-V/3
aux(38) =< V
aux(13) =< 2*V
aux(59) =< V1
aux(60) =< 2*V1
aux(61) =< 3*V1
aux(62) =< V1/2
it(27) =< aux(59)
it(28) =< aux(59)
it(29) =< aux(59)
it(30) =< aux(59)
it(31) =< aux(59)
it(30) =< aux(25)
it(31) =< aux(25)
it(30) =< aux(61)
it(31) =< aux(61)
it(29) =< aux(61)
it(27) =< aux(27)
it(28) =< aux(27)
it(30) =< aux(27)
it(31) =< aux(27)
it(27) =< aux(60)
it(28) =< aux(60)
it(30) =< aux(60)
it(31) =< aux(60)
it(29) =< aux(60)
aux(3) =< aux(31)
it(28) =< aux(31)
it(29) =< aux(31)
it(30) =< aux(31)
it(31) =< aux(31)
s(12) =< aux(31)
aux(3) =< aux(61)
it(28) =< aux(61)
s(12) =< aux(61)
it(27) =< aux(62)
it(28) =< aux(62)
it(30) =< aux(62)
it(31) =< aux(62)
it(27) =< aux(36)
it(28) =< aux(36)
it(27) =< aux(61)
it(30) =< it(29)+aux(3)+aux(3)+aux(38)
it(31) =< it(29)+aux(3)+aux(3)+aux(38)
aux(11) =< aux(3)*2
it(30) =< it(29)+aux(3)+aux(3)+aux(59)
it(31) =< it(29)+aux(3)+aux(3)+aux(59)
it(31) =< it(29)*2+aux(11)+aux(11)+aux(60)
s(12) =< it(29)*2+aux(11)+aux(11)+aux(60)
it(31) =< it(29)*2+aux(11)+aux(11)+aux(13)
s(12) =< it(29)*2+aux(11)+aux(11)+aux(13)
s(12) =< it(30)*aux(27)
s(11) =< s(12)
s(9) =< aux(3)

  with precondition: [V>=0,Out>=2,V1>=Out] 

* Chain [[27,28,29,30,31,36],32,37]: 2*it(27)+2*it(28)+1*it(29)+2*it(30)+2*it(31)+2*it(36)+2*s(9)+2*s(11)+2*s(15)+3
  Such that:aux(25) =< V1-V
aux(31) =< 2*V1+V
aux(32) =< 3*V1
aux(34) =< V1/2
aux(36) =< V1/3-V/3
aux(38) =< V
aux(13) =< 2*V
aux(63) =< V1
aux(64) =< V1+V
aux(65) =< 2*V1
s(15) =< aux(64)
it(27) =< aux(63)
it(28) =< aux(63)
it(29) =< aux(63)
it(30) =< aux(63)
it(31) =< aux(63)
it(36) =< aux(63)
it(30) =< aux(25)
it(31) =< aux(25)
it(30) =< aux(65)
it(31) =< aux(65)
it(36) =< aux(65)
it(27) =< aux(64)
it(28) =< aux(64)
it(30) =< aux(64)
it(31) =< aux(64)
it(36) =< aux(64)
it(27) =< aux(65)
it(28) =< aux(65)
it(29) =< aux(65)
aux(3) =< aux(31)
it(28) =< aux(31)
it(29) =< aux(31)
it(30) =< aux(31)
it(31) =< aux(31)
it(36) =< aux(31)
s(12) =< aux(31)
aux(3) =< aux(32)
it(28) =< aux(32)
it(29) =< aux(32)
it(30) =< aux(32)
it(31) =< aux(32)
it(36) =< aux(32)
s(12) =< aux(32)
it(27) =< aux(34)
it(28) =< aux(34)
it(30) =< aux(34)
it(31) =< aux(34)
it(27) =< aux(36)
it(28) =< aux(36)
it(30) =< it(29)+aux(3)+aux(3)+aux(38)
it(31) =< it(29)+aux(3)+aux(3)+aux(38)
aux(11) =< aux(3)*2
it(30) =< it(29)+aux(3)+aux(3)+aux(63)
it(31) =< it(29)+aux(3)+aux(3)+aux(63)
it(31) =< it(29)*2+aux(11)+aux(11)+aux(65)
s(12) =< it(29)*2+aux(11)+aux(11)+aux(65)
it(31) =< it(29)*2+aux(11)+aux(11)+aux(13)
s(12) =< it(29)*2+aux(11)+aux(11)+aux(13)
s(12) =< it(30)*aux(64)
s(11) =< s(12)
s(9) =< aux(3)

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

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

* Chain [35,37]: 3
  with precondition: [Out=1,V1>=1,V>=0] 

* Chain [34,37]: 2*s(13)+3
  Such that:aux(52) =< V
s(13) =< aux(52)

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

* Chain [33,37]: 3
  with precondition: [Out=1,V1>=1,V>=1] 

* Chain [32,37]: 1*s(15)+1*s(16)+3
  Such that:s(15) =< V1
s(16) =< V

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


#### Cost of chains of plus(V1,V,Out):
* Chain [[38,39,40,43],45]: 0
  with precondition: [V>=0,Out>=1,Out+V1>=V+2,V+V1>=Out] 

* Chain [[38,39,40,43],44]: 0
  with precondition: [V1>=1,V>=0,Out>=0,V1>=Out] 

* Chain [[38,39,40,43],42,45]: 0
  with precondition: [V1>=2,V>=0,Out>=1,V1>=Out] 

* Chain [[38,39,40,43],42,44]: 0
  with precondition: [V1>=2,V>=0,Out>=1,V1>=Out] 

* Chain [[38,39,40,43],41,45]: 0
  with precondition: [V1>=2,V>=0,Out>=3,2*V+2*V1>=Out+1] 

* Chain [[38,39,40,43],41,44]: 0
  with precondition: [V1>=2,V>=0,Out>=1,V1>=Out,V+V1>=Out+1] 

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

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

* Chain [42,45]: 0
  with precondition: [Out=1,V1>=1,V>=0] 

* Chain [42,44]: 0
  with precondition: [Out=1,V1>=1,V>=0] 

* Chain [41,45]: 0
  with precondition: [V1>=1,Out>=3,2*V+1>=Out] 

* Chain [41,44]: 0
  with precondition: [Out=1,V1>=1,V>=1] 


#### Cost of chains of start(V1,V):
* Chain [47]: 4*s(123)+2*s(124)+8*s(135)+10*s(136)+10*s(137)+4*s(138)+4*s(139)+4*s(143)+8*s(144)+4*s(145)+4*s(146)+4*s(148)+2*s(162)+2*s(163)+4*s(168)+4*s(174)+1*s(176)+2*s(177)+2*s(178)+2*s(181)+3
  Such that:aux(101) =< V1
aux(102) =< V1-V
aux(103) =< V1+V
aux(104) =< 2*V1
aux(105) =< 2*V1+V
aux(106) =< 3*V1
aux(107) =< V1/2
aux(108) =< V1/3-V/3
aux(109) =< V
aux(110) =< 2*V
s(124) =< aux(101)
s(123) =< aux(109)
s(135) =< aux(101)
s(136) =< aux(101)
s(137) =< aux(101)
s(138) =< aux(101)
s(139) =< aux(101)
s(138) =< aux(102)
s(139) =< aux(102)
s(138) =< aux(106)
s(139) =< aux(106)
s(137) =< aux(106)
s(135) =< aux(103)
s(136) =< aux(103)
s(138) =< aux(103)
s(139) =< aux(103)
s(135) =< aux(104)
s(136) =< aux(104)
s(138) =< aux(104)
s(139) =< aux(104)
s(137) =< aux(104)
s(140) =< aux(105)
s(136) =< aux(105)
s(137) =< aux(105)
s(138) =< aux(105)
s(139) =< aux(105)
s(141) =< aux(105)
s(140) =< aux(106)
s(136) =< aux(106)
s(141) =< aux(106)
s(135) =< aux(107)
s(136) =< aux(107)
s(138) =< aux(107)
s(139) =< aux(107)
s(135) =< aux(108)
s(136) =< aux(108)
s(135) =< aux(106)
s(138) =< s(137)+s(140)+s(140)+aux(109)
s(139) =< s(137)+s(140)+s(140)+aux(109)
s(142) =< s(140)*2
s(138) =< s(137)+s(140)+s(140)+aux(101)
s(139) =< s(137)+s(140)+s(140)+aux(101)
s(139) =< s(137)*2+s(142)+s(142)+aux(104)
s(141) =< s(137)*2+s(142)+s(142)+aux(104)
s(139) =< s(137)*2+s(142)+s(142)+aux(110)
s(141) =< s(137)*2+s(142)+s(142)+aux(110)
s(141) =< s(138)*aux(103)
s(143) =< s(141)
s(144) =< s(140)
s(145) =< aux(101)
s(146) =< aux(101)
s(145) =< aux(102)
s(146) =< aux(102)
s(145) =< aux(106)
s(146) =< aux(106)
s(145) =< aux(103)
s(146) =< aux(103)
s(145) =< aux(104)
s(146) =< aux(104)
s(145) =< aux(105)
s(146) =< aux(105)
s(147) =< aux(105)
s(147) =< aux(106)
s(145) =< aux(107)
s(146) =< aux(107)
s(145) =< s(137)+s(140)+s(140)+aux(109)
s(146) =< s(137)+s(140)+s(140)+aux(109)
s(146) =< s(137)*2+s(142)+s(142)+aux(110)
s(147) =< s(137)*2+s(142)+s(142)+aux(110)
s(147) =< s(145)*aux(103)
s(148) =< s(147)
s(162) =< aux(103)
s(163) =< aux(101)
s(168) =< aux(101)
s(168) =< aux(104)
s(163) =< aux(103)
s(168) =< aux(103)
s(163) =< aux(104)
s(168) =< aux(105)
s(168) =< aux(106)
s(163) =< aux(107)
s(163) =< aux(108)
s(174) =< aux(105)
s(176) =< aux(101)
s(177) =< aux(101)
s(178) =< aux(101)
s(177) =< aux(102)
s(178) =< aux(102)
s(177) =< aux(106)
s(178) =< aux(106)
s(177) =< aux(103)
s(178) =< aux(103)
s(176) =< aux(104)
s(177) =< aux(104)
s(178) =< aux(104)
s(176) =< aux(105)
s(177) =< aux(105)
s(178) =< aux(105)
s(179) =< aux(105)
s(177) =< aux(107)
s(178) =< aux(107)
s(177) =< s(176)+aux(105)+aux(105)+aux(109)
s(178) =< s(176)+aux(105)+aux(105)+aux(109)
s(180) =< aux(105)*2
s(177) =< s(176)+aux(105)+aux(105)+aux(101)
s(178) =< s(176)+aux(105)+aux(105)+aux(101)
s(178) =< s(176)*2+s(180)+s(180)+aux(104)
s(179) =< s(176)*2+s(180)+s(180)+aux(104)
s(178) =< s(176)*2+s(180)+s(180)+aux(110)
s(179) =< s(176)*2+s(180)+s(180)+aux(110)
s(179) =< s(177)*aux(103)
s(181) =< s(179)

  with precondition: [V1>=0] 

* Chain [46]: 0
  with precondition: [V=0,V1>=0] 


Closed-form bounds of start(V1,V): 
-------------------------------------
* Chain [47] with precondition: [V1>=0] 
    - Upper bound: 57*V1+3+nat(V)*4+nat(V1+V)*2+nat(2*V1+V)*22 
    - Complexity: n 
* Chain [46] with precondition: [V=0,V1>=0] 
    - Upper bound: 0 
    - Complexity: constant 

### Maximum cost of start(V1,V): 57*V1+3+nat(V)*4+nat(V1+V)*2+nat(2*V1+V)*22 
Asymptotic class: n 
* Total analysis performed in 1261 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:

   MINUS(z0, 0) -> c
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
   DOUBLE(0) -> c2
   DOUBLE(s(z0)) -> c3(DOUBLE(z0))
   PLUS(0, z0) -> c4
   PLUS(s(z0), z1) -> c5(PLUS(z0, z1))
   PLUS(s(z0), z1) -> c6(PLUS(z0, s(z1)))
   PLUS(s(z0), z1) -> c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1))
   PLUS(s(z0), z1) -> c8(PLUS(minus(z0, z1), double(z1)), DOUBLE(z1))

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

   minus(z0, 0) -> z0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   double(0) -> 0
   double(s(z0)) -> s(s(double(z0)))
   plus(0, z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   plus(s(z0), z1) -> plus(z0, s(z1))
   plus(s(z0), z1) -> s(plus(minus(z0, z1), double(z1)))

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

PLUS(s(z0), z1) ->^+ c6(PLUS(z0, s(z1)))

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

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

The result substitution is [z1 / s(z1)].




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

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

   MINUS(z0, 0) -> c
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
   DOUBLE(0) -> c2
   DOUBLE(s(z0)) -> c3(DOUBLE(z0))
   PLUS(0, z0) -> c4
   PLUS(s(z0), z1) -> c5(PLUS(z0, z1))
   PLUS(s(z0), z1) -> c6(PLUS(z0, s(z1)))
   PLUS(s(z0), z1) -> c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1))
   PLUS(s(z0), z1) -> c8(PLUS(minus(z0, z1), double(z1)), DOUBLE(z1))

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

   minus(z0, 0) -> z0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   double(0) -> 0
   double(s(z0)) -> s(s(double(z0)))
   plus(0, z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   plus(s(z0), z1) -> plus(z0, s(z1))
   plus(s(z0), z1) -> s(plus(minus(z0, z1), double(z1)))

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:

   MINUS(z0, 0) -> c
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
   DOUBLE(0) -> c2
   DOUBLE(s(z0)) -> c3(DOUBLE(z0))
   PLUS(0, z0) -> c4
   PLUS(s(z0), z1) -> c5(PLUS(z0, z1))
   PLUS(s(z0), z1) -> c6(PLUS(z0, s(z1)))
   PLUS(s(z0), z1) -> c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1))
   PLUS(s(z0), z1) -> c8(PLUS(minus(z0, z1), double(z1)), DOUBLE(z1))

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

   minus(z0, 0) -> z0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   double(0) -> 0
   double(s(z0)) -> s(s(double(z0)))
   plus(0, z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   plus(s(z0), z1) -> plus(z0, s(z1))
   plus(s(z0), z1) -> s(plus(minus(z0, z1), double(z1)))

Rewrite Strategy: INNERMOST