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


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

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
(3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CdtProblem
(5) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
(7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) CpxTRS
(9) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(10) CpxWeightedTrs
(11) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(12) CpxTypedWeightedTrs
(13) CompletionProof [UPPER BOUND(ID), 0 ms]
(14) CpxTypedWeightedCompleteTrs
(15) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
(16) CpxRNTS
(17) CompleteCoflocoProof [FINISHED, 134 ms]
(18) BOUNDS(1, n^1)


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

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


The TRS R consists of the following rules:

   double(0) -> 0
   double(s(x)) -> s(s(double(x)))
   +(x, 0) -> x
   +(x, s(y)) -> s(+(x, y))
   +(s(x), y) -> s(+(x, y))
   double(x) -> +(x, x)

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   double(0) -> 0
   double(s(z0)) -> s(s(double(z0)))
   double(z0) -> +(z0, z0)
   +(z0, 0) -> z0
   +(z0, s(z1)) -> s(+(z0, z1))
   +(s(z0), z1) -> s(+(z0, z1))
Tuples:
   DOUBLE(0) -> c
   DOUBLE(s(z0)) -> c1(DOUBLE(z0))
   DOUBLE(z0) -> c2(+'(z0, z0))
   +'(z0, 0) -> c3
   +'(z0, s(z1)) -> c4(+'(z0, z1))
   +'(s(z0), z1) -> c5(+'(z0, z1))
S tuples:
   DOUBLE(0) -> c
   DOUBLE(s(z0)) -> c1(DOUBLE(z0))
   DOUBLE(z0) -> c2(+'(z0, z0))
   +'(z0, 0) -> c3
   +'(z0, s(z1)) -> c4(+'(z0, z1))
   +'(s(z0), z1) -> c5(+'(z0, z1))
K tuples:none
Defined Rule Symbols:   double_1, +_2

Defined Pair Symbols:   DOUBLE_1, +'_2

Compound Symbols:   c, c1_1, c2_1, c3, c4_1, c5_1


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

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 2 trailing nodes:
   DOUBLE(0) -> c
   +'(z0, 0) -> c3

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   double(0) -> 0
   double(s(z0)) -> s(s(double(z0)))
   double(z0) -> +(z0, z0)
   +(z0, 0) -> z0
   +(z0, s(z1)) -> s(+(z0, z1))
   +(s(z0), z1) -> s(+(z0, z1))
Tuples:
   DOUBLE(s(z0)) -> c1(DOUBLE(z0))
   DOUBLE(z0) -> c2(+'(z0, z0))
   +'(z0, s(z1)) -> c4(+'(z0, z1))
   +'(s(z0), z1) -> c5(+'(z0, z1))
S tuples:
   DOUBLE(s(z0)) -> c1(DOUBLE(z0))
   DOUBLE(z0) -> c2(+'(z0, z0))
   +'(z0, s(z1)) -> c4(+'(z0, z1))
   +'(s(z0), z1) -> c5(+'(z0, z1))
K tuples:none
Defined Rule Symbols:   double_1, +_2

Defined Pair Symbols:   DOUBLE_1, +'_2

Compound Symbols:   c1_1, c2_1, c4_1, c5_1


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

(5) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   double(0) -> 0
   double(s(z0)) -> s(s(double(z0)))
   double(z0) -> +(z0, z0)
   +(z0, 0) -> z0
   +(z0, s(z1)) -> s(+(z0, z1))
   +(s(z0), z1) -> s(+(z0, z1))

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   DOUBLE(s(z0)) -> c1(DOUBLE(z0))
   DOUBLE(z0) -> c2(+'(z0, z0))
   +'(z0, s(z1)) -> c4(+'(z0, z1))
   +'(s(z0), z1) -> c5(+'(z0, z1))
S tuples:
   DOUBLE(s(z0)) -> c1(DOUBLE(z0))
   DOUBLE(z0) -> c2(+'(z0, z0))
   +'(z0, s(z1)) -> c4(+'(z0, z1))
   +'(s(z0), z1) -> c5(+'(z0, z1))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:   DOUBLE_1, +'_2

Compound Symbols:   c1_1, c2_1, c4_1, c5_1


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

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

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


The TRS R consists of the following rules:

   DOUBLE(s(z0)) -> c1(DOUBLE(z0))
   DOUBLE(z0) -> c2(+'(z0, z0))
   +'(z0, s(z1)) -> c4(+'(z0, z1))
   +'(s(z0), z1) -> c5(+'(z0, z1))

S is empty.
Rewrite Strategy: INNERMOST
----------------------------------------

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

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

   DOUBLE(s(z0)) -> c1(DOUBLE(z0)) [1]
   DOUBLE(z0) -> c2(+'(z0, z0)) [1]
   +'(z0, s(z1)) -> c4(+'(z0, z1)) [1]
   +'(s(z0), z1) -> c5(+'(z0, z1)) [1]

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

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

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

   DOUBLE(s(z0)) -> c1(DOUBLE(z0)) [1]
   DOUBLE(z0) -> c2(+'(z0, z0)) [1]
   +'(z0, s(z1)) -> c4(+'(z0, z1)) [1]
   +'(s(z0), z1) -> c5(+'(z0, z1)) [1]

