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

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

revApp#2(Nil, x16) → x16
revApp#2(Cons(x6, x4), x2) → revApp#2(x4, Cons(x6, x2))
dfsAcc#3(Leaf(x8), x16) → Cons(x8, x16)
dfsAcc#3(Node(x6, x4), x2) → dfsAcc#3(x4, dfsAcc#3(x6, x2))
main(x1) → revApp#2(dfsAcc#3(x1, Nil), Nil)

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

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

revApp#2(Nil, x16) → x16 [1]
revApp#2(Cons(x6, x4), x2) → revApp#2(x4, Cons(x6, x2)) [1]
dfsAcc#3(Leaf(x8), x16) → Cons(x8, x16) [1]
dfsAcc#3(Node(x6, x4), x2) → dfsAcc#3(x4, dfsAcc#3(x6, x2)) [1]
main(x1) → revApp#2(dfsAcc#3(x1, Nil), Nil) [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

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

revApp#2(Nil, x16) → x16 [1]
revApp#2(Cons(x6, x4), x2) → revApp#2(x4, Cons(x6, x2)) [1]
dfsAcc#3(Leaf(x8), x16) → Cons(x8, x16) [1]
dfsAcc#3(Node(x6, x4), x2) → dfsAcc#3(x4, dfsAcc#3(x6, x2)) [1]
main(x1) → revApp#2(dfsAcc#3(x1, Nil), Nil) [1]

The TRS has the following type information:

revApp#2 :: Nil:Cons → Nil:Cons → Nil:Cons Nil :: Nil:Cons Cons :: a → Nil:Cons → Nil:Cons dfsAcc#3 :: Leaf:Node → Nil:Cons → Nil:Cons Leaf :: a → Leaf:Node Node :: Leaf:Node → Leaf:Node → Leaf:Node main :: Leaf:Node → Nil:Cons

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

dfsAcc#3(v0, v1) → null_dfsAcc#3 [0]
revApp#2(v0, v1) → null_revApp#2 [0]

And the following fresh constants:

null_dfsAcc#3, null_revApp#2, const, const1

(6) 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: revApp#2(Nil, x16) → x16 [1] revApp#2(Cons(x6, x4), x2) → revApp#2(x4, Cons(x6, x2)) [1] dfsAcc#3(Leaf(x8), x16) → Cons(x8, x16) [1] dfsAcc#3(Node(x6, x4), x2) → dfsAcc#3(x4, dfsAcc#3(x6, x2)) [1] main(x1) → revApp#2(dfsAcc#3(x1, Nil), Nil) [1] dfsAcc#3(v0, v1) → null_dfsAcc#3 [0] revApp#2(v0, v1) → null_revApp#2 [0] The TRS has the following type information: revApp#2 :: Nil:Cons:null_dfsAcc#3:null_revApp#2 → Nil:Cons:null_dfsAcc#3:null_revApp#2 → Nil:Cons:null_dfsAcc#3:null_revApp#2 Nil :: Nil:Cons:null_dfsAcc#3:null_revApp#2 Cons :: a → Nil:Cons:null_dfsAcc#3:null_revApp#2 → Nil:Cons:null_dfsAcc#3:null_revApp#2 dfsAcc#3 :: Leaf:Node → Nil:Cons:null_dfsAcc#3:null_revApp#2 → Nil:Cons:null_dfsAcc#3:null_revApp#2 Leaf :: a → Leaf:Node Node :: Leaf:Node → Leaf:Node → Leaf:Node main :: Leaf:Node → Nil:Cons:null_dfsAcc#3:null_revApp#2 null_dfsAcc#3 :: Nil:Cons:null_dfsAcc#3:null_revApp#2 null_revApp#2 :: Nil:Cons:null_dfsAcc#3:null_revApp#2 const :: a const1 :: Leaf:Node Rewrite Strategy: INNERMOST

(7) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

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

Nil => 0
null_dfsAcc#3 => 0
null_revApp#2 => 0
const => 0
const1 => 0

(8) Obligation:

Complexity RNTS consisting of the following rules:

dfsAcc#3(z, z') -{ 1 }→ dfsAcc#3(x4, dfsAcc#3(x6, x2)) :|: z' = x2, x4 >= 0, x6 >= 0, z = 1 + x6 + x4, x2 >= 0
dfsAcc#3(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
dfsAcc#3(z, z') -{ 1 }→ 1 + x8 + x16 :|: x8 >= 0, z = 1 + x8, z' = x16, x16 >= 0
main(z) -{ 1 }→ revApp#2(dfsAcc#3(x1, 0), 0) :|: x1 >= 0, z = x1
revApp#2(z, z') -{ 1 }→ x16 :|: z' = x16, z = 0, x16 >= 0
revApp#2(z, z') -{ 1 }→ revApp#2(x4, 1 + x6 + x2) :|: z' = x2, x4 >= 0, x6 >= 0, z = 1 + x6 + x4, x2 >= 0
revApp#2(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1

