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), 5 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 1411 ms)
↳10 BOUNDS(1, n^2)
fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) → process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(self, nil), store)), m)
fstsplit(0, x) → nil [1]
fstsplit(s(n), nil) → nil [1]
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t)) [1]
sndsplit(0, x) → x [1]
sndsplit(s(n), nil) → nil [1]
sndsplit(s(n), cons(h, t)) → sndsplit(n, t) [1]
empty(nil) → true [1]
empty(cons(h, t)) → false [1]
leq(0, m) → true [1]
leq(s(n), 0) → false [1]
leq(s(n), s(m)) → leq(n, m) [1]
length(nil) → 0 [1]
length(cons(h, t)) → s(length(t)) [1]
app(nil, x) → x [1]
app(cons(h, t), x) → cons(h, app(t, x)) [1]
map_f(pid, nil) → nil [1]
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t)) [1]
process(store, m) → if1(store, m, leq(m, length(store))) [1]
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store))) [1]
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store)))) [1]
if2(store, m, false) → process(app(map_f(self, nil), sndsplit(m, store)), m) [1]
if3(store, m, false) → process(sndsplit(m, app(map_f(self, nil), store)), m) [1]
fstsplit(0, x) → nil [1]
fstsplit(s(n), nil) → nil [1]
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t)) [1]
sndsplit(0, x) → x [1]
sndsplit(s(n), nil) → nil [1]
sndsplit(s(n), cons(h, t)) → sndsplit(n, t) [1]
empty(nil) → true [1]
empty(cons(h, t)) → false [1]
leq(0, m) → true [1]
leq(s(n), 0) → false [1]
leq(s(n), s(m)) → leq(n, m) [1]
length(nil) → 0 [1]
length(cons(h, t)) → s(length(t)) [1]
app(nil, x) → x [1]
app(cons(h, t), x) → cons(h, app(t, x)) [1]
map_f(pid, nil) → nil [1]
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t)) [1]
process(store, m) → if1(store, m, leq(m, length(store))) [1]
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store))) [1]
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store)))) [1]
if2(store, m, false) → process(app(map_f(self, nil), sndsplit(m, store)), m) [1]
if3(store, m, false) → process(sndsplit(m, app(map_f(self, nil), store)), m) [1]
| fstsplit :: 0:s → nil:cons:f → nil:cons:f 0 :: 0:s nil :: nil:cons:f s :: 0:s → 0:s cons :: a → nil:cons:f → nil:cons:f sndsplit :: 0:s → nil:cons:f → nil:cons:f empty :: nil:cons:f → true:false true :: true:false false :: true:false leq :: 0:s → 0:s → true:false length :: nil:cons:f → 0:s app :: nil:cons:f → nil:cons:f → nil:cons:f map_f :: self → nil:cons:f → nil:cons:f f :: self → a → nil:cons:f process :: nil:cons:f → 0:s → process:if1:if2:if3 if1 :: nil:cons:f → 0:s → true:false → process:if1:if2:if3 if2 :: nil:cons:f → 0:s → true:false → process:if1:if2:if3 if3 :: nil:cons:f → 0:s → true:false → process:if1:if2:if3 self :: self |
fstsplit(v0, v1) → null_fstsplit [0]
sndsplit(v0, v1) → null_sndsplit [0]
empty(v0) → null_empty [0]
length(v0) → null_length [0]
app(v0, v1) → null_app [0]
map_f(v0, v1) → null_map_f [0]
if2(v0, v1, v2) → null_if2 [0]
if3(v0, v1, v2) → null_if3 [0]
leq(v0, v1) → null_leq [0]
if1(v0, v1, v2) → null_if1 [0]
null_fstsplit, null_sndsplit, null_empty, null_length, null_app, null_map_f, null_if2, null_if3, null_leq, null_if1, const
| 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
nil => 0
true => 2
false => 1
self => 0
null_fstsplit => 0
null_sndsplit => 0
null_empty => 0
null_length => 0
null_app => 0
null_map_f => 0
null_if2 => 0
null_if3 => 0
null_leq => 0
null_if1 => 0
const => 0
app(z, z') -{ 1 }→ x :|: z' = x, x >= 0, z = 0
app(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
app(z, z') -{ 1 }→ 1 + h + app(t, x) :|: z = 1 + h + t, z' = x, x >= 0, h >= 0, t >= 0
empty(z) -{ 1 }→ 2 :|: z = 0
empty(z) -{ 1 }→ 1 :|: z = 1 + h + t, h >= 0, t >= 0
empty(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
fstsplit(z, z') -{ 1 }→ 0 :|: z' = x, x >= 0, z = 0
fstsplit(z, z') -{ 1 }→ 0 :|: n >= 0, z = 1 + n, z' = 0
fstsplit(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
fstsplit(z, z') -{ 1 }→ 1 + h + fstsplit(n, t) :|: z' = 1 + h + t, n >= 0, h >= 0, t >= 0, z = 1 + n
if1(z, z', z'') -{ 1 }→ if3(store, m, empty(fstsplit(m, app(map_f(0, 0), store)))) :|: z = store, z' = m, store >= 0, z'' = 1, m >= 0
if1(z, z', z'') -{ 1 }→ if2(store, m, empty(fstsplit(m, store))) :|: z = store, z' = m, z'' = 2, store >= 0, m >= 0
if1(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
if2(z, z', z'') -{ 1 }→ process(app(map_f(0, 0), sndsplit(m, store)), m) :|: z = store, z' = m, store >= 0, z'' = 1, m >= 0
if2(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
if3(z, z', z'') -{ 1 }→ process(sndsplit(m, app(map_f(0, 0), store)), m) :|: z = store, z' = m, store >= 0, z'' = 1, m >= 0
if3(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
length(z) -{ 1 }→ 1 + length(t) :|: z = 1 + h + t, h >= 0, t >= 0
leq(z, z') -{ 1 }→ leq(n, m) :|: n >= 0, z' = 1 + m, z = 1 + n, m >= 0
leq(z, z') -{ 1 }→ 2 :|: z' = m, z = 0, m >= 0
leq(z, z') -{ 1 }→ 1 :|: n >= 0, z = 1 + n, z' = 0
leq(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
map_f(z, z') -{ 1 }→ app(1 + pid + h, map_f(pid, t)) :|: z' = 1 + h + t, z = pid, h >= 0, t >= 0, pid >= 0
map_f(z, z') -{ 1 }→ 0 :|: z = pid, pid >= 0, z' = 0
map_f(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
process(z, z') -{ 1 }→ if1(store, m, leq(m, length(store))) :|: z = store, z' = m, store >= 0, m >= 0
sndsplit(z, z') -{ 1 }→ x :|: z' = x, x >= 0, z = 0
sndsplit(z, z') -{ 1 }→ sndsplit(n, t) :|: z' = 1 + h + t, n >= 0, h >= 0, t >= 0, z = 1 + n
sndsplit(z, z') -{ 1 }→ 0 :|: n >= 0, z = 1 + n, z' = 0
sndsplit(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
| eq(start(V, V1, V30),0,[fstsplit(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V30),0,[sndsplit(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V30),0,[empty(V, Out)],[V >= 0]). eq(start(V, V1, V30),0,[leq(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V30),0,[length(V, Out)],[V >= 0]). eq(start(V, V1, V30),0,[app(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V30),0,[fun(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V30),0,[process(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V30),0,[if1(V, V1, V30, Out)],[V >= 0,V1 >= 0,V30 >= 0]). eq(start(V, V1, V30),0,[if2(V, V1, V30, Out)],[V >= 0,V1 >= 0,V30 >= 0]). eq(start(V, V1, V30),0,[if3(V, V1, V30, Out)],[V >= 0,V1 >= 0,V30 >= 0]). eq(fstsplit(V, V1, Out),1,[],[Out = 0,V1 = V2,V2 >= 0,V = 0]). eq(fstsplit(V, V1, Out),1,[],[Out = 0,V3 >= 0,V = 1 + V3,V1 = 0]). eq(fstsplit(V, V1, Out),1,[fstsplit(V5, V6, Ret1)],[Out = 1 + Ret1 + V4,V1 = 1 + V4 + V6,V5 >= 0,V4 >= 0,V6 >= 0,V = 1 + V5]). eq(sndsplit(V, V1, Out),1,[],[Out = V7,V1 = V7,V7 >= 0,V = 0]). eq(sndsplit(V, V1, Out),1,[],[Out = 0,V8 >= 0,V = 1 + V8,V1 = 0]). eq(sndsplit(V, V1, Out),1,[sndsplit(V9, V10, Ret)],[Out = Ret,V1 = 1 + V10 + V11,V9 >= 0,V11 >= 0,V10 >= 0,V = 1 + V9]). eq(empty(V, Out),1,[],[Out = 2,V = 0]). eq(empty(V, Out),1,[],[Out = 1,V = 1 + V12 + V13,V12 >= 0,V13 >= 0]). eq(leq(V, V1, Out),1,[],[Out = 2,V1 = V14,V = 0,V14 >= 0]). eq(leq(V, V1, Out),1,[],[Out = 1,V15 >= 0,V = 1 + V15,V1 = 0]). eq(leq(V, V1, Out),1,[leq(V16, V17, Ret2)],[Out = Ret2,V16 >= 0,V1 = 1 + V17,V = 1 + V16,V17 >= 0]). eq(length(V, Out),1,[],[Out = 0,V = 0]). eq(length(V, Out),1,[length(V18, Ret11)],[Out = 1 + Ret11,V = 1 + V18 + V19,V19 >= 0,V18 >= 0]). eq(app(V, V1, Out),1,[],[Out = V20,V1 = V20,V20 >= 0,V = 0]). eq(app(V, V1, Out),1,[app(V22, V23, Ret12)],[Out = 1 + Ret12 + V21,V = 1 + V21 + V22,V1 = V23,V23 >= 0,V21 >= 0,V22 >= 0]). eq(fun(V, V1, Out),1,[],[Out = 0,V = V24,V24 >= 0,V1 = 0]). eq(fun(V, V1, Out),1,[fun(V25, V27, Ret13),app(1 + V25 + V26, Ret13, Ret3)],[Out = Ret3,V1 = 1 + V26 + V27,V = V25,V26 >= 0,V27 >= 0,V25 >= 0]). eq(process(V, V1, Out),1,[length(V28, Ret21),leq(V29, Ret21, Ret22),if1(V28, V29, Ret22, Ret4)],[Out = Ret4,V = V28,V1 = V29,V28 >= 0,V29 >= 0]). eq(if1(V, V1, V30, Out),1,[fstsplit(V32, V31, Ret20),empty(Ret20, Ret23),if2(V31, V32, Ret23, Ret5)],[Out = Ret5,V = V31,V1 = V32,V30 = 2,V31 >= 0,V32 >= 0]). eq(if1(V, V1, V30, Out),1,[fun(0, 0, Ret2010),app(Ret2010, V33, Ret201),fstsplit(V34, Ret201, Ret202),empty(Ret202, Ret24),if3(V33, V34, Ret24, Ret6)],[Out = Ret6,V = V33,V1 = V34,V33 >= 0,V30 = 1,V34 >= 0]). eq(if2(V, V1, V30, Out),1,[fun(0, 0, Ret00),sndsplit(V35, V36, Ret01),app(Ret00, Ret01, Ret0),process(Ret0, V35, Ret7)],[Out = Ret7,V = V36,V1 = V35,V36 >= 0,V30 = 1,V35 >= 0]). eq(if3(V, V1, V30, Out),1,[fun(0, 0, Ret010),app(Ret010, V38, Ret011),sndsplit(V37, Ret011, Ret02),process(Ret02, V37, Ret8)],[Out = Ret8,V = V38,V1 = V37,V38 >= 0,V30 = 1,V37 >= 0]). eq(fstsplit(V, V1, Out),0,[],[Out = 0,V39 >= 0,V40 >= 0,V = V39,V1 = V40]). eq(sndsplit(V, V1, Out),0,[],[Out = 0,V41 >= 0,V42 >= 0,V = V41,V1 = V42]). eq(empty(V, Out),0,[],[Out = 0,V43 >= 0,V = V43]). eq(length(V, Out),0,[],[Out = 0,V44 >= 0,V = V44]). eq(app(V, V1, Out),0,[],[Out = 0,V45 >= 0,V46 >= 0,V = V45,V1 = V46]). eq(fun(V, V1, Out),0,[],[Out = 0,V47 >= 0,V48 >= 0,V = V47,V1 = V48]). eq(if2(V, V1, V30, Out),0,[],[Out = 0,V49 >= 0,V30 = V50,V51 >= 0,V = V49,V1 = V51,V50 >= 0]). eq(if3(V, V1, V30, Out),0,[],[Out = 0,V52 >= 0,V30 = V53,V54 >= 0,V = V52,V1 = V54,V53 >= 0]). eq(leq(V, V1, Out),0,[],[Out = 0,V55 >= 0,V56 >= 0,V = V55,V1 = V56]). eq(if1(V, V1, V30, Out),0,[],[Out = 0,V57 >= 0,V30 = V58,V59 >= 0,V = V57,V1 = V59,V58 >= 0]). input_output_vars(fstsplit(V,V1,Out),[V,V1],[Out]). input_output_vars(sndsplit(V,V1,Out),[V,V1],[Out]). input_output_vars(empty(V,Out),[V],[Out]). input_output_vars(leq(V,V1,Out),[V,V1],[Out]). input_output_vars(length(V,Out),[V],[Out]). input_output_vars(app(V,V1,Out),[V,V1],[Out]). input_output_vars(fun(V,V1,Out),[V,V1],[Out]). input_output_vars(process(V,V1,Out),[V,V1],[Out]). input_output_vars(if1(V,V1,V30,Out),[V,V1,V30],[Out]). input_output_vars(if2(V,V1,V30,Out),[V,V1,V30],[Out]). input_output_vars(if3(V,V1,V30,Out),[V,V1,V30],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [app/3]
1. non_recursive : [empty/2]
2. recursive : [fstsplit/3]
3. recursive [non_tail] : [fun/3]
4. recursive : [length/2]
5. recursive : [leq/3]
6. recursive : [sndsplit/3]
7. recursive : [if1/4,if2/4,if3/4,process/3]
8. non_recursive : [start/3]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into app/3
1. SCC is partially evaluated into empty/2
2. SCC is partially evaluated into fstsplit/3
3. SCC is partially evaluated into fun/3
4. SCC is partially evaluated into length/2
5. SCC is partially evaluated into leq/3
6. SCC is partially evaluated into sndsplit/3
7. SCC is partially evaluated into process/3
8. SCC is partially evaluated into start/3
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations app/3
* CE 22 is refined into CE [46]
* CE 20 is refined into CE [47]
* CE 21 is refined into CE [48]
### Cost equations --> "Loop" of app/3
* CEs [48] --> Loop 25
* CEs [46] --> Loop 26
* CEs [47] --> Loop 27
### Ranking functions of CR app(V,V1,Out)
* RF of phase [25]: [V]
#### Partial ranking functions of CR app(V,V1,Out)
* Partial RF of phase [25]:
- RF of loop [25:1]:
V
### Specialization of cost equations empty/2
* CE 28 is refined into CE [49]
* CE 29 is refined into CE [50]
* CE 27 is refined into CE [51]
### Cost equations --> "Loop" of empty/2
* CEs [49] --> Loop 28
* CEs [50] --> Loop 29
* CEs [51] --> Loop 30
### Ranking functions of CR empty(V,Out)
#### Partial ranking functions of CR empty(V,Out)
### Specialization of cost equations fstsplit/3
* CE 24 is refined into CE [52]
* CE 23 is refined into CE [53]
* CE 26 is refined into CE [54]
* CE 25 is refined into CE [55]
### Cost equations --> "Loop" of fstsplit/3
* CEs [55] --> Loop 31
* CEs [52] --> Loop 32
* CEs [53,54] --> Loop 33
### Ranking functions of CR fstsplit(V,V1,Out)
* RF of phase [31]: [V,V1]
#### Partial ranking functions of CR fstsplit(V,V1,Out)
* Partial RF of phase [31]:
- RF of loop [31:1]:
V
V1
### Specialization of cost equations fun/3
* CE 17 is refined into CE [56]
* CE 19 is refined into CE [57]
* CE 18 is refined into CE [58,59,60]
### Cost equations --> "Loop" of fun/3
* CEs [59] --> Loop 34
* CEs [60] --> Loop 35
* CEs [58] --> Loop 36
* CEs [56,57] --> Loop 37
### Ranking functions of CR fun(V,V1,Out)
* RF of phase [34,35,36]: [V1]
#### Partial ranking functions of CR fun(V,V1,Out)
* Partial RF of phase [34,35,36]:
- RF of loop [34:1,35:1,36:1]:
V1
### Specialization of cost equations length/2
* CE 43 is refined into CE [61]
* CE 45 is refined into CE [62]
* CE 44 is refined into CE [63]
### Cost equations --> "Loop" of length/2
* CEs [63] --> Loop 38
* CEs [61,62] --> Loop 39
### Ranking functions of CR length(V,Out)
* RF of phase [38]: [V]
#### Partial ranking functions of CR length(V,Out)
* Partial RF of phase [38]:
- RF of loop [38:1]:
V
### Specialization of cost equations leq/3
* CE 42 is refined into CE [64]
* CE 40 is refined into CE [65]
* CE 39 is refined into CE [66]
* CE 41 is refined into CE [67]
### Cost equations --> "Loop" of leq/3
* CEs [67] --> Loop 40
* CEs [64] --> Loop 41
* CEs [65] --> Loop 42
* CEs [66] --> Loop 43
### Ranking functions of CR leq(V,V1,Out)
* RF of phase [40]: [V,V1]
#### Partial ranking functions of CR leq(V,V1,Out)
* Partial RF of phase [40]:
- RF of loop [40:1]:
V
V1
### Specialization of cost equations sndsplit/3
* CE 31 is refined into CE [68]
* CE 33 is refined into CE [69]
* CE 30 is refined into CE [70]
* CE 32 is refined into CE [71]
### Cost equations --> "Loop" of sndsplit/3
* CEs [71] --> Loop 44
* CEs [68,69] --> Loop 45
* CEs [70] --> Loop 46
### Ranking functions of CR sndsplit(V,V1,Out)
* RF of phase [44]: [V,V1]
#### Partial ranking functions of CR sndsplit(V,V1,Out)
* Partial RF of phase [44]:
- RF of loop [44:1]:
V
V1
### Specialization of cost equations process/3
* CE 34 is refined into CE [72,73,74,75,76,77,78]
* CE 36 is refined into CE [79,80,81,82,83,84,85,86,87,88,89,90]
* CE 38 is refined into CE [91,92,93,94,95,96,97,98]
* CE 35 is refined into CE [99,100,101,102,103,104]
* CE 37 is refined into CE [105,106,107,108]
### Cost equations --> "Loop" of process/3
* CEs [100,103,107] --> Loop 47
* CEs [99,101,102,104,105,106,108] --> Loop 48
* CEs [72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98] --> Loop 49
### Ranking functions of CR process(V,V1,Out)
* RF of phase [47]: [V,V-V1+1]
#### Partial ranking functions of CR process(V,V1,Out)
* Partial RF of phase [47]:
- RF of loop [47:1]:
V
V-V1+1
### Specialization of cost equations start/3
* CE 5 is refined into CE [109,110,111,112]
* CE 6 is refined into CE [113,114,115,116]
* CE 2 is refined into CE [117]
* CE 3 is refined into CE [118,119,120]
* CE 4 is refined into CE [121,122,123,124,125,126]
* CE 7 is refined into CE [127,128,129,130,131,132]
* CE 8 is refined into CE [133,134,135,136,137]
* CE 9 is refined into CE [138,139]
* CE 10 is refined into CE [140,141,142]
* CE 11 is refined into CE [143,144,145]
* CE 12 is refined into CE [146,147,148,149,150]
* CE 13 is refined into CE [151,152]
* CE 14 is refined into CE [153,154,155,156]
* CE 15 is refined into CE [157,158]
* CE 16 is refined into CE [159]
### Cost equations --> "Loop" of start/3
* CEs [109,110,111,112,113,114,115,116] --> Loop 50
* CEs [147] --> Loop 51
* CEs [118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137] --> Loop 52
* CEs [117,138,139,140,141,142,143,144,145,146,148,149,150,151,152,153,154,155,156,157,158,159] --> Loop 53
### Ranking functions of CR start(V,V1,V30)
#### Partial ranking functions of CR start(V,V1,V30)
Computing Bounds
=====================================
#### Cost of chains of app(V,V1,Out):
* Chain [[25],27]: 1*it(25)+1
Such that:it(25) =< -V1+Out
with precondition: [V+V1=Out,V>=1,V1>=0]
* Chain [[25],26]: 1*it(25)+0
Such that:it(25) =< Out
with precondition: [V1>=0,Out>=1,V>=Out]
* Chain [27]: 1
with precondition: [V=0,V1=Out,V1>=0]
* Chain [26]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of empty(V,Out):
* Chain [30]: 1
with precondition: [V=0,Out=2]
* Chain [29]: 0
with precondition: [Out=0,V>=0]
* Chain [28]: 1
with precondition: [Out=1,V>=1]
#### Cost of chains of fstsplit(V,V1,Out):
* Chain [[31],33]: 1*it(31)+1
Such that:it(31) =< V
with precondition: [V>=1,Out>=1,V1>=Out]
* Chain [[31],32]: 1*it(31)+1
Such that:it(31) =< V
with precondition: [V1=Out,V>=2,V1>=1]
* Chain [33]: 1
with precondition: [Out=0,V>=0,V1>=0]
* Chain [32]: 1
with precondition: [V1=0,Out=0,V>=1]
#### Cost of chains of fun(V,V1,Out):
* Chain [[34,35,36],37]: 4*it(34)+1*s(7)+1*s(8)+1
Such that:aux(2) =< V+V1
aux(6) =< V1
it(34) =< aux(6)
aux(3) =< aux(2)
s(7) =< it(34)*aux(2)
s(8) =< it(34)*aux(3)
with precondition: [V>=0,V1>=1,Out>=0]
* Chain [37]: 1
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of length(V,Out):
* Chain [[38],39]: 1*it(38)+1
Such that:it(38) =< V
with precondition: [Out>=1,V>=Out]
* Chain [39]: 1
with precondition: [Out=0,V>=0]
#### Cost of chains of leq(V,V1,Out):
* Chain [[40],43]: 1*it(40)+1
Such that:it(40) =< V
with precondition: [Out=2,V>=1,V1>=V]
* Chain [[40],42]: 1*it(40)+1
Such that:it(40) =< V1
with precondition: [Out=1,V1>=1,V>=V1+1]
* Chain [[40],41]: 1*it(40)+0
Such that:it(40) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [43]: 1
with precondition: [V=0,Out=2,V1>=0]
* Chain [42]: 1
with precondition: [V1=0,Out=1,V>=1]
* Chain [41]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of sndsplit(V,V1,Out):
* Chain [[44],46]: 1*it(44)+1
Such that:it(44) =< V
with precondition: [V>=1,Out>=0,V1>=Out+V]
* Chain [[44],45]: 1*it(44)+1
Such that:it(44) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [46]: 1
with precondition: [V=0,V1=Out,V1>=0]
* Chain [45]: 1
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of process(V,V1,Out):
* Chain [[47],49]: 45*it(47)+19*s(18)+2*s(71)+8
Such that:aux(18) =< V1
aux(27) =< V
it(47) =< aux(27)
s(18) =< aux(18)
s(73) =< it(47)*aux(27)
s(71) =< s(73)
with precondition: [Out=0,V1>=1,V>=V1]
* Chain [[47],48,49]: 34*it(47)+37*s(18)+2*s(71)+20
Such that:aux(37) =< V1
aux(38) =< V
it(47) =< aux(38)
s(18) =< aux(37)
s(73) =< it(47)*aux(38)
s(71) =< s(73)
with precondition: [Out=0,V1>=1,V>=V1+1]
* Chain [49]: 22*s(12)+19*s(18)+8
Such that:aux(17) =< V
aux(18) =< V1
s(12) =< aux(17)
s(18) =< aux(18)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [48,49]: 37*s(18)+11*s(76)+20
Such that:aux(35) =< V
aux(37) =< V1
s(18) =< aux(37)
s(76) =< aux(35)
with precondition: [Out=0,V>=1,V1>=1]
#### Cost of chains of start(V,V1,V30):
* Chain [53]: 119*s(126)+119*s(127)+1*s(139)+1*s(140)+4*s(146)+20
Such that:s(135) =< V+V1
aux(41) =< V
aux(42) =< V1
s(126) =< aux(41)
s(127) =< aux(42)
s(145) =< s(126)*aux(41)
s(146) =< s(145)
s(138) =< s(135)
s(139) =< s(127)*s(135)
s(140) =< s(127)*s(138)
with precondition: [V>=0]
* Chain [52]: 1134*s(148)+228*s(149)+336*s(162)+12*s(164)+8*s(183)+29
Such that:aux(53) =< V
aux(54) =< V-V1
aux(55) =< V1
s(149) =< aux(53)
s(148) =< aux(55)
s(182) =< s(149)*aux(53)
s(183) =< s(182)
s(162) =< aux(54)
s(163) =< s(162)*aux(54)
s(164) =< s(163)
with precondition: [V30=1,V>=0,V1>=0]
* Chain [51]: 1
with precondition: [V1=0,V>=1]
* Chain [50]: 462*s(252)+2*s(253)+112*s(275)+4*s(277)+27
Such that:s(272) =< V-V1
aux(60) =< V
aux(61) =< V1
s(253) =< aux(60)
s(252) =< aux(61)
s(275) =< s(272)
s(276) =< s(275)*s(272)
s(277) =< s(276)
with precondition: [V30=2,V>=0,V1>=0]
Closed-form bounds of start(V,V1,V30):
-------------------------------------
* Chain [53] with precondition: [V>=0]
- Upper bound: 119*V+20+4*V*V+nat(V1)*119+nat(V+V1)*2*nat(V1)
- Complexity: n^2
* Chain [52] with precondition: [V30=1,V>=0,V1>=0]
- Upper bound: 228*V+29+8*V*V+1134*V1+nat(V-V1)*336+nat(V-V1)*12*nat(V-V1)
- Complexity: n^2
* Chain [51] with precondition: [V1=0,V>=1]
- Upper bound: 1
- Complexity: constant
* Chain [50] with precondition: [V30=2,V>=0,V1>=0]
- Upper bound: 2*V+462*V1+27+nat(V-V1)*112+nat(V-V1)*4*nat(V-V1)
- Complexity: n^2
### Maximum cost of start(V,V1,V30): 2*V+19+nat(V1)*119+max([4*V*V+117*V+max([nat(V+V1)*2*nat(V1),109*V+9+4*V*V+nat(V1)*1015+nat(V-V1)*336+nat(V-V1)*12*nat(V-V1)]),nat(V1)*343+7+nat(V-V1)*112+nat(V-V1)*4*nat(V-V1)])+1
Asymptotic class: n^2
* Total analysis performed in 1216 ms.