The TRS has the following type information:
DOUBLE :: s -> c1:c2
s :: s -> s
c1 :: c1:c2 -> c1:c2
c2 :: c4:c5 -> c1:c2
+' :: s -> s -> c4:c5
c4 :: c4:c5 -> c4:c5
c5 :: c4:c5 -> c4:c5

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

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

   +'(v0, v1) -> null_+' [0]

And the following fresh constants:    null_+', const, const1

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

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

   DOUBLE(s(z0)) -> c1(DOUBLE(z0)) [1]
   DOUBLE(z0) -> c2(+'(z0, z0)) [1]
   +'(z0, s(z1)) -> c4(+'(z0, z1)) [1]
   +'(s(z0), z1) -> c5(+'(z0, z1)) [1]
   +'(v0, v1) -> null_+' [0]

The TRS has the following type information:
DOUBLE :: s -> c1:c2
s :: s -> s
c1 :: c1:c2 -> c1:c2
c2 :: c4:c5:null_+' -> c1:c2
+' :: s -> s -> c4:c5:null_+'
c4 :: c4:c5:null_+' -> c4:c5:null_+'
c5 :: c4:c5:null_+' -> c4:c5:null_+'
null_+' :: c4:c5:null_+'
const :: c1:c2
const1 :: s

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

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

   null_+' => 0
   const => 0
   const1 => 0

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

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

   +'(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   +'(z, z') -{ 1 }-> 1 + +'(z0, z1) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   +'(z, z') -{ 1 }-> 1 + +'(z0, z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   DOUBLE(z) -{ 1 }-> 1 + DOUBLE(z0) :|: z = 1 + z0, z0 >= 0
   DOUBLE(z) -{ 1 }-> 1 + +'(z0, z0) :|: z = z0, z0 >= 0

Only complete derivations are relevant for the runtime complexity.

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

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

eq(start(V, V3),0,[fun(V, Out)],[V >= 0]).
eq(start(V, V3),0,[fun1(V, V3, Out)],[V >= 0,V3 >= 0]).
eq(fun(V, Out),1,[fun(V1, Ret1)],[Out = 1 + Ret1,V = 1 + V1,V1 >= 0]).
eq(fun(V, Out),1,[fun1(V2, V2, Ret11)],[Out = 1 + Ret11,V = V2,V2 >= 0]).
eq(fun1(V, V3, Out),1,[fun1(V5, V4, Ret12)],[Out = 1 + Ret12,V = V5,V4 >= 0,V5 >= 0,V3 = 1 + V4]).
eq(fun1(V, V3, Out),1,[fun1(V6, V7, Ret13)],[Out = 1 + Ret13,V7 >= 0,V = 1 + V6,V3 = V7,V6 >= 0]).
eq(fun1(V, V3, Out),0,[],[Out = 0,V9 >= 0,V8 >= 0,V = V9,V3 = V8]).
input_output_vars(fun(V,Out),[V],[Out]).
input_output_vars(fun1(V,V3,Out),[V,V3],[Out]).


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

#### Computed strongly connected components 
0. recursive  : [fun1/3]
1. recursive  : [fun/2]
2. non_recursive  : [start/2]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into fun1/3
1. SCC is partially evaluated into fun/2
2. SCC is partially evaluated into start/2

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

### Specialization of cost equations fun1/3 
* CE 7 is refined into CE [8] 
* CE 5 is refined into CE [9] 
* CE 6 is refined into CE [10] 


### Cost equations --> "Loop" of fun1/3 
* CEs [9] --> Loop 7 
* CEs [10] --> Loop 8 
* CEs [8] --> Loop 9 

### Ranking functions of CR fun1(V,V3,Out) 
* RF of phase [7,8]: [V+V3]

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


### Specialization of cost equations fun/2 
* CE 4 is refined into CE [11,12] 
* CE 3 is refined into CE [13] 


### Cost equations --> "Loop" of fun/2 
* CEs [13] --> Loop 10 
* CEs [12] --> Loop 11 
* CEs [11] --> Loop 12 

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

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


### Specialization of cost equations start/2 
* CE 1 is refined into CE [14,15] 
* CE 2 is refined into CE [16,17] 


### Cost equations --> "Loop" of start/2 
* CEs [14,15,16,17] --> Loop 13 

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

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


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

#### Cost of chains of fun1(V,V3,Out):
* Chain [[7,8],9]: 2*it(7)+0
  Such that:aux(1) =< V+V3
aux(3) =< Out
it(7) =< aux(3)
it(7) =< aux(1)

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

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


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

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

* Chain [[10],11]: 3*it(10)+1
  Such that:aux(5) =< 2*V
it(10) =< aux(5)

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

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

* Chain [11]: 2*s(3)+1
  Such that:aux(4) =< 2*V
s(3) =< aux(4)

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


#### Cost of chains of start(V,V3):
* Chain [13]: 1*s(9)+5*s(11)+2*s(14)+1
  Such that:aux(7) =< V+V3
s(10) =< 2*V
s(9) =< 2*V+1
s(14) =< aux(7)
s(11) =< s(10)

  with precondition: [V>=0] 


Closed-form bounds of start(V,V3): 
-------------------------------------
* Chain [13] with precondition: [V>=0] 
    - Upper bound: 10*V+1+nat(V+V3)*2+(2*V+1) 
    - Complexity: n 

### Maximum cost of start(V,V3): 10*V+1+nat(V+V3)*2+(2*V+1) 
Asymptotic class: n 
* Total analysis performed in 101 ms.


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

(18)
BOUNDS(1, n^1)