0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 235 ms)
↳10 BOUNDS(1, n^1)
digits → d(0)
d(x) → if(le(x, s(s(s(s(s(s(s(s(s(0)))))))))), 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)
digits → d(0) [1]
d(x) → if(le(x, s(s(s(s(s(s(s(s(s(0)))))))))), x) [1]
if(true, x) → cons(x, d(s(x))) [1]
if(false, x) → nil [1]
le(0, y) → true [1]
le(s(x), 0) → false [1]
le(s(x), s(y)) → le(x, y) [1]
digits → d(0) [1]
d(x) → if(le(x, s(s(s(s(s(s(s(s(s(0)))))))))), x) [1]
if(true, x) → cons(x, d(s(x))) [1]
if(false, x) → nil [1]
le(0, y) → true [1]
le(s(x), 0) → false [1]
le(s(x), s(y)) → le(x, y) [1]
| digits :: cons:nil d :: 0:s → cons:nil 0 :: 0:s if :: true:false → 0:s → cons:nil le :: 0:s → 0:s → true:false s :: 0:s → 0:s true :: true:false cons :: 0:s → cons:nil → cons:nil false :: true:false nil :: cons:nil |
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
true => 1
false => 0
nil => 0
d(z) -{ 1 }→ if(le(x, 1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + 0))))))))), x) :|: x >= 0, z = x
digits -{ 1 }→ d(0) :|:
if(z, z') -{ 1 }→ 0 :|: z' = x, x >= 0, z = 0
if(z, z') -{ 1 }→ 1 + x + d(1 + x) :|: z' = x, z = 1, x >= 0
le(z, z') -{ 1 }→ le(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
le(z, z') -{ 1 }→ 1 :|: y >= 0, z = 0, z' = y
le(z, z') -{ 1 }→ 0 :|: x >= 0, z = 1 + x, z' = 0
| eq(start(V, V2),0,[digits(Out)],[]). eq(start(V, V2),0,[d(V, Out)],[V >= 0]). eq(start(V, V2),0,[if(V, V2, Out)],[V >= 0,V2 >= 0]). eq(start(V, V2),0,[le(V, V2, Out)],[V >= 0,V2 >= 0]). eq(digits(Out),1,[d(0, Ret)],[Out = Ret]). eq(d(V, Out),1,[le(V1, 1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + 0)))))))), Ret0),if(Ret0, V1, Ret1)],[Out = Ret1,V1 >= 0,V = V1]). eq(if(V, V2, Out),1,[d(1 + V3, Ret11)],[Out = 1 + Ret11 + V3,V2 = V3,V = 1,V3 >= 0]). eq(if(V, V2, Out),1,[],[Out = 0,V2 = V4,V4 >= 0,V = 0]). eq(le(V, V2, Out),1,[],[Out = 1,V5 >= 0,V = 0,V2 = V5]). eq(le(V, V2, Out),1,[],[Out = 0,V6 >= 0,V = 1 + V6,V2 = 0]). eq(le(V, V2, Out),1,[le(V7, V8, Ret2)],[Out = Ret2,V2 = 1 + V8,V7 >= 0,V8 >= 0,V = 1 + V7]). input_output_vars(digits(Out),[],[Out]). input_output_vars(d(V,Out),[V],[Out]). input_output_vars(if(V,V2,Out),[V,V2],[Out]). input_output_vars(le(V,V2,Out),[V,V2],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [le/3]
1. recursive : [d/2,if/3]
2. non_recursive : [digits/1]
3. non_recursive : [start/2]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into le/3
1. SCC is partially evaluated into d/2
2. SCC is completely evaluated into other SCCs
3. SCC is partially evaluated into start/2
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations le/3
* CE 11 is refined into CE [12]
* CE 10 is refined into CE [13]
* CE 9 is refined into CE [14]
### Cost equations --> "Loop" of le/3
* CEs [13] --> Loop 7
* CEs [14] --> Loop 8
* CEs [12] --> Loop 9
### Ranking functions of CR le(V,V2,Out)
* RF of phase [9]: [V,V2]
#### Partial ranking functions of CR le(V,V2,Out)
* Partial RF of phase [9]:
- RF of loop [9:1]:
V
V2
### Specialization of cost equations d/2
* CE 8 is refined into CE [15,16]
* CE 7 is refined into CE [17]
### Cost equations --> "Loop" of d/2
* CEs [17] --> Loop 10
* CEs [16] --> Loop 11
* CEs [15] --> Loop 12
### Ranking functions of CR d(V,Out)
* RF of phase [11]: [-V+10]
#### Partial ranking functions of CR d(V,Out)
* Partial RF of phase [11]:
- RF of loop [11:1]:
-V+10
### Specialization of cost equations start/2
* CE 2 is refined into CE [18]
* CE 3 is refined into CE [19,20]
* CE 4 is refined into CE [21]
* CE 5 is refined into CE [22,23,24]
* CE 6 is refined into CE [25,26,27,28]
### Cost equations --> "Loop" of start/2
* CEs [18,19,20,21,22,23,24,25,26,27,28] --> Loop 13
### Ranking functions of CR start(V,V2)
#### Partial ranking functions of CR start(V,V2)
Computing Bounds
=====================================
#### Cost of chains of le(V,V2,Out):
* Chain [[9],8]: 1*it(9)+1
Such that:it(9) =< V
with precondition: [Out=1,V>=1,V2>=V]
* Chain [[9],7]: 1*it(9)+1
Such that:it(9) =< V2
with precondition: [Out=0,V2>=1,V>=V2+1]
* Chain [8]: 1
with precondition: [V=0,Out=1,V2>=0]
* Chain [7]: 1
with precondition: [V2=0,Out=0,V>=1]
#### Cost of chains of d(V,Out):
* Chain [[11],10]: 3*it(11)+1*s(1)+1*s(4)+3
Such that:s(1) =< 9
s(4) =< -9*V+90
it(11) =< -V+10
with precondition: [9>=V,V>=1]
* Chain [12,[11],10]: 4*it(11)+1*s(4)+6
Such that:s(4) =< 81
aux(1) =< 9
it(11) =< aux(1)
with precondition: [V=0]
* Chain [10]: 1*s(1)+3
Such that:s(1) =< 9
with precondition: [Out=0,V>=10]
#### Cost of chains of start(V,V2):
* Chain [13]: 12*s(5)+1*s(7)+3*s(8)+2*s(9)+1*s(17)+3*s(18)+1*s(19)+1*s(20)+7
Such that:s(17) =< -9*V+90
s(18) =< -V+10
s(20) =< V
s(7) =< -9*V2+81
s(8) =< -V2+9
s(19) =< V2
aux(2) =< 9
aux(3) =< 81
s(5) =< aux(2)
s(9) =< aux(3)
with precondition: []
Closed-form bounds of start(V,V2):
-------------------------------------
* Chain [13] with precondition: []
- Upper bound: nat(V)+277+nat(V2)+nat(-V+10)*3+nat(-V2+9)*3+nat(-9*V+90)+nat(-9*V2+81)
- Complexity: n
### Maximum cost of start(V,V2): nat(V)+277+nat(V2)+nat(-V+10)*3+nat(-V2+9)*3+nat(-9*V+90)+nat(-9*V2+81)
Asymptotic class: n
* Total analysis performed in 140 ms.