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), 17 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 1968 ms)
↳10 BOUNDS(1, n^3)
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gcd(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → gcd(y, x)
if2(true, x, y) → gcd(minus(x, y), y)
if2(false, x, y) → x
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x), y) → if(gt(s(x), y), x, y) [1]
if(true, x, y) → s(minus(x, y)) [1]
if(false, x, y) → 0 [1]
gcd(x, y) → if1(ge(x, y), x, y) [1]
if1(true, x, y) → if2(gt(y, 0), x, y) [1]
if1(false, x, y) → gcd(y, x) [1]
if2(true, x, y) → gcd(minus(x, y), y) [1]
if2(false, x, y) → x [1]
gt(0, y) → false [1]
gt(s(x), 0) → true [1]
gt(s(x), s(y)) → gt(x, y) [1]
ge(x, 0) → true [1]
ge(0, s(x)) → false [1]
ge(s(x), s(y)) → ge(x, y) [1]
minus(s(x), y) → if(gt(s(x), y), x, y) [1]
if(true, x, y) → s(minus(x, y)) [1]
if(false, x, y) → 0 [1]
gcd(x, y) → if1(ge(x, y), x, y) [1]
if1(true, x, y) → if2(gt(y, 0), x, y) [1]
if1(false, x, y) → gcd(y, x) [1]
if2(true, x, y) → gcd(minus(x, y), y) [1]
if2(false, x, y) → x [1]
gt(0, y) → false [1]
gt(s(x), 0) → true [1]
gt(s(x), s(y)) → gt(x, y) [1]
ge(x, 0) → true [1]
ge(0, s(x)) → false [1]
ge(s(x), s(y)) → ge(x, y) [1]
| minus :: s:0 → s:0 → s:0 s :: s:0 → s:0 if :: true:false → s:0 → s:0 → s:0 gt :: s:0 → s:0 → true:false true :: true:false false :: true:false 0 :: s:0 gcd :: s:0 → s:0 → s:0 if1 :: true:false → s:0 → s:0 → s:0 ge :: s:0 → s:0 → true:false if2 :: true:false → s:0 → s:0 → s:0 |
minus(v0, v1) → null_minus [0]
gt(v0, v1) → null_gt [0]
ge(v0, v1) → null_ge [0]
if(v0, v1, v2) → null_if [0]
if1(v0, v1, v2) → null_if1 [0]
if2(v0, v1, v2) → null_if2 [0]
null_minus, null_gt, null_ge, null_if, null_if1, null_if2
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
true => 2
false => 1
0 => 0
null_minus => 0
null_gt => 0
null_ge => 0
null_if => 0
null_if1 => 0
null_if2 => 0
gcd(z, z') -{ 1 }→ if1(ge(x, y), x, y) :|: x >= 0, y >= 0, z = x, z' = y
ge(z, z') -{ 1 }→ ge(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
ge(z, z') -{ 1 }→ 2 :|: x >= 0, z = x, z' = 0
ge(z, z') -{ 1 }→ 1 :|: z' = 1 + x, x >= 0, z = 0
ge(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
gt(z, z') -{ 1 }→ gt(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
gt(z, z') -{ 1 }→ 2 :|: x >= 0, z = 1 + x, z' = 0
gt(z, z') -{ 1 }→ 1 :|: y >= 0, z = 0, z' = y
gt(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
if(z, z', z'') -{ 1 }→ 0 :|: z' = x, z'' = y, z = 1, x >= 0, y >= 0
if(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
if(z, z', z'') -{ 1 }→ 1 + minus(x, y) :|: z = 2, z' = x, z'' = y, x >= 0, y >= 0
if1(z, z', z'') -{ 1 }→ if2(gt(y, 0), x, y) :|: z = 2, z' = x, z'' = y, x >= 0, y >= 0
if1(z, z', z'') -{ 1 }→ gcd(y, x) :|: z' = x, z'' = y, z = 1, x >= 0, y >= 0
if1(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
if2(z, z', z'') -{ 1 }→ x :|: z' = x, z'' = y, z = 1, x >= 0, y >= 0
if2(z, z', z'') -{ 1 }→ gcd(minus(x, y), y) :|: z = 2, z' = x, z'' = y, x >= 0, y >= 0
if2(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
minus(z, z') -{ 1 }→ if(gt(1 + x, y), x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y
minus(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
| eq(start(V, V1, V4),0,[minus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V4),0,[if(V, V1, V4, Out)],[V >= 0,V1 >= 0,V4 >= 0]). eq(start(V, V1, V4),0,[gcd(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V4),0,[if1(V, V1, V4, Out)],[V >= 0,V1 >= 0,V4 >= 0]). eq(start(V, V1, V4),0,[if2(V, V1, V4, Out)],[V >= 0,V1 >= 0,V4 >= 0]). eq(start(V, V1, V4),0,[gt(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V4),0,[ge(V, V1, Out)],[V >= 0,V1 >= 0]). eq(minus(V, V1, Out),1,[gt(1 + V2, V3, Ret0),if(Ret0, V2, V3, Ret)],[Out = Ret,V2 >= 0,V3 >= 0,V = 1 + V2,V1 = V3]). eq(if(V, V1, V4, Out),1,[minus(V5, V6, Ret1)],[Out = 1 + Ret1,V = 2,V1 = V5,V4 = V6,V5 >= 0,V6 >= 0]). eq(if(V, V1, V4, Out),1,[],[Out = 0,V1 = V7,V4 = V8,V = 1,V7 >= 0,V8 >= 0]). eq(gcd(V, V1, Out),1,[ge(V9, V10, Ret01),if1(Ret01, V9, V10, Ret2)],[Out = Ret2,V9 >= 0,V10 >= 0,V = V9,V1 = V10]). eq(if1(V, V1, V4, Out),1,[gt(V11, 0, Ret02),if2(Ret02, V12, V11, Ret3)],[Out = Ret3,V = 2,V1 = V12,V4 = V11,V12 >= 0,V11 >= 0]). eq(if1(V, V1, V4, Out),1,[gcd(V13, V14, Ret4)],[Out = Ret4,V1 = V14,V4 = V13,V = 1,V14 >= 0,V13 >= 0]). eq(if2(V, V1, V4, Out),1,[minus(V15, V16, Ret03),gcd(Ret03, V16, Ret5)],[Out = Ret5,V = 2,V1 = V15,V4 = V16,V15 >= 0,V16 >= 0]). eq(if2(V, V1, V4, Out),1,[],[Out = V17,V1 = V17,V4 = V18,V = 1,V17 >= 0,V18 >= 0]). eq(gt(V, V1, Out),1,[],[Out = 1,V19 >= 0,V = 0,V1 = V19]). eq(gt(V, V1, Out),1,[],[Out = 2,V20 >= 0,V = 1 + V20,V1 = 0]). eq(gt(V, V1, Out),1,[gt(V21, V22, Ret6)],[Out = Ret6,V1 = 1 + V22,V21 >= 0,V22 >= 0,V = 1 + V21]). eq(ge(V, V1, Out),1,[],[Out = 2,V23 >= 0,V = V23,V1 = 0]). eq(ge(V, V1, Out),1,[],[Out = 1,V1 = 1 + V24,V24 >= 0,V = 0]). eq(ge(V, V1, Out),1,[ge(V25, V26, Ret7)],[Out = Ret7,V1 = 1 + V26,V25 >= 0,V26 >= 0,V = 1 + V25]). eq(minus(V, V1, Out),0,[],[Out = 0,V27 >= 0,V28 >= 0,V = V27,V1 = V28]). eq(gt(V, V1, Out),0,[],[Out = 0,V29 >= 0,V30 >= 0,V = V29,V1 = V30]). eq(ge(V, V1, Out),0,[],[Out = 0,V31 >= 0,V32 >= 0,V = V31,V1 = V32]). eq(if(V, V1, V4, Out),0,[],[Out = 0,V33 >= 0,V4 = V34,V35 >= 0,V = V33,V1 = V35,V34 >= 0]). eq(if1(V, V1, V4, Out),0,[],[Out = 0,V36 >= 0,V4 = V37,V38 >= 0,V = V36,V1 = V38,V37 >= 0]). eq(if2(V, V1, V4, Out),0,[],[Out = 0,V39 >= 0,V4 = V40,V41 >= 0,V = V39,V1 = V41,V40 >= 0]). input_output_vars(minus(V,V1,Out),[V,V1],[Out]). input_output_vars(if(V,V1,V4,Out),[V,V1,V4],[Out]). input_output_vars(gcd(V,V1,Out),[V,V1],[Out]). input_output_vars(if1(V,V1,V4,Out),[V,V1,V4],[Out]). input_output_vars(if2(V,V1,V4,Out),[V,V1,V4],[Out]). input_output_vars(gt(V,V1,Out),[V,V1],[Out]). input_output_vars(ge(V,V1,Out),[V,V1],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [ge/3]
1. recursive : [gt/3]
2. recursive : [if/4,minus/3]
3. recursive : [gcd/3,if1/4,if2/4]
4. non_recursive : [start/3]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into ge/3
1. SCC is partially evaluated into gt/3
2. SCC is partially evaluated into minus/3
3. SCC is partially evaluated into gcd/3
4. SCC is partially evaluated into start/3
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations ge/3
* CE 30 is refined into CE [31]
* CE 27 is refined into CE [32]
* CE 28 is refined into CE [33]
* CE 29 is refined into CE [34]
### Cost equations --> "Loop" of ge/3
* CEs [34] --> Loop 17
* CEs [31] --> Loop 18
* CEs [32] --> Loop 19
* CEs [33] --> Loop 20
### Ranking functions of CR ge(V,V1,Out)
* RF of phase [17]: [V,V1]
#### Partial ranking functions of CR ge(V,V1,Out)
* Partial RF of phase [17]:
- RF of loop [17:1]:
V
V1
### Specialization of cost equations gt/3
* CE 17 is refined into CE [35]
* CE 15 is refined into CE [36]
* CE 14 is refined into CE [37]
* CE 16 is refined into CE [38]
### Cost equations --> "Loop" of gt/3
* CEs [38] --> Loop 21
* CEs [35] --> Loop 22
* CEs [36] --> Loop 23
* CEs [37] --> Loop 24
### Ranking functions of CR gt(V,V1,Out)
* RF of phase [21]: [V,V1]
#### Partial ranking functions of CR gt(V,V1,Out)
* Partial RF of phase [21]:
- RF of loop [21:1]:
V
V1
### Specialization of cost equations minus/3
* CE 18 is refined into CE [39,40,41,42]
* CE 19 is refined into CE [43]
* CE 21 is refined into CE [44]
* CE 20 is refined into CE [45,46]
### Cost equations --> "Loop" of minus/3
* CEs [46] --> Loop 25
* CEs [45] --> Loop 26
* CEs [39,40,41,42,43,44] --> Loop 27
### Ranking functions of CR minus(V,V1,Out)
* RF of phase [25]: [V-1,V-V1]
* RF of phase [26]: [V]
#### Partial ranking functions of CR minus(V,V1,Out)
* Partial RF of phase [25]:
- RF of loop [25:1]:
V-1
V-V1
* Partial RF of phase [26]:
- RF of loop [26:1]:
V
### Specialization of cost equations gcd/3
* CE 24 is refined into CE [47,48]
* CE 26 is refined into CE [49,50]
* CE 23 is refined into CE [51]
* CE 22 is refined into CE [52,53,54,55]
* CE 25 is refined into CE [56,57,58,59,60]
### Cost equations --> "Loop" of gcd/3
* CEs [51] --> Loop 28
* CEs [52,53,57] --> Loop 29
* CEs [54,55,56,58,59,60] --> Loop 30
* CEs [48] --> Loop 31
* CEs [50] --> Loop 32
* CEs [47] --> Loop 33
* CEs [49] --> Loop 34
### Ranking functions of CR gcd(V,V1,Out)
* RF of phase [31,32]: [V+2*V1-3]
#### Partial ranking functions of CR gcd(V,V1,Out)
* Partial RF of phase [31,32]:
- RF of loop [31:1]:
V-1 depends on loops [32:1]
V-V1 depends on loops [32:1]
- RF of loop [32:1]:
-V/2+V1/2 depends on loops [31:1]
V1-1
### Specialization of cost equations start/3
* CE 2 is refined into CE [61,62,63]
* CE 4 is refined into CE [64]
* CE 6 is refined into CE [65,66,67,68,69]
* CE 7 is refined into CE [70,71,72,73,74,75,76,77,78,79]
* CE 9 is refined into CE [80,81,82]
* CE 3 is refined into CE [83]
* CE 5 is refined into CE [84]
* CE 8 is refined into CE [85,86,87,88,89,90]
* CE 10 is refined into CE [91,92,93]
* CE 11 is refined into CE [94,95,96,97,98,99]
* CE 12 is refined into CE [100,101,102,103,104]
* CE 13 is refined into CE [105,106,107,108,109]
### Cost equations --> "Loop" of start/3
* CEs [91,96,97,101,106] --> Loop 35
* CEs [61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82] --> Loop 36
* CEs [86] --> Loop 37
* CEs [84,85,87,88,89,90] --> Loop 38
* CEs [83,92,93,94,95,98,99,100,102,103,104,105,107,108,109] --> Loop 39
### Ranking functions of CR start(V,V1,V4)
#### Partial ranking functions of CR start(V,V1,V4)
Computing Bounds
=====================================
#### Cost of chains of ge(V,V1,Out):
* Chain [[17],20]: 1*it(17)+1
Such that:it(17) =< V
with precondition: [Out=1,V>=1,V1>=V+1]
* Chain [[17],19]: 1*it(17)+1
Such that:it(17) =< V1
with precondition: [Out=2,V1>=1,V>=V1]
* Chain [[17],18]: 1*it(17)+0
Such that:it(17) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [20]: 1
with precondition: [V=0,Out=1,V1>=1]
* Chain [19]: 1
with precondition: [V1=0,Out=2,V>=0]
* Chain [18]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of gt(V,V1,Out):
* Chain [[21],24]: 1*it(21)+1
Such that:it(21) =< V
with precondition: [Out=1,V>=1,V1>=V]
* Chain [[21],23]: 1*it(21)+1
Such that:it(21) =< V1
with precondition: [Out=2,V1>=1,V>=V1+1]
* Chain [[21],22]: 1*it(21)+0
Such that:it(21) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [24]: 1
with precondition: [V=0,Out=1,V1>=0]
* Chain [23]: 1
with precondition: [V1=0,Out=2,V>=1]
* Chain [22]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of minus(V,V1,Out):
* Chain [[26],27]: 3*it(26)+2*s(4)+3
Such that:aux(1) =< V-Out
it(26) =< Out
s(4) =< aux(1)
with precondition: [V1=0,Out>=1,V>=Out]
* Chain [[25],27]: 3*it(25)+2*s(3)+2*s(4)+1*s(9)+3
Such that:aux(1) =< V-Out
it(25) =< Out
aux(4) =< V1
s(4) =< aux(1)
s(3) =< aux(4)
s(9) =< it(25)*aux(4)
with precondition: [V1>=1,Out>=1,V>=Out+V1]
* Chain [27]: 2*s(3)+2*s(4)+3
Such that:aux(1) =< V
aux(2) =< V1
s(4) =< aux(1)
s(3) =< aux(2)
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of gcd(V,V1,Out):
* Chain [[31,32],33,34,30]: 8*it(31)+3*it(32)+6*s(14)+3*s(36)+3*s(37)+2*s(38)+1*s(39)+1*s(42)+15
Such that:aux(36) =< -V+V1
aux(12) =< V-V1
aux(25) =< -V/2+V1/2
aux(42) =< V/2+V1/2
aux(45) =< V
aux(46) =< V+V1
aux(47) =< V+2*V1
aux(48) =< V1
it(32) =< aux(48)
s(14) =< aux(47)
it(31) =< aux(47)
it(32) =< aux(47)
aux(24) =< aux(42)
aux(24) =< aux(46)
aux(23) =< aux(48)
aux(26) =< aux(46)+1
aux(27) =< aux(24)*2
it(32) =< aux(24)+aux(25)
aux(9) =< aux(27)+aux(36)
aux(9) =< it(32)*aux(23)
aux(11) =< aux(27)+aux(36)
aux(11) =< it(32)*aux(48)
s(42) =< it(32)*aux(26)
s(41) =< aux(9)+aux(45)
it(31) =< aux(11)+aux(12)
it(31) =< aux(9)+aux(45)
s(40) =< aux(9)+aux(45)
s(41) =< it(31)*aux(23)
s(37) =< it(31)*aux(46)
s(40) =< it(31)*aux(46)
s(36) =< s(41)
s(38) =< s(40)
s(39) =< s(37)*aux(48)
with precondition: [Out=0,V>=1,V1>=1,V+V1>=3]
* Chain [[31,32],33,34,29]: 8*it(31)+3*it(32)+5*s(16)+3*s(36)+3*s(37)+2*s(38)+1*s(39)+1*s(42)+15
Such that:aux(36) =< -V+V1
aux(12) =< V-V1
aux(25) =< -V/2+V1/2
aux(42) =< V/2+V1/2
aux(49) =< V
aux(50) =< V+V1
aux(51) =< V+2*V1
aux(52) =< V1
it(32) =< aux(52)
s(16) =< aux(51)
it(31) =< aux(51)
it(32) =< aux(51)
aux(24) =< aux(42)
aux(24) =< aux(50)
aux(23) =< aux(52)
aux(26) =< aux(50)+1
aux(27) =< aux(24)*2
it(32) =< aux(24)+aux(25)
aux(9) =< aux(27)+aux(36)
aux(9) =< it(32)*aux(23)
aux(11) =< aux(27)+aux(36)
aux(11) =< it(32)*aux(52)
s(42) =< it(32)*aux(26)
s(41) =< aux(9)+aux(49)
it(31) =< aux(11)+aux(12)
it(31) =< aux(9)+aux(49)
s(40) =< aux(9)+aux(49)
s(41) =< it(31)*aux(23)
s(37) =< it(31)*aux(50)
s(40) =< it(31)*aux(50)
s(36) =< s(41)
s(38) =< s(40)
s(39) =< s(37)*aux(52)
with precondition: [Out=0,V>=1,V1>=1,V+V1>=3]
* Chain [[31,32],33,34,28]: 8*it(31)+3*it(32)+3*s(16)+2*s(19)+3*s(36)+3*s(37)+2*s(38)+1*s(39)+1*s(42)+16
Such that:aux(36) =< -V+V1
aux(37) =< V
aux(12) =< V-V1
aux(38) =< V+V1
aux(39) =< V+2*V1
aux(40) =< V+2*V1-2*Out
aux(41) =< V-Out
aux(25) =< -V/2+V1/2
aux(42) =< V/2+V1/2
aux(44) =< V1
it(32) =< V1-Out
aux(6) =< Out
aux(53) =< V+V1-Out
s(16) =< aux(6)
s(19) =< aux(53)
it(31) =< aux(39)
it(32) =< aux(39)
it(31) =< aux(40)
it(32) =< aux(40)
aux(24) =< aux(42)
aux(24) =< aux(53)
it(32) =< aux(44)
aux(23) =< aux(44)
aux(26) =< aux(38)+1
aux(27) =< aux(24)*2
it(32) =< aux(24)+aux(25)
aux(9) =< aux(27)+aux(36)
aux(9) =< it(32)*aux(23)
aux(11) =< aux(27)+aux(36)
aux(11) =< it(32)*aux(44)
s(42) =< it(32)*aux(26)
s(41) =< aux(9)+aux(37)
it(31) =< aux(11)+aux(12)
it(31) =< aux(9)+aux(37)
s(41) =< aux(9)+aux(41)
s(40) =< aux(9)+aux(41)
s(40) =< aux(9)+aux(37)
it(31) =< aux(9)+aux(41)
s(41) =< it(31)*aux(23)
s(37) =< it(31)*aux(38)
s(40) =< it(31)*aux(38)
s(36) =< s(41)
s(38) =< s(40)
s(39) =< s(37)*aux(44)
with precondition: [Out>=1,V>=Out,V1>=Out,V+V1>=2*Out+1]
* Chain [[31,32],33,30]: 8*it(31)+3*it(32)+9*s(10)+3*s(36)+3*s(37)+2*s(38)+1*s(39)+1*s(42)+12
Such that:aux(36) =< -V+V1
aux(12) =< V-V1
aux(25) =< -V/2+V1/2
aux(42) =< V/2+V1/2
aux(55) =< V
aux(56) =< V+V1
aux(57) =< V+2*V1
aux(58) =< V1
it(32) =< aux(58)
s(10) =< aux(56)
it(31) =< aux(57)
it(32) =< aux(57)
aux(24) =< aux(42)
aux(24) =< aux(56)
aux(23) =< aux(58)
aux(26) =< aux(56)+1
aux(27) =< aux(24)*2
it(32) =< aux(24)+aux(25)
aux(9) =< aux(27)+aux(36)
aux(9) =< it(32)*aux(23)
aux(11) =< aux(27)+aux(36)
aux(11) =< it(32)*aux(58)
s(42) =< it(32)*aux(26)
s(41) =< aux(9)+aux(55)
it(31) =< aux(11)+aux(12)
it(31) =< aux(9)+aux(55)
s(40) =< aux(9)+aux(55)
s(41) =< it(31)*aux(23)
s(37) =< it(31)*aux(56)
s(40) =< it(31)*aux(56)
s(36) =< s(41)
s(38) =< s(40)
s(39) =< s(37)*aux(58)
with precondition: [Out=0,V>=1,V1>=1,V+V1>=3]
* Chain [[31,32],30]: 8*it(31)+3*it(32)+5*s(10)+3*s(36)+3*s(37)+2*s(38)+1*s(39)+1*s(42)+4
Such that:aux(36) =< -V+V1
aux(12) =< V-V1
aux(25) =< -V/2+V1/2
aux(42) =< V/2+V1/2
aux(59) =< V
aux(60) =< V+V1
aux(61) =< V+2*V1
aux(62) =< V1
s(10) =< aux(60)
it(32) =< aux(62)
it(31) =< aux(61)
it(32) =< aux(61)
aux(24) =< aux(42)
aux(24) =< aux(60)
aux(23) =< aux(62)
aux(26) =< aux(60)+1
aux(27) =< aux(24)*2
it(32) =< aux(24)+aux(25)
aux(9) =< aux(27)+aux(36)
aux(9) =< it(32)*aux(23)
aux(11) =< aux(27)+aux(36)
aux(11) =< it(32)*aux(62)
s(42) =< it(32)*aux(26)
s(41) =< aux(9)+aux(59)
it(31) =< aux(11)+aux(12)
it(31) =< aux(9)+aux(59)
s(40) =< aux(9)+aux(59)
s(41) =< it(31)*aux(23)
s(37) =< it(31)*aux(60)
s(40) =< it(31)*aux(60)
s(36) =< s(41)
s(38) =< s(40)
s(39) =< s(37)*aux(62)
with precondition: [Out=0,V>=1,V1>=1,V+V1>=3]
* Chain [34,30]: 1*s(14)+7
Such that:s(14) =< V1
with precondition: [V=0,Out=0,V1>=1]
* Chain [34,29]: 7
with precondition: [V=0,Out=0,V1>=1]
* Chain [34,28]: 8
with precondition: [V=0,V1=Out,V1>=1]
* Chain [33,34,30]: 4*s(14)+2*s(19)+15
Such that:s(17) =< V
aux(7) =< V1
s(14) =< aux(7)
s(19) =< s(17)
with precondition: [Out=0,V1>=1,V>=V1]
* Chain [33,34,29]: 3*s(16)+2*s(19)+15
Such that:s(17) =< V
aux(6) =< V1
s(16) =< aux(6)
s(19) =< s(17)
with precondition: [Out=0,V1>=1,V>=V1]
* Chain [33,34,28]: 3*s(16)+2*s(19)+16
Such that:s(17) =< V
aux(6) =< Out
s(16) =< aux(6)
s(19) =< s(17)
with precondition: [V1=Out,V1>=1,V>=V1]
* Chain [33,30]: 7*s(10)+2*s(19)+12
Such that:s(17) =< V
aux(54) =< V1
s(10) =< aux(54)
s(19) =< s(17)
with precondition: [Out=0,V1>=1,V>=V1]
* Chain [30]: 4*s(10)+1*s(14)+4
Such that:s(14) =< V
aux(5) =< V1
s(10) =< aux(5)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [29]: 4
with precondition: [V1=0,Out=0,V>=0]
* Chain [28]: 5
with precondition: [V1=0,V=Out,V>=0]
#### Cost of chains of start(V,V1,V4):
* Chain [39]: 18*s(158)+30*s(159)+1*s(165)+19*s(176)+15*s(177)+40*s(178)+5*s(185)+15*s(188)+15*s(189)+10*s(190)+5*s(191)+11*s(192)+16
Such that:aux(76) =< -V+V1
aux(77) =< V
aux(78) =< V-V1
aux(79) =< V+V1
aux(80) =< V+2*V1
aux(81) =< -V/2+V1/2
aux(82) =< V/2+V1/2
aux(83) =< V1
s(158) =< aux(77)
s(159) =< aux(83)
s(176) =< aux(79)
s(177) =< aux(83)
s(178) =< aux(80)
s(177) =< aux(80)
s(179) =< aux(82)
s(179) =< aux(79)
s(180) =< aux(83)
s(181) =< aux(79)+1
s(182) =< s(179)*2
s(177) =< s(179)+aux(81)
s(183) =< s(182)+aux(76)
s(183) =< s(177)*s(180)
s(184) =< s(182)+aux(76)
s(184) =< s(177)*aux(83)
s(185) =< s(177)*s(181)
s(186) =< s(183)+aux(77)
s(178) =< s(184)+aux(78)
s(178) =< s(183)+aux(77)
s(187) =< s(183)+aux(77)
s(186) =< s(178)*s(180)
s(188) =< s(178)*aux(79)
s(187) =< s(178)*aux(79)
s(189) =< s(186)
s(190) =< s(187)
s(191) =< s(188)*aux(83)
s(192) =< aux(80)
s(165) =< s(158)*aux(83)
with precondition: [V>=0,V1>=0]
* Chain [38]: 9*s(240)+22*s(241)+19*s(242)+15*s(243)+40*s(244)+5*s(251)+15*s(254)+15*s(255)+10*s(256)+5*s(257)+11*s(258)+17
Such that:aux(88) =< -V1+V4
aux(89) =< V1
aux(90) =< V1-V4
aux(91) =< V1+V4
aux(92) =< 2*V1+V4
aux(93) =< V1/2-V4/2
aux(94) =< V1/2+V4/2
aux(95) =< V4
s(240) =< aux(95)
s(241) =< aux(89)
s(242) =< aux(91)
s(243) =< aux(89)
s(244) =< aux(92)
s(243) =< aux(92)
s(245) =< aux(94)
s(245) =< aux(91)
s(246) =< aux(89)
s(247) =< aux(91)+1
s(248) =< s(245)*2
s(243) =< s(245)+aux(93)
s(249) =< s(248)+aux(90)
s(249) =< s(243)*s(246)
s(250) =< s(248)+aux(90)
s(250) =< s(243)*aux(89)
s(251) =< s(243)*s(247)
s(252) =< s(249)+aux(95)
s(244) =< s(250)+aux(88)
s(244) =< s(249)+aux(95)
s(253) =< s(249)+aux(95)
s(252) =< s(244)*s(246)
s(254) =< s(244)*aux(91)
s(253) =< s(244)*aux(91)
s(255) =< s(252)
s(256) =< s(253)
s(257) =< s(254)*aux(89)
s(258) =< aux(92)
with precondition: [V=1,V1>=0,V4>=0]
* Chain [37]: 9
with precondition: [V=1,V4=0,V1>=1]
* Chain [36]: 147*s(295)+134*s(296)+24*s(308)+64*s(309)+8*s(316)+24*s(319)+24*s(320)+16*s(321)+8*s(322)+22*s(323)+7*s(333)+42*s(344)+24*s(345)+64*s(346)+8*s(353)+24*s(356)+24*s(357)+16*s(358)+8*s(359)+22*s(360)+6*s(387)+16*s(392)+2*s(399)+6*s(402)+6*s(403)+4*s(404)+2*s(405)+12*s(431)+8*s(433)+22
Such that:aux(124) =< V1
aux(125) =< V1-2*V4
aux(126) =< V1+V4
aux(127) =< V1+2*V4
aux(128) =< -V4
aux(129) =< V4
aux(130) =< 2*V4
aux(131) =< V4/2
s(295) =< aux(124)
s(296) =< aux(129)
s(333) =< s(295)*aux(129)
s(430) =< aux(124)
s(431) =< s(295)*aux(124)
s(430) =< s(295)*aux(124)
s(433) =< s(430)
s(308) =< aux(129)
s(309) =< aux(130)
s(308) =< aux(130)
s(310) =< aux(131)
s(310) =< aux(129)
s(311) =< aux(129)
s(312) =< aux(129)+1
s(313) =< s(310)*2
s(308) =< s(310)+aux(131)
s(314) =< s(313)+aux(129)
s(314) =< s(308)*s(311)
s(315) =< s(313)+aux(129)
s(315) =< s(308)*aux(129)
s(316) =< s(308)*s(312)
s(317) =< s(314)
s(309) =< s(315)+aux(128)
s(309) =< s(314)
s(318) =< s(314)
s(317) =< s(309)*s(311)
s(319) =< s(309)*aux(129)
s(318) =< s(309)*aux(129)
s(320) =< s(317)
s(321) =< s(318)
s(322) =< s(319)*aux(129)
s(323) =< aux(130)
s(344) =< aux(126)
s(345) =< aux(129)
s(346) =< aux(127)
s(345) =< aux(127)
s(349) =< aux(126)+1
s(350) =< aux(126)*2
s(345) =< aux(126)+aux(131)
s(351) =< s(350)+aux(129)
s(351) =< s(345)*s(311)
s(352) =< s(350)+aux(129)
s(352) =< s(345)*aux(129)
s(353) =< s(345)*s(349)
s(354) =< s(351)+aux(124)
s(346) =< s(352)+aux(125)
s(346) =< s(351)+aux(124)
s(355) =< s(351)+aux(124)
s(354) =< s(346)*s(311)
s(356) =< s(346)*aux(126)
s(355) =< s(346)*aux(126)
s(357) =< s(354)
s(358) =< s(355)
s(359) =< s(356)*aux(129)
s(360) =< aux(127)
s(387) =< aux(129)
s(392) =< aux(127)
s(387) =< aux(127)
s(387) =< aux(126)+aux(129)
s(397) =< s(350)+aux(129)
s(397) =< s(387)*s(311)
s(398) =< s(350)+aux(129)
s(398) =< s(387)*aux(129)
s(399) =< s(387)*s(349)
s(400) =< s(397)+aux(124)
s(392) =< s(398)+aux(125)
s(392) =< s(397)+aux(124)
s(401) =< s(397)+aux(124)
s(400) =< s(392)*s(311)
s(402) =< s(392)*aux(126)
s(401) =< s(392)*aux(126)
s(403) =< s(400)
s(404) =< s(401)
s(405) =< s(402)*aux(129)
with precondition: [V=2,V1>=0,V4>=0]
* Chain [35]: 5*s(577)+5
Such that:aux(132) =< V
s(577) =< aux(132)
with precondition: [V1=0,V>=0]
Closed-form bounds of start(V,V1,V4):
-------------------------------------
* Chain [39] with precondition: [V>=0,V1>=0]
- Upper bound: 43*V+50*V1+16+V1*V+ (V+2*V1)* ((V+V1)* (5*V1))+ (19*V+19*V1)+ (5*V+5*V1)*V1+ (15*V+15*V1)* (V+2*V1)+ (51*V+102*V1)+nat(-V+V1)*25+ (25*V+25*V1)
- Complexity: n^3
* Chain [38] with precondition: [V=1,V1>=0,V4>=0]
- Upper bound: 42*V1+17+ (2*V1+V4)* ((V1+V4)* (5*V1))+34*V4+ (19*V1+19*V4)+ (5*V1+5*V4)*V1+ (15*V1+15*V4)* (2*V1+V4)+ (102*V1+51*V4)+ (25*V1+25*V4)+nat(V1-V4)*25
- Complexity: n^3
* Chain [37] with precondition: [V=1,V4=0,V1>=1]
- Upper bound: 9
- Complexity: constant
* Chain [36] with precondition: [V=2,V1>=0,V4>=0]
- Upper bound: 205*V1+22+12*V1*V1+296*V4+7*V4*V1+8*V4*V4+8*V4*V4* (2*V4)+24*V4* (2*V4)+ (V1+2*V4)* ((V1+V4)* (10*V4))+172*V4+ (142*V1+142*V4)+ (10*V1+10*V4)*V4+ (30*V1+30*V4)* (V1+2*V4)+ (102*V1+204*V4)+40*V4
- Complexity: n^3
* Chain [35] with precondition: [V1=0,V>=0]
- Upper bound: 5*V+5
- Complexity: n
### Maximum cost of start(V,V1,V4): max([max([5*V,4]),42*V1+11+max([8*V1+max([43*V+V1*V+ (V+2*V1)* ((V+V1)* (5*V1))+ (19*V+19*V1)+ (5*V+5*V1)*V1+ (15*V+15*V1)* (V+2*V1)+ (51*V+102*V1)+nat(-V+V1)*25+ (25*V+25*V1),155*V1+6+12*V1*V1+nat(V4)*296+nat(V4)*7*V1+nat(V4)*8*nat(V4)+nat(V4)*8*nat(V4)*nat(2*V4)+nat(V4)*24*nat(2*V4)+nat(V4)*10*nat(V1+V4)*nat(V1+2*V4)+nat(2*V4)*86+nat(V1+V4)*142+nat(V1+V4)*10*nat(V4)+nat(V1+V4)*30*nat(V1+2*V4)+nat(V1+2*V4)*102+nat(V4/2)*80]),5*V1*nat(V1+V4)*nat(2*V1+V4)+1+nat(V4)*34+nat(V1+V4)*19+nat(V1+V4)*5*V1+nat(V1+V4)*15*nat(2*V1+V4)+nat(2*V1+V4)*51+nat(V1/2+V4/2)*50+nat(V1-V4)*25])])+5
Asymptotic class: n^3
* Total analysis performed in 1525 ms.