Only complete derivations are relevant for the runtime complexity.

(9) CompleteCoflocoProof (EQUIVALENT transformation)

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

eq(start(V, V1),0,[fun(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[fun1(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[main(V, Out)],[V >= 0]). eq(fun(V, V1, Out),1,[],[Out = V2,V1 = V2,V = 0,V2 >= 0]). eq(fun(V, V1, Out),1,[fun(V3, 1 + V4 + V5, Ret)],[Out = Ret,V1 = V5,V3 >= 0,V4 >= 0,V = 1 + V3 + V4,V5 >= 0]). eq(fun1(V, V1, Out),1,[],[Out = 1 + V6 + V7,V6 >= 0,V = 1 + V6,V1 = V7,V7 >= 0]). eq(fun1(V, V1, Out),1,[fun1(V9, V10, Ret1),fun1(V8, Ret1, Ret2)],[Out = Ret2,V1 = V10,V8 >= 0,V9 >= 0,V = 1 + V8 + V9,V10 >= 0]). eq(main(V, Out),1,[fun1(V11, 0, Ret0),fun(Ret0, 0, Ret3)],[Out = Ret3,V11 >= 0,V = V11]). eq(fun1(V, V1, Out),0,[],[Out = 0,V12 >= 0,V13 >= 0,V = V12,V1 = V13]). eq(fun(V, V1, Out),0,[],[Out = 0,V14 >= 0,V15 >= 0,V = V14,V1 = V15]). input_output_vars(fun(V,V1,Out),[V,V1],[Out]). input_output_vars(fun1(V,V1,Out),[V,V1],[Out]). input_output_vars(main(V,Out),[V],[Out]).

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

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

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

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

### Specialization of cost equations fun/3
* CE 7 is refined into CE [12]
* CE 5 is refined into CE [13]
* CE 6 is refined into CE [14]


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

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

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


### Specialization of cost equations fun1/3
* CE 8 is refined into CE [15]
* CE 10 is refined into CE [16]
* CE 9 is refined into CE [17]


### Cost equations --> "Loop" of fun1/3
* CEs [17] --> Loop 12
* CEs [15] --> Loop 13
* CEs [16] --> Loop 14

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

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


### Specialization of cost equations main/2
* CE 11 is refined into CE [18,19,20,21,22,23,24]


### Cost equations --> "Loop" of main/2
* CEs [24] --> Loop 15
* CEs [21] --> Loop 16
* CEs [18,19,20,22,23] --> Loop 17

### Ranking functions of CR main(V,Out)

#### Partial ranking functions of CR main(V,Out)


### Specialization of cost equations start/2
* CE 2 is refined into CE [25,26,27]
* CE 3 is refined into CE [28,29,30]
* CE 4 is refined into CE [31,32,33]


### Cost equations --> "Loop" of start/2
* CEs [25,26,27,28,29,30,31,32,33] --> Loop 18

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

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


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

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

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

* Chain [[9],10]: 1*it(9)+0
Such that:it(9) =< V

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

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

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


#### Cost of chains of fun1(V,V1,Out):
* Chain [14]: 0
with precondition: [Out=0,V>=0,V1>=0]

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

* Chain [multiple([12],[[14],[13]])]: 1*it(12)+1*it([13])+0
Such that:it([13]) =< V/2+1/2
aux(1) =< V
it(12) =< aux(1)
it([13]) =< aux(1)

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


#### Cost of chains of main(V,Out):
* Chain [17]: 4*s(3)+2*s(4)+2
Such that:aux(3) =< V
aux(4) =< V/2+1/2
s(3) =< aux(3)
s(4) =< aux(4)
s(4) =< aux(3)

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

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

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

* Chain [15]: 1*s(12)+2*s(14)+2
Such that:s(12) =< V/2+1/2
aux(5) =< V
s(14) =< aux(5)
s(12) =< aux(5)

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


#### Cost of chains of start(V,V1):
* Chain [18]: 10*s(16)+4*s(18)+3
Such that:aux(6) =< V
aux(7) =< V/2+1/2
s(16) =< aux(6)
s(18) =< aux(7)
s(18) =< aux(6)

with precondition: [V>=0]


Closed-form bounds of start(V,V1):
-------------------------------------
* Chain [18] with precondition: [V>=0]
- Upper bound: 12*V+5
- Complexity: n

### Maximum cost of start(V,V1): 12*V+5
Asymptotic class: n
* Total analysis performed in 184 ms.

(10) BOUNDS(1, n^1)