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), 16 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 9281 ms)
↳10 BOUNDS(1, n^4)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
eq(0, 0) → true [1]
eq(0, s(x)) → false [1]
eq(s(x), 0) → false [1]
eq(s(x), s(y)) → eq(x, y) [1]
le(0, y) → true [1]
le(s(x), 0) → false [1]
le(s(x), s(y)) → le(x, y) [1]
app(nil, y) → y [1]
app(add(n, x), y) → add(n, app(x, y)) [1]
min(add(n, nil)) → n [1]
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x))) [1]
if_min(true, add(n, add(m, x))) → min(add(n, x)) [1]
if_min(false, add(n, add(m, x))) → min(add(m, x)) [1]
rm(n, nil) → nil [1]
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x)) [1]
if_rm(true, n, add(m, x)) → rm(n, x) [1]
if_rm(false, n, add(m, x)) → add(m, rm(n, x)) [1]
minsort(nil, nil) → nil [1]
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y) [1]
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil)) [1]
if_minsort(false, add(n, x), y) → minsort(x, add(n, y)) [1]
eq(0, 0) → true [1]
eq(0, s(x)) → false [1]
eq(s(x), 0) → false [1]
eq(s(x), s(y)) → eq(x, y) [1]
le(0, y) → true [1]
le(s(x), 0) → false [1]
le(s(x), s(y)) → le(x, y) [1]
app(nil, y) → y [1]
app(add(n, x), y) → add(n, app(x, y)) [1]
min(add(n, nil)) → n [1]
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x))) [1]
if_min(true, add(n, add(m, x))) → min(add(n, x)) [1]
if_min(false, add(n, add(m, x))) → min(add(m, x)) [1]
rm(n, nil) → nil [1]
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x)) [1]
if_rm(true, n, add(m, x)) → rm(n, x) [1]
if_rm(false, n, add(m, x)) → add(m, rm(n, x)) [1]
minsort(nil, nil) → nil [1]
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y) [1]
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil)) [1]
if_minsort(false, add(n, x), y) → minsort(x, add(n, y)) [1]
| eq :: 0:s → 0:s → true:false 0 :: 0:s true :: true:false s :: 0:s → 0:s false :: true:false le :: 0:s → 0:s → true:false app :: nil:add → nil:add → nil:add nil :: nil:add add :: 0:s → nil:add → nil:add min :: nil:add → 0:s if_min :: true:false → nil:add → 0:s rm :: 0:s → nil:add → nil:add if_rm :: true:false → 0:s → nil:add → nil:add minsort :: nil:add → nil:add → nil:add if_minsort :: true:false → nil:add → nil:add → nil:add |
min(v0) → null_min [0]
if_min(v0, v1) → null_if_min [0]
if_rm(v0, v1, v2) → null_if_rm [0]
minsort(v0, v1) → null_minsort [0]
if_minsort(v0, v1, v2) → null_if_minsort [0]
eq(v0, v1) → null_eq [0]
le(v0, v1) → null_le [0]
app(v0, v1) → null_app [0]
rm(v0, v1) → null_rm [0]
null_min, null_if_min, null_if_rm, null_minsort, null_if_minsort, null_eq, null_le, null_app, null_rm
| 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 => 2
false => 1
nil => 0
null_min => 0
null_if_min => 0
null_if_rm => 0
null_minsort => 0
null_if_minsort => 0
null_eq => 0
null_le => 0
null_app => 0
null_rm => 0
app(z, z') -{ 1 }→ y :|: y >= 0, z = 0, z' = y
app(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
app(z, z') -{ 1 }→ 1 + n + app(x, y) :|: n >= 0, x >= 0, y >= 0, z = 1 + n + x, z' = y
eq(z, z') -{ 1 }→ eq(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
eq(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 1 :|: z' = 1 + x, x >= 0, z = 0
eq(z, z') -{ 1 }→ 1 :|: x >= 0, z = 1 + x, z' = 0
eq(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
if_min(z, z') -{ 1 }→ min(1 + m + x) :|: n >= 0, z = 1, x >= 0, z' = 1 + n + (1 + m + x), m >= 0
if_min(z, z') -{ 1 }→ min(1 + n + x) :|: z = 2, n >= 0, x >= 0, z' = 1 + n + (1 + m + x), m >= 0
if_min(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
if_minsort(z, z', z'') -{ 1 }→ minsort(x, 1 + n + y) :|: n >= 0, z'' = y, z = 1, z' = 1 + n + x, x >= 0, y >= 0
if_minsort(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
if_minsort(z, z', z'') -{ 1 }→ 1 + n + minsort(app(rm(n, x), y), 0) :|: z = 2, n >= 0, z'' = y, z' = 1 + n + x, x >= 0, y >= 0
if_rm(z, z', z'') -{ 1 }→ rm(n, x) :|: z = 2, n >= 0, z'' = 1 + m + x, x >= 0, z' = n, m >= 0
if_rm(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
if_rm(z, z', z'') -{ 1 }→ 1 + m + rm(n, x) :|: n >= 0, z = 1, z'' = 1 + m + x, x >= 0, z' = n, m >= 0
le(z, z') -{ 1 }→ le(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
le(z, z') -{ 1 }→ 2 :|: y >= 0, z = 0, z' = y
le(z, z') -{ 1 }→ 1 :|: x >= 0, z = 1 + x, z' = 0
le(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
min(z) -{ 1 }→ n :|: z = 1 + n + 0, n >= 0
min(z) -{ 1 }→ if_min(le(n, m), 1 + n + (1 + m + x)) :|: n >= 0, x >= 0, z = 1 + n + (1 + m + x), m >= 0
min(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
minsort(z, z') -{ 1 }→ if_minsort(eq(n, min(1 + n + x)), 1 + n + x, y) :|: n >= 0, x >= 0, y >= 0, z = 1 + n + x, z' = y
minsort(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
minsort(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
rm(z, z') -{ 1 }→ if_rm(eq(n, m), n, 1 + m + x) :|: n >= 0, z' = 1 + m + x, z = n, x >= 0, m >= 0
rm(z, z') -{ 1 }→ 0 :|: n >= 0, z = n, z' = 0
rm(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
| eq(start(V, V1, V28),0,[eq(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V28),0,[le(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V28),0,[app(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V28),0,[min(V, Out)],[V >= 0]). eq(start(V, V1, V28),0,[fun(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V28),0,[rm(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V28),0,[fun1(V, V1, V28, Out)],[V >= 0,V1 >= 0,V28 >= 0]). eq(start(V, V1, V28),0,[minsort(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V28),0,[fun2(V, V1, V28, Out)],[V >= 0,V1 >= 0,V28 >= 0]). eq(eq(V, V1, Out),1,[],[Out = 2,V = 0,V1 = 0]). eq(eq(V, V1, Out),1,[],[Out = 1,V1 = 1 + V2,V2 >= 0,V = 0]). eq(eq(V, V1, Out),1,[],[Out = 1,V3 >= 0,V = 1 + V3,V1 = 0]). eq(eq(V, V1, Out),1,[eq(V4, V5, Ret)],[Out = Ret,V1 = 1 + V5,V4 >= 0,V5 >= 0,V = 1 + V4]). eq(le(V, V1, Out),1,[],[Out = 2,V6 >= 0,V = 0,V1 = V6]). eq(le(V, V1, Out),1,[],[Out = 1,V7 >= 0,V = 1 + V7,V1 = 0]). eq(le(V, V1, Out),1,[le(V8, V9, Ret1)],[Out = Ret1,V1 = 1 + V9,V8 >= 0,V9 >= 0,V = 1 + V8]). eq(app(V, V1, Out),1,[],[Out = V10,V10 >= 0,V = 0,V1 = V10]). eq(app(V, V1, Out),1,[app(V12, V13, Ret11)],[Out = 1 + Ret11 + V11,V11 >= 0,V12 >= 0,V13 >= 0,V = 1 + V11 + V12,V1 = V13]). eq(min(V, Out),1,[],[Out = V14,V = 1 + V14,V14 >= 0]). eq(min(V, Out),1,[le(V15, V16, Ret0),fun(Ret0, 1 + V15 + (1 + V16 + V17), Ret2)],[Out = Ret2,V15 >= 0,V17 >= 0,V = 2 + V15 + V16 + V17,V16 >= 0]). eq(fun(V, V1, Out),1,[min(1 + V18 + V19, Ret3)],[Out = Ret3,V = 2,V18 >= 0,V19 >= 0,V1 = 2 + V18 + V19 + V20,V20 >= 0]). eq(fun(V, V1, Out),1,[min(1 + V21 + V22, Ret4)],[Out = Ret4,V23 >= 0,V = 1,V22 >= 0,V1 = 2 + V21 + V22 + V23,V21 >= 0]). eq(rm(V, V1, Out),1,[],[Out = 0,V24 >= 0,V = V24,V1 = 0]). eq(rm(V, V1, Out),1,[eq(V25, V26, Ret01),fun1(Ret01, V25, 1 + V26 + V27, Ret5)],[Out = Ret5,V25 >= 0,V1 = 1 + V26 + V27,V = V25,V27 >= 0,V26 >= 0]). eq(fun1(V, V1, V28, Out),1,[rm(V29, V30, Ret6)],[Out = Ret6,V = 2,V29 >= 0,V28 = 1 + V30 + V31,V30 >= 0,V1 = V29,V31 >= 0]). eq(fun1(V, V1, V28, Out),1,[rm(V33, V34, Ret12)],[Out = 1 + Ret12 + V32,V33 >= 0,V = 1,V28 = 1 + V32 + V34,V34 >= 0,V1 = V33,V32 >= 0]). eq(minsort(V, V1, Out),1,[],[Out = 0,V = 0,V1 = 0]). eq(minsort(V, V1, Out),1,[min(1 + V35 + V36, Ret011),eq(V35, Ret011, Ret02),fun2(Ret02, 1 + V35 + V36, V37, Ret7)],[Out = Ret7,V35 >= 0,V36 >= 0,V37 >= 0,V = 1 + V35 + V36,V1 = V37]). eq(fun2(V, V1, V28, Out),1,[rm(V38, V39, Ret100),app(Ret100, V40, Ret10),minsort(Ret10, 0, Ret13)],[Out = 1 + Ret13 + V38,V = 2,V38 >= 0,V28 = V40,V1 = 1 + V38 + V39,V39 >= 0,V40 >= 0]). eq(fun2(V, V1, V28, Out),1,[minsort(V41, 1 + V42 + V43, Ret8)],[Out = Ret8,V42 >= 0,V28 = V43,V = 1,V1 = 1 + V41 + V42,V41 >= 0,V43 >= 0]). eq(min(V, Out),0,[],[Out = 0,V44 >= 0,V = V44]). eq(fun(V, V1, Out),0,[],[Out = 0,V45 >= 0,V46 >= 0,V = V45,V1 = V46]). eq(fun1(V, V1, V28, Out),0,[],[Out = 0,V47 >= 0,V28 = V48,V49 >= 0,V = V47,V1 = V49,V48 >= 0]). eq(minsort(V, V1, Out),0,[],[Out = 0,V50 >= 0,V51 >= 0,V = V50,V1 = V51]). eq(fun2(V, V1, V28, Out),0,[],[Out = 0,V52 >= 0,V28 = V53,V54 >= 0,V = V52,V1 = V54,V53 >= 0]). eq(eq(V, V1, Out),0,[],[Out = 0,V55 >= 0,V56 >= 0,V = V55,V1 = V56]). eq(le(V, V1, Out),0,[],[Out = 0,V57 >= 0,V58 >= 0,V = V57,V1 = V58]). eq(app(V, V1, Out),0,[],[Out = 0,V59 >= 0,V60 >= 0,V = V59,V1 = V60]). eq(rm(V, V1, Out),0,[],[Out = 0,V61 >= 0,V62 >= 0,V = V61,V1 = V62]). input_output_vars(eq(V,V1,Out),[V,V1],[Out]). input_output_vars(le(V,V1,Out),[V,V1],[Out]). input_output_vars(app(V,V1,Out),[V,V1],[Out]). input_output_vars(min(V,Out),[V],[Out]). input_output_vars(fun(V,V1,Out),[V,V1],[Out]). input_output_vars(rm(V,V1,Out),[V,V1],[Out]). input_output_vars(fun1(V,V1,V28,Out),[V,V1,V28],[Out]). input_output_vars(minsort(V,V1,Out),[V,V1],[Out]). input_output_vars(fun2(V,V1,V28,Out),[V,V1,V28],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [app/3]
1. recursive : [eq/3]
2. recursive : [le/3]
3. recursive : [fun/3,min/2]
4. recursive : [fun1/4,rm/3]
5. recursive : [fun2/4,minsort/3]
6. non_recursive : [start/3]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into app/3
1. SCC is partially evaluated into eq/3
2. SCC is partially evaluated into le/3
3. SCC is partially evaluated into min/2
4. SCC is partially evaluated into rm/3
5. SCC is partially evaluated into minsort/3
6. SCC is partially evaluated into start/3
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations app/3
* CE 27 is refined into CE [42]
* CE 25 is refined into CE [43]
* CE 26 is refined into CE [44]
### Cost equations --> "Loop" of app/3
* CEs [44] --> Loop 28
* CEs [42] --> Loop 29
* CEs [43] --> Loop 30
### Ranking functions of CR app(V,V1,Out)
* RF of phase [28]: [V]
#### Partial ranking functions of CR app(V,V1,Out)
* Partial RF of phase [28]:
- RF of loop [28:1]:
V
### Specialization of cost equations eq/3
* CE 37 is refined into CE [45]
* CE 35 is refined into CE [46]
* CE 34 is refined into CE [47]
* CE 33 is refined into CE [48]
* CE 36 is refined into CE [49]
### Cost equations --> "Loop" of eq/3
* CEs [49] --> Loop 31
* CEs [45] --> Loop 32
* CEs [46] --> Loop 33
* CEs [47] --> Loop 34
* CEs [48] --> Loop 35
### Ranking functions of CR eq(V,V1,Out)
* RF of phase [31]: [V,V1]
#### Partial ranking functions of CR eq(V,V1,Out)
* Partial RF of phase [31]:
- RF of loop [31:1]:
V
V1
### Specialization of cost equations le/3
* CE 41 is refined into CE [50]
* CE 39 is refined into CE [51]
* CE 38 is refined into CE [52]
* CE 40 is refined into CE [53]
### Cost equations --> "Loop" of le/3
* CEs [53] --> Loop 36
* CEs [50] --> Loop 37
* CEs [51] --> Loop 38
* CEs [52] --> Loop 39
### Ranking functions of CR le(V,V1,Out)
* RF of phase [36]: [V,V1]
#### Partial ranking functions of CR le(V,V1,Out)
* Partial RF of phase [36]:
- RF of loop [36:1]:
V
V1
### Specialization of cost equations min/2
* CE 31 is refined into CE [54]
* CE 28 is refined into CE [55,56,57,58,59]
* CE 32 is refined into CE [60]
* CE 29 is refined into CE [61,62]
* CE 30 is refined into CE [63,64]
### Cost equations --> "Loop" of min/2
* CEs [61,62,63,64] --> Loop 40
* CEs [54] --> Loop 41
* CEs [55,56,57,58,59,60] --> Loop 42
### Ranking functions of CR min(V,Out)
* RF of phase [40]: [V-1]
#### Partial ranking functions of CR min(V,Out)
* Partial RF of phase [40]:
- RF of loop [40:1]:
V-1
### Specialization of cost equations rm/3
* CE 20 is refined into CE [65,66,67,68,69,70,71]
* CE 23 is refined into CE [72]
* CE 24 is refined into CE [73]
* CE 21 is refined into CE [74,75,76,77]
* CE 22 is refined into CE [78,79]
### Cost equations --> "Loop" of rm/3
* CEs [75,76,77] --> Loop 43
* CEs [79] --> Loop 44
* CEs [74] --> Loop 45
* CEs [78] --> Loop 46
* CEs [72] --> Loop 47
* CEs [65,66,67,68,69,70,71,73] --> Loop 48
### Ranking functions of CR rm(V,V1,Out)
* RF of phase [43,44]: [V1]
* RF of phase [45,46]: [V1]
#### Partial ranking functions of CR rm(V,V1,Out)
* Partial RF of phase [43,44]:
- RF of loop [43:1]:
V1
- RF of loop [44:1]:
-V+V1
V1-1
* Partial RF of phase [45,46]:
- RF of loop [45:1]:
V1-1
- RF of loop [46:1]:
V1
### Specialization of cost equations minsort/3
* CE 15 is refined into CE [80,81,82,83,84,85,86,87,88,89,90,91,92,93,94]
* CE 18 is refined into CE [95]
* CE 19 is refined into CE [96]
* CE 16 is refined into CE [97,98,99,100,101,102,103]
* CE 17 is refined into CE [104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145]
### Cost equations --> "Loop" of minsort/3
* CEs [97,98,99,100,101,102,103] --> Loop 49
* CEs [112,124,134,144] --> Loop 50
* CEs [113,125,135,145] --> Loop 51
* CEs [106,118,128,138] --> Loop 52
* CEs [107,119,129,139] --> Loop 53
* CEs [104,116,120,126,130,136,140] --> Loop 54
* CEs [105,117,121,127,131,137,141] --> Loop 55
* CEs [108,110,114,122,132,142] --> Loop 56
* CEs [109,111,115,123,133,143] --> Loop 57
* CEs [83] --> Loop 58
* CEs [80,81,82,84,85,86,87,88,89,90,91,92,93,94,95,96] --> Loop 59
### Ranking functions of CR minsort(V,V1,Out)
#### Partial ranking functions of CR minsort(V,V1,Out)
* Partial RF of phase [49,50,51,52,53,54,56]:
- RF of loop [49:1,53:1]:
V-1 depends on loops [50:1,52:1,54:1,56:1]
- RF of loop [50:1]:
V/2+V1/2-1
- RF of loop [51:1]:
V/2-1 depends on loops [50:1,52:1,54:1,56:1]
- RF of loop [52:1,54:1]:
V+V1-1
- RF of loop [56:1]:
V+V1
### Specialization of cost equations start/3
* CE 8 is refined into CE [146,147,148]
* CE 4 is refined into CE [149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165]
* CE 6 is refined into CE [166,167,168]
* CE 7 is refined into CE [169,170,171]
* CE 3 is refined into CE [172,173]
* CE 2 is refined into CE [174]
* CE 5 is refined into CE [175,176,177]
* CE 9 is refined into CE [178,179,180,181,182,183,184]
* CE 10 is refined into CE [185,186,187,188,189]
* CE 11 is refined into CE [190,191,192,193]
* CE 12 is refined into CE [194,195,196]
* CE 13 is refined into CE [197,198,199]
* CE 14 is refined into CE [200,201]
### Cost equations --> "Loop" of start/3
* CEs [184] --> Loop 60
* CEs [180,186] --> Loop 61
* CEs [146,147,148] --> Loop 62
* CEs [149,151,152,153,154,155,156,158,159,161,162,163,164,165] --> Loop 63
* CEs [150,157,160,166,167,168] --> Loop 64
* CEs [169,170,171] --> Loop 65
* CEs [172,173] --> Loop 66
* CEs [175,176,177] --> Loop 67
* CEs [174,178,179,181,182,183,185,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201] --> Loop 68
### Ranking functions of CR start(V,V1,V28)
#### Partial ranking functions of CR start(V,V1,V28)
Computing Bounds
=====================================
#### Cost of chains of app(V,V1,Out):
* Chain [[28],30]: 1*it(28)+1
Such that:it(28) =< -V1+Out
with precondition: [V+V1=Out,V>=1,V1>=0]
* Chain [[28],29]: 1*it(28)+0
Such that:it(28) =< Out
with precondition: [V1>=0,Out>=1,V>=Out]
* Chain [30]: 1
with precondition: [V=0,V1=Out,V1>=0]
* Chain [29]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of eq(V,V1,Out):
* Chain [[31],35]: 1*it(31)+1
Such that:it(31) =< V
with precondition: [Out=2,V=V1,V>=1]
* Chain [[31],34]: 1*it(31)+1
Such that:it(31) =< V
with precondition: [Out=1,V>=1,V1>=V+1]
* Chain [[31],33]: 1*it(31)+1
Such that:it(31) =< V1
with precondition: [Out=1,V1>=1,V>=V1+1]
* Chain [[31],32]: 1*it(31)+0
Such that:it(31) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [35]: 1
with precondition: [V=0,V1=0,Out=2]
* Chain [34]: 1
with precondition: [V=0,Out=1,V1>=1]
* Chain [33]: 1
with precondition: [V1=0,Out=1,V>=1]
* Chain [32]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of le(V,V1,Out):
* Chain [[36],39]: 1*it(36)+1
Such that:it(36) =< V
with precondition: [Out=2,V>=1,V1>=V]
* Chain [[36],38]: 1*it(36)+1
Such that:it(36) =< V1
with precondition: [Out=1,V1>=1,V>=V1+1]
* Chain [[36],37]: 1*it(36)+0
Such that:it(36) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [39]: 1
with precondition: [V=0,Out=2,V1>=0]
* Chain [38]: 1
with precondition: [V1=0,Out=1,V>=1]
* Chain [37]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of min(V,Out):
* Chain [[40],42]: 6*it(40)+2*s(10)+2
Such that:aux(3) =< V/2
aux(4) =< V
it(40) =< aux(4)
s(11) =< it(40)*aux(3)
s(10) =< s(11)
with precondition: [Out=0,V>=2]
* Chain [[40],41]: 3*it(40)+2*s(10)+1
Such that:it(40) =< V-Out
aux(3) =< V/2
s(11) =< it(40)*aux(3)
s(10) =< s(11)
with precondition: [Out>=0,V>=Out+2]
* Chain [42]: 1*s(3)+2*s(4)+2
Such that:s(3) =< V
aux(1) =< V/2
s(4) =< aux(1)
with precondition: [Out=0,V>=0]
* Chain [41]: 1
with precondition: [V=Out+1,V>=1]
#### Cost of chains of rm(V,V1,Out):
* Chain [[45,46],48]: 8*it(45)+2
Such that:aux(11) =< V1
it(45) =< aux(11)
with precondition: [V=0,Out>=0,V1>=Out,2*V1>=Out+2]
* Chain [[45,46],47]: 6*it(45)+1
Such that:aux(12) =< V1
it(45) =< aux(12)
with precondition: [V=0,Out>=0,V1>=Out,2*V1>=Out+2]
* Chain [[43,44],48]: 5*it(43)+3*it(44)+2*s(21)+1*s(30)+1*s(31)+1*s(32)+2
Such that:it(44) =< -V+V1
aux(18) =< V
aux(19) =< V1
it(44) =< aux(19)
s(21) =< aux(18)
it(43) =< aux(19)
aux(15) =< aux(18)
s(30) =< it(43)*aux(18)
s(31) =< it(43)*aux(19)
s(32) =< it(44)*aux(15)
with precondition: [V>=1,Out>=0,V1>=Out,Out+V1>=2]
* Chain [[43,44],47]: 3*it(43)+3*it(44)+1*s(30)+1*s(31)+1*s(32)+1
Such that:it(44) =< -V+V1
aux(14) =< V
aux(20) =< V1
it(44) =< aux(20)
it(43) =< aux(20)
aux(15) =< aux(14)
s(30) =< it(43)*aux(14)
s(31) =< it(43)*aux(20)
s(32) =< it(44)*aux(15)
with precondition: [V>=1,Out>=0,V1>=Out,Out+V1>=2]
* Chain [48]: 2*s(20)+2*s(21)+2
Such that:aux(7) =< V
aux(8) =< V1
s(21) =< aux(7)
s(20) =< aux(8)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [47]: 1
with precondition: [V1=0,Out=0,V>=0]
#### Cost of chains of minsort(V,V1,Out):
* Chain [[49,50,51,52,53,54,56],59]: 5*it(49)+8*it(50)+14*it(51)+260*it(52)+20*s(63)+22*s(493)+2*s(494)+10*s(495)+79*s(503)+2*s(504)+6*s(505)+16*s(506)+8*s(507)+4*s(508)+150*s(513)+4*s(514)+12*s(515)+16*s(516)+8*s(517)+4*s(518)+71*s(523)+2*s(524)+6*s(525)+4*s(526)+4*s(534)+2*s(540)+18*s(541)+4*s(546)+16*s(548)+8*s(549)+4
Such that:it(50) =< V/2+V1/2
aux(178) =< V
aux(179) =< V+V1
it(52) =< aux(179)
s(62) =< it(52)*aux(179)
s(63) =< s(62)
it(51) =< aux(179)
it(50) =< aux(179)
s(551) =< aux(179)
aux(140) =< aux(179)+1
aux(92) =< aux(179)
aux(135) =< aux(179)-1
aux(97) =< aux(179)-2
s(138) =< aux(179)* (1/2)
s(551) =< aux(179)* (1/2)
s(543) =< aux(179)* (1/2)
aux(82) =< it(50)*aux(179)
aux(83) =< it(52)*aux(140)
aux(84) =< it(52)*aux(92)
s(530) =< it(52)*aux(135)
s(512) =< it(50)*aux(97)
aux(96) =< it(50)*aux(92)
s(528) =< aux(84)* (1/2)
s(510) =< aux(96)* (1/2)
it(49) =< aux(83)+aux(84)+aux(83)+aux(82)+aux(178)
it(51) =< aux(83)+aux(84)+aux(83)+aux(82)+aux(178)
s(538) =< it(51)*aux(135)
aux(131) =< it(51)*aux(92)
s(522) =< it(51)*aux(97)
aux(94) =< it(49)*aux(92)
s(520) =< aux(131)* (1/2)
s(499) =< aux(94)* (1/2)
s(284) =< aux(92)
s(548) =< it(52)*aux(92)
s(549) =< it(52)*s(284)
s(546) =< s(551)
s(542) =< it(52)*s(138)
s(541) =< s(542)
s(540) =< s(543)
s(534) =< s(538)
s(513) =< aux(131)
s(514) =< s(520)
s(519) =< s(513)*s(138)
s(515) =< s(519)
s(526) =< s(530)
s(523) =< aux(84)
s(524) =< s(528)
s(527) =< s(523)*s(138)
s(525) =< s(527)
s(518) =< s(522)
s(516) =< s(513)*aux(92)
s(517) =< s(513)*s(284)
s(508) =< s(512)
s(503) =< aux(96)
s(506) =< s(503)*aux(179)
s(507) =< s(503)*aux(92)
s(504) =< s(510)
s(509) =< s(503)*s(138)
s(505) =< s(509)
s(493) =< aux(94)
s(498) =< s(493)*s(138)
s(495) =< s(498)
s(494) =< s(499)
with precondition: [V>=1,V1>=0,Out>=0,Out+V>=2,V+V1>=Out]
* Chain [[49,50,51,52,53,54,56],58]: 5*it(49)+8*it(50)+7*it(51)+197*it(52)+7*it(53)+8*it(54)+22*s(493)+2*s(494)+10*s(495)+79*s(503)+2*s(504)+6*s(505)+16*s(506)+8*s(507)+4*s(508)+79*s(513)+2*s(514)+6*s(515)+16*s(516)+8*s(517)+4*s(518)+71*s(523)+2*s(524)+6*s(525)+4*s(526)+71*s(531)+2*s(532)+6*s(533)+4*s(534)+2*s(540)+18*s(541)+4*s(546)+16*s(548)+8*s(549)+3
Such that:aux(180) =< V
aux(181) =< V+V1
aux(182) =< V/2+V1/2
it(50) =< aux(182)
it(52) =< aux(181)
it(53) =< aux(181)
it(54) =< aux(181)
it(51) =< aux(182)
it(54) =< aux(182)
s(551) =< aux(182)
aux(140) =< aux(181)+1
aux(92) =< aux(181)
aux(135) =< aux(181)-1
aux(97) =< aux(181)-2
s(138) =< aux(181)* (1/2)
s(551) =< aux(181)* (1/2)
s(543) =< aux(181)* (1/2)
aux(82) =< it(50)*aux(181)
aux(83) =< it(52)*aux(140)
aux(84) =< it(54)*aux(92)
s(530) =< it(52)*aux(135)
aux(134) =< it(52)*aux(92)
s(512) =< it(50)*aux(97)
aux(96) =< it(50)*aux(92)
s(528) =< aux(134)* (1/2)
s(510) =< aux(96)* (1/2)
it(49) =< aux(83)+aux(84)+aux(83)+aux(82)+aux(180)
it(51) =< aux(83)+aux(84)+aux(83)+aux(82)+aux(180)
it(53) =< aux(83)+aux(84)+aux(83)+aux(82)+aux(180)
s(538) =< it(53)*aux(135)
aux(151) =< it(53)*aux(92)
s(522) =< it(51)*aux(97)
aux(131) =< it(51)*aux(92)
aux(94) =< it(49)*aux(92)
s(536) =< aux(151)* (1/2)
s(520) =< aux(131)* (1/2)
s(499) =< aux(94)* (1/2)
s(284) =< aux(92)
s(548) =< it(52)*aux(92)
s(549) =< it(52)*s(284)
s(546) =< s(551)
s(542) =< it(52)*s(138)
s(541) =< s(542)
s(540) =< s(543)
s(534) =< s(538)
s(531) =< aux(151)
s(532) =< s(536)
s(535) =< s(531)*s(138)
s(533) =< s(535)
s(526) =< s(530)
s(523) =< aux(134)
s(524) =< s(528)
s(527) =< s(523)*s(138)
s(525) =< s(527)
s(518) =< s(522)
s(513) =< aux(131)
s(516) =< s(513)*aux(92)
s(517) =< s(513)*s(284)
s(514) =< s(520)
s(519) =< s(513)*s(138)
s(515) =< s(519)
s(508) =< s(512)
s(503) =< aux(96)
s(506) =< s(503)*aux(181)
s(507) =< s(503)*aux(92)
s(504) =< s(510)
s(509) =< s(503)*s(138)
s(505) =< s(509)
s(493) =< aux(94)
s(498) =< s(493)*s(138)
s(495) =< s(498)
s(494) =< s(499)
with precondition: [V>=1,V1>=0,Out>=0,V+V1>=2,Out+V>=2,V+V1>=Out+1]
* Chain [[49,50,51,52,53,54,56],57,59]: 5*it(49)+12*it(50)+7*it(51)+287*it(52)+7*it(53)+8*it(54)+22*s(493)+2*s(494)+10*s(495)+79*s(503)+2*s(504)+6*s(505)+16*s(506)+8*s(507)+4*s(508)+79*s(513)+2*s(514)+6*s(515)+16*s(516)+8*s(517)+4*s(518)+71*s(523)+2*s(524)+6*s(525)+4*s(526)+71*s(531)+2*s(532)+6*s(533)+4*s(534)+2*s(540)+18*s(541)+4*s(546)+16*s(548)+8*s(549)+8*s(558)+16*s(575)+8*s(577)+11
Such that:aux(192) =< V
aux(193) =< V+V1
aux(194) =< V/2+V1/2
it(50) =< aux(194)
it(52) =< aux(193)
s(574) =< aux(193)
s(575) =< it(52)*aux(193)
s(577) =< it(52)*s(574)
s(557) =< it(52)*aux(194)
s(558) =< s(557)
it(53) =< aux(193)
it(54) =< aux(193)
it(51) =< aux(194)
it(54) =< aux(194)
s(551) =< aux(194)
aux(140) =< aux(193)+1
aux(92) =< aux(193)
aux(135) =< aux(193)-1
aux(97) =< aux(193)-2
s(138) =< aux(193)* (1/2)
s(551) =< aux(193)* (1/2)
s(543) =< aux(193)* (1/2)
aux(82) =< it(50)*aux(193)
aux(83) =< it(52)*aux(140)
aux(84) =< it(54)*aux(92)
s(530) =< it(52)*aux(135)
aux(134) =< it(52)*aux(92)
s(512) =< it(50)*aux(97)
aux(96) =< it(50)*aux(92)
s(528) =< aux(134)* (1/2)
s(510) =< aux(96)* (1/2)
it(49) =< aux(83)+aux(84)+aux(83)+aux(82)+aux(192)
it(51) =< aux(83)+aux(84)+aux(83)+aux(82)+aux(192)
it(53) =< aux(83)+aux(84)+aux(83)+aux(82)+aux(192)
s(538) =< it(53)*aux(135)
aux(151) =< it(53)*aux(92)
s(522) =< it(51)*aux(97)
aux(131) =< it(51)*aux(92)
aux(94) =< it(49)*aux(92)
s(536) =< aux(151)* (1/2)
s(520) =< aux(131)* (1/2)
s(499) =< aux(94)* (1/2)
s(284) =< aux(92)
s(548) =< it(52)*aux(92)
s(549) =< it(52)*s(284)
s(546) =< s(551)
s(542) =< it(52)*s(138)
s(541) =< s(542)
s(540) =< s(543)
s(534) =< s(538)
s(531) =< aux(151)
s(532) =< s(536)
s(535) =< s(531)*s(138)
s(533) =< s(535)
s(526) =< s(530)
s(523) =< aux(134)
s(524) =< s(528)
s(527) =< s(523)*s(138)
s(525) =< s(527)
s(518) =< s(522)
s(513) =< aux(131)
s(516) =< s(513)*aux(92)
s(517) =< s(513)*s(284)
s(514) =< s(520)
s(519) =< s(513)*s(138)
s(515) =< s(519)
s(508) =< s(512)
s(503) =< aux(96)
s(506) =< s(503)*aux(193)
s(507) =< s(503)*aux(92)
s(504) =< s(510)
s(509) =< s(503)*s(138)
s(505) =< s(509)
s(493) =< aux(94)
s(498) =< s(493)*s(138)
s(495) =< s(498)
s(494) =< s(499)
with precondition: [V>=1,V1>=0,Out>=1,V+V1>=2,Out+V>=3,V+V1>=Out]
* Chain [[49,50,51,52,53,54,56],55,59]: 5*it(49)+10*it(50)+7*it(51)+288*it(52)+7*it(53)+8*it(54)+22*s(493)+2*s(494)+10*s(495)+79*s(503)+2*s(504)+6*s(505)+16*s(506)+8*s(507)+4*s(508)+79*s(513)+2*s(514)+6*s(515)+16*s(516)+8*s(517)+4*s(518)+71*s(523)+2*s(524)+6*s(525)+4*s(526)+71*s(531)+2*s(532)+6*s(533)+4*s(534)+2*s(540)+18*s(541)+4*s(546)+16*s(548)+8*s(549)+10*s(628)+11
Such that:aux(205) =< V
aux(206) =< V+V1
aux(207) =< V/2+V1/2
it(50) =< aux(207)
it(52) =< aux(206)
s(627) =< it(52)*aux(207)
s(628) =< s(627)
it(53) =< aux(206)
it(54) =< aux(206)
it(51) =< aux(207)
it(54) =< aux(207)
s(551) =< aux(207)
aux(140) =< aux(206)+1
aux(92) =< aux(206)
aux(135) =< aux(206)-1
aux(97) =< aux(206)-2
s(138) =< aux(206)* (1/2)
s(551) =< aux(206)* (1/2)
s(543) =< aux(206)* (1/2)
aux(82) =< it(50)*aux(206)
aux(83) =< it(52)*aux(140)
aux(84) =< it(54)*aux(92)
s(530) =< it(52)*aux(135)
aux(134) =< it(52)*aux(92)
s(512) =< it(50)*aux(97)
aux(96) =< it(50)*aux(92)
s(528) =< aux(134)* (1/2)
s(510) =< aux(96)* (1/2)
it(49) =< aux(83)+aux(84)+aux(83)+aux(82)+aux(205)
it(51) =< aux(83)+aux(84)+aux(83)+aux(82)+aux(205)
it(53) =< aux(83)+aux(84)+aux(83)+aux(82)+aux(205)
s(538) =< it(53)*aux(135)
aux(151) =< it(53)*aux(92)
s(522) =< it(51)*aux(97)
aux(131) =< it(51)*aux(92)
aux(94) =< it(49)*aux(92)
s(536) =< aux(151)* (1/2)
s(520) =< aux(131)* (1/2)
s(499) =< aux(94)* (1/2)
s(284) =< aux(92)
s(548) =< it(52)*aux(92)
s(549) =< it(52)*s(284)
s(546) =< s(551)
s(542) =< it(52)*s(138)
s(541) =< s(542)
s(540) =< s(543)
s(534) =< s(538)
s(531) =< aux(151)
s(532) =< s(536)
s(535) =< s(531)*s(138)
s(533) =< s(535)
s(526) =< s(530)
s(523) =< aux(134)
s(524) =< s(528)
s(527) =< s(523)*s(138)
s(525) =< s(527)
s(518) =< s(522)
s(513) =< aux(131)
s(516) =< s(513)*aux(92)
s(517) =< s(513)*s(284)
s(514) =< s(520)
s(519) =< s(513)*s(138)
s(515) =< s(519)
s(508) =< s(512)
s(503) =< aux(96)
s(506) =< s(503)*aux(206)
s(507) =< s(503)*aux(92)
s(504) =< s(510)
s(509) =< s(503)*s(138)
s(505) =< s(509)
s(493) =< aux(94)
s(498) =< s(493)*s(138)
s(495) =< s(498)
s(494) =< s(499)
with precondition: [V>=1,V1>=0,Out>=1,V+V1>=3,V+2*Out>=5,V+V1>=Out]
* Chain [59]: 49*s(60)+6*s(61)+20*s(63)+4
Such that:aux(29) =< V
aux(30) =< V/2
s(60) =< aux(29)
s(61) =< aux(30)
s(62) =< s(60)*aux(30)
s(63) =< s(62)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [58]: 3
with precondition: [V=1,Out=0,V1>=0]
* Chain [57,59]: 90*s(555)+4*s(556)+8*s(558)+16*s(575)+8*s(577)+11
Such that:aux(189) =< V
aux(190) =< V/2
s(555) =< aux(189)
s(574) =< aux(189)
s(575) =< s(555)*aux(189)
s(577) =< s(555)*s(574)
s(556) =< aux(190)
s(557) =< s(555)*aux(190)
s(558) =< s(557)
with precondition: [V1>=0,Out>=1,V>=Out]
* Chain [55,59]: 91*s(625)+2*s(626)+10*s(628)+11
Such that:aux(202) =< V
aux(203) =< V/2
s(625) =< aux(202)
s(626) =< aux(203)
s(627) =< s(625)*aux(203)
s(628) =< s(627)
with precondition: [V>=2,V1>=0,Out>=1,V>=Out]
#### Cost of chains of start(V,V1,V28):
* Chain [68]: 28*s(961)+248*s(962)+14*s(972)+42*s(974)+6*s(988)+2*s(991)+2*s(992)+2*s(993)+32*s(1005)+16*s(1011)+8*s(1012)+30*s(1013)+1032*s(1014)+18*s(1016)+21*s(1017)+21*s(1018)+15*s(1035)+72*s(1045)+32*s(1046)+12*s(1047)+72*s(1049)+8*s(1050)+12*s(1051)+213*s(1052)+6*s(1053)+18*s(1055)+16*s(1056)+284*s(1057)+8*s(1058)+24*s(1060)+12*s(1061)+237*s(1062)+48*s(1063)+24*s(1064)+6*s(1065)+18*s(1067)+12*s(1068)+237*s(1069)+48*s(1070)+24*s(1071)+6*s(1072)+18*s(1074)+66*s(1075)+30*s(1077)+6*s(1078)+16*s(1079)+20*s(1125)+14*s(1126)+5*s(1131)+4*s(1138)+4*s(1139)+150*s(1140)+4*s(1141)+12*s(1143)+4*s(1144)+16*s(1145)+8*s(1146)+4*s(1147)+79*s(1148)+16*s(1149)+8*s(1150)+2*s(1151)+6*s(1153)+22*s(1154)+10*s(1156)+2*s(1157)+11
Such that:s(985) =< -V+V1
s(1002) =< V+V1
s(1004) =< V/2+V1/2
aux(212) =< V
aux(213) =< V/2
aux(214) =< V1
s(962) =< aux(212)
s(961) =< aux(214)
s(988) =< s(985)
s(988) =< aux(214)
s(990) =< aux(212)
s(991) =< s(961)*aux(212)
s(992) =< s(961)*aux(214)
s(993) =< s(988)*s(990)
s(972) =< aux(213)
s(973) =< s(962)*aux(213)
s(974) =< s(973)
s(1005) =< s(1004)
s(1011) =< s(962)*aux(212)
s(1012) =< s(962)*s(990)
s(1013) =< s(1004)
s(1014) =< s(1002)
s(1015) =< s(1014)*s(1004)
s(1016) =< s(1015)
s(1017) =< s(1002)
s(1005) =< s(1002)
s(1018) =< s(1004)
s(1019) =< s(1004)
s(1020) =< s(1002)+1
s(1021) =< s(1002)
s(1022) =< s(1002)-1
s(1023) =< s(1002)-2
s(1024) =< s(1002)* (1/2)
s(1019) =< s(1002)* (1/2)
s(1025) =< s(1002)* (1/2)
s(1026) =< s(1013)*s(1002)
s(1027) =< s(1014)*s(1020)
s(1028) =< s(1005)*s(1021)
s(1029) =< s(1014)*s(1022)
s(1030) =< s(1014)*s(1021)
s(1031) =< s(1013)*s(1023)
s(1032) =< s(1013)*s(1021)
s(1033) =< s(1030)* (1/2)
s(1034) =< s(1032)* (1/2)
s(1035) =< s(1027)+s(1028)+s(1027)+s(1026)+aux(212)
s(1018) =< s(1027)+s(1028)+s(1027)+s(1026)+aux(212)
s(1017) =< s(1027)+s(1028)+s(1027)+s(1026)+aux(212)
s(1036) =< s(1017)*s(1022)
s(1037) =< s(1017)*s(1021)
s(1038) =< s(1018)*s(1023)
s(1039) =< s(1018)*s(1021)
s(1040) =< s(1035)*s(1021)
s(1041) =< s(1037)* (1/2)
s(1042) =< s(1039)* (1/2)
s(1043) =< s(1040)* (1/2)
s(1044) =< s(1021)
s(1045) =< s(1014)*s(1021)
s(1046) =< s(1014)*s(1044)
s(1047) =< s(1019)
s(1048) =< s(1014)*s(1024)
s(1049) =< s(1048)
s(1050) =< s(1025)
s(1051) =< s(1036)
s(1052) =< s(1037)
s(1053) =< s(1041)
s(1054) =< s(1052)*s(1024)
s(1055) =< s(1054)
s(1056) =< s(1029)
s(1057) =< s(1030)
s(1058) =< s(1033)
s(1059) =< s(1057)*s(1024)
s(1060) =< s(1059)
s(1061) =< s(1038)
s(1062) =< s(1039)
s(1063) =< s(1062)*s(1021)
s(1064) =< s(1062)*s(1044)
s(1065) =< s(1042)
s(1066) =< s(1062)*s(1024)
s(1067) =< s(1066)
s(1068) =< s(1031)
s(1069) =< s(1032)
s(1070) =< s(1069)*s(1002)
s(1071) =< s(1069)*s(1021)
s(1072) =< s(1034)
s(1073) =< s(1069)*s(1024)
s(1074) =< s(1073)
s(1075) =< s(1040)
s(1076) =< s(1075)*s(1024)
s(1077) =< s(1076)
s(1078) =< s(1043)
s(1079) =< s(1014)*s(1002)
s(1124) =< s(1014)*s(1002)
s(1125) =< s(1124)
s(1126) =< s(1002)
s(1127) =< s(1002)
s(1127) =< s(1002)* (1/2)
s(1128) =< s(1005)*s(1002)
s(1129) =< s(1005)*s(1023)
s(1130) =< s(1028)* (1/2)
s(1131) =< s(1027)+s(1030)+s(1027)+s(1128)+aux(212)
s(1126) =< s(1027)+s(1030)+s(1027)+s(1128)+aux(212)
s(1132) =< s(1126)*s(1022)
s(1133) =< s(1126)*s(1021)
s(1134) =< s(1126)*s(1023)
s(1135) =< s(1131)*s(1021)
s(1136) =< s(1133)* (1/2)
s(1137) =< s(1135)* (1/2)
s(1138) =< s(1127)
s(1139) =< s(1132)
s(1140) =< s(1133)
s(1141) =< s(1136)
s(1142) =< s(1140)*s(1024)
s(1143) =< s(1142)
s(1144) =< s(1134)
s(1145) =< s(1140)*s(1021)
s(1146) =< s(1140)*s(1044)
s(1147) =< s(1129)
s(1148) =< s(1028)
s(1149) =< s(1148)*s(1002)
s(1150) =< s(1148)*s(1021)
s(1151) =< s(1130)
s(1152) =< s(1148)*s(1024)
s(1153) =< s(1152)
s(1154) =< s(1135)
s(1155) =< s(1154)*s(1024)
s(1156) =< s(1155)
s(1157) =< s(1137)
with precondition: [V>=0]
* Chain [67]: 24*s(1159)+4*s(1162)+6*s(1167)+2*s(1170)+2*s(1171)+2*s(1172)+3
Such that:s(1164) =< -V1+V28
aux(215) =< V1
aux(216) =< V28
s(1167) =< s(1164)
s(1167) =< aux(216)
s(1159) =< aux(216)
s(1169) =< aux(215)
s(1170) =< s(1159)*aux(215)
s(1171) =< s(1159)*aux(216)
s(1172) =< s(1167)*s(1169)
s(1162) =< aux(215)
with precondition: [V=1,V1>=0,V28>=1]
* Chain [66]: 230*s(1176)+12*s(1177)+38*s(1179)+32*s(1184)+16*s(1190)+8*s(1191)+30*s(1192)+1032*s(1193)+18*s(1195)+21*s(1196)+21*s(1197)+15*s(1214)+72*s(1224)+32*s(1225)+12*s(1226)+72*s(1228)+8*s(1229)+12*s(1230)+213*s(1231)+6*s(1232)+18*s(1234)+16*s(1235)+284*s(1236)+8*s(1237)+24*s(1239)+12*s(1240)+237*s(1241)+48*s(1242)+24*s(1243)+6*s(1244)+18*s(1246)+12*s(1247)+237*s(1248)+48*s(1249)+24*s(1250)+6*s(1251)+18*s(1253)+66*s(1254)+30*s(1256)+6*s(1257)+16*s(1258)+20*s(1304)+14*s(1305)+5*s(1310)+4*s(1317)+4*s(1318)+150*s(1319)+4*s(1320)+12*s(1322)+4*s(1323)+16*s(1324)+8*s(1325)+4*s(1326)+79*s(1327)+16*s(1328)+8*s(1329)+2*s(1330)+6*s(1332)+22*s(1333)+10*s(1335)+2*s(1336)+12
Such that:s(1181) =< V1+V28
s(1183) =< V1/2+V28/2
aux(217) =< V1
aux(218) =< V1/2
s(1176) =< aux(217)
s(1177) =< aux(218)
s(1178) =< s(1176)*aux(218)
s(1179) =< s(1178)
s(1184) =< s(1183)
s(1189) =< aux(217)
s(1190) =< s(1176)*aux(217)
s(1191) =< s(1176)*s(1189)
s(1192) =< s(1183)
s(1193) =< s(1181)
s(1194) =< s(1193)*s(1183)
s(1195) =< s(1194)
s(1196) =< s(1181)
s(1184) =< s(1181)
s(1197) =< s(1183)
s(1198) =< s(1183)
s(1199) =< s(1181)+1
s(1200) =< s(1181)
s(1201) =< s(1181)-1
s(1202) =< s(1181)-2
s(1203) =< s(1181)* (1/2)
s(1198) =< s(1181)* (1/2)
s(1204) =< s(1181)* (1/2)
s(1205) =< s(1192)*s(1181)
s(1206) =< s(1193)*s(1199)
s(1207) =< s(1184)*s(1200)
s(1208) =< s(1193)*s(1201)
s(1209) =< s(1193)*s(1200)
s(1210) =< s(1192)*s(1202)
s(1211) =< s(1192)*s(1200)
s(1212) =< s(1209)* (1/2)
s(1213) =< s(1211)* (1/2)
s(1214) =< s(1206)+s(1207)+s(1206)+s(1205)+aux(217)
s(1197) =< s(1206)+s(1207)+s(1206)+s(1205)+aux(217)
s(1196) =< s(1206)+s(1207)+s(1206)+s(1205)+aux(217)
s(1215) =< s(1196)*s(1201)
s(1216) =< s(1196)*s(1200)
s(1217) =< s(1197)*s(1202)
s(1218) =< s(1197)*s(1200)
s(1219) =< s(1214)*s(1200)
s(1220) =< s(1216)* (1/2)
s(1221) =< s(1218)* (1/2)
s(1222) =< s(1219)* (1/2)
s(1223) =< s(1200)
s(1224) =< s(1193)*s(1200)
s(1225) =< s(1193)*s(1223)
s(1226) =< s(1198)
s(1227) =< s(1193)*s(1203)
s(1228) =< s(1227)
s(1229) =< s(1204)
s(1230) =< s(1215)
s(1231) =< s(1216)
s(1232) =< s(1220)
s(1233) =< s(1231)*s(1203)
s(1234) =< s(1233)
s(1235) =< s(1208)
s(1236) =< s(1209)
s(1237) =< s(1212)
s(1238) =< s(1236)*s(1203)
s(1239) =< s(1238)
s(1240) =< s(1217)
s(1241) =< s(1218)
s(1242) =< s(1241)*s(1200)
s(1243) =< s(1241)*s(1223)
s(1244) =< s(1221)
s(1245) =< s(1241)*s(1203)
s(1246) =< s(1245)
s(1247) =< s(1210)
s(1248) =< s(1211)
s(1249) =< s(1248)*s(1181)
s(1250) =< s(1248)*s(1200)
s(1251) =< s(1213)
s(1252) =< s(1248)*s(1203)
s(1253) =< s(1252)
s(1254) =< s(1219)
s(1255) =< s(1254)*s(1203)
s(1256) =< s(1255)
s(1257) =< s(1222)
s(1258) =< s(1193)*s(1181)
s(1303) =< s(1193)*s(1181)
s(1304) =< s(1303)
s(1305) =< s(1181)
s(1306) =< s(1181)
s(1306) =< s(1181)* (1/2)
s(1307) =< s(1184)*s(1181)
s(1308) =< s(1184)*s(1202)
s(1309) =< s(1207)* (1/2)
s(1310) =< s(1206)+s(1209)+s(1206)+s(1307)+aux(217)
s(1305) =< s(1206)+s(1209)+s(1206)+s(1307)+aux(217)
s(1311) =< s(1305)*s(1201)
s(1312) =< s(1305)*s(1200)
s(1313) =< s(1305)*s(1202)
s(1314) =< s(1310)*s(1200)
s(1315) =< s(1312)* (1/2)
s(1316) =< s(1314)* (1/2)
s(1317) =< s(1306)
s(1318) =< s(1311)
s(1319) =< s(1312)
s(1320) =< s(1315)
s(1321) =< s(1319)*s(1203)
s(1322) =< s(1321)
s(1323) =< s(1313)
s(1324) =< s(1319)*s(1200)
s(1325) =< s(1319)*s(1223)
s(1326) =< s(1308)
s(1327) =< s(1207)
s(1328) =< s(1327)*s(1181)
s(1329) =< s(1327)*s(1200)
s(1330) =< s(1309)
s(1331) =< s(1327)*s(1203)
s(1332) =< s(1331)
s(1333) =< s(1314)
s(1334) =< s(1333)*s(1203)
s(1335) =< s(1334)
s(1336) =< s(1316)
with precondition: [V=1,V1>=1,V28>=0]
* Chain [65]: 10*s(1339)+2*s(1340)+4*s(1342)+3
Such that:aux(219) =< V1
aux(220) =< V1/2
s(1339) =< aux(219)
s(1340) =< aux(220)
s(1341) =< s(1339)*aux(220)
s(1342) =< s(1341)
with precondition: [V=1,V1>=2]
* Chain [64]: 38*s(1348)+96*s(1353)+3663*s(1354)+108*s(1355)+108*s(1357)+98*s(1359)+240*s(1360)+63*s(1365)+63*s(1366)+45*s(1383)+96*s(1394)+36*s(1395)+216*s(1397)+24*s(1398)+36*s(1399)+639*s(1400)+18*s(1401)+54*s(1403)+48*s(1404)+852*s(1405)+24*s(1406)+72*s(1408)+36*s(1409)+711*s(1410)+144*s(1411)+72*s(1412)+18*s(1413)+54*s(1415)+36*s(1416)+711*s(1417)+144*s(1418)+72*s(1419)+18*s(1420)+54*s(1422)+198*s(1423)+90*s(1425)+18*s(1426)+60*s(1473)+42*s(1474)+15*s(1479)+12*s(1486)+12*s(1487)+450*s(1488)+12*s(1489)+36*s(1491)+12*s(1492)+48*s(1493)+24*s(1494)+12*s(1495)+237*s(1496)+48*s(1497)+24*s(1498)+6*s(1499)+18*s(1501)+66*s(1502)+30*s(1504)+6*s(1505)+4*s(1673)+2*s(1675)+6*s(1843)+2*s(1846)+2*s(1848)+15
Such that:s(1840) =< -V1+V28
aux(229) =< V1
aux(230) =< V28
aux(231) =< V28/2
s(1843) =< s(1840)
s(1843) =< aux(230)
s(1354) =< aux(230)
s(1672) =< aux(229)
s(1846) =< s(1354)*aux(229)
s(1359) =< s(1354)*aux(230)
s(1848) =< s(1843)*s(1672)
s(1348) =< aux(229)
s(1353) =< aux(231)
s(1355) =< aux(231)
s(1356) =< s(1354)*aux(231)
s(1357) =< s(1356)
s(1358) =< aux(230)
s(1360) =< s(1354)*s(1358)
s(1365) =< aux(230)
s(1353) =< aux(230)
s(1366) =< aux(231)
s(1367) =< aux(231)
s(1368) =< aux(230)+1
s(1370) =< aux(230)-1
s(1371) =< aux(230)-2
s(1372) =< aux(230)* (1/2)
s(1367) =< aux(230)* (1/2)
s(1373) =< aux(230)* (1/2)
s(1374) =< s(1355)*aux(230)
s(1375) =< s(1354)*s(1368)
s(1376) =< s(1353)*s(1358)
s(1377) =< s(1354)*s(1370)
s(1378) =< s(1354)*s(1358)
s(1379) =< s(1355)*s(1371)
s(1380) =< s(1355)*s(1358)
s(1381) =< s(1378)* (1/2)
s(1382) =< s(1380)* (1/2)
s(1383) =< s(1375)+s(1376)+s(1375)+s(1374)+aux(230)
s(1366) =< s(1375)+s(1376)+s(1375)+s(1374)+aux(230)
s(1365) =< s(1375)+s(1376)+s(1375)+s(1374)+aux(230)
s(1384) =< s(1365)*s(1370)
s(1385) =< s(1365)*s(1358)
s(1386) =< s(1366)*s(1371)
s(1387) =< s(1366)*s(1358)
s(1388) =< s(1383)*s(1358)
s(1389) =< s(1385)* (1/2)
s(1390) =< s(1387)* (1/2)
s(1391) =< s(1388)* (1/2)
s(1392) =< s(1358)
s(1394) =< s(1354)*s(1392)
s(1395) =< s(1367)
s(1396) =< s(1354)*s(1372)
s(1397) =< s(1396)
s(1398) =< s(1373)
s(1399) =< s(1384)
s(1400) =< s(1385)
s(1401) =< s(1389)
s(1402) =< s(1400)*s(1372)
s(1403) =< s(1402)
s(1404) =< s(1377)
s(1405) =< s(1378)
s(1406) =< s(1381)
s(1407) =< s(1405)*s(1372)
s(1408) =< s(1407)
s(1409) =< s(1386)
s(1410) =< s(1387)
s(1411) =< s(1410)*s(1358)
s(1412) =< s(1410)*s(1392)
s(1413) =< s(1390)
s(1414) =< s(1410)*s(1372)
s(1415) =< s(1414)
s(1416) =< s(1379)
s(1417) =< s(1380)
s(1418) =< s(1417)*aux(230)
s(1419) =< s(1417)*s(1358)
s(1420) =< s(1382)
s(1421) =< s(1417)*s(1372)
s(1422) =< s(1421)
s(1423) =< s(1388)
s(1424) =< s(1423)*s(1372)
s(1425) =< s(1424)
s(1426) =< s(1391)
s(1472) =< s(1354)*aux(230)
s(1473) =< s(1472)
s(1474) =< aux(230)
s(1475) =< aux(230)
s(1475) =< aux(230)* (1/2)
s(1476) =< s(1353)*aux(230)
s(1477) =< s(1353)*s(1371)
s(1478) =< s(1376)* (1/2)
s(1479) =< s(1375)+s(1378)+s(1375)+s(1476)+aux(230)
s(1474) =< s(1375)+s(1378)+s(1375)+s(1476)+aux(230)
s(1480) =< s(1474)*s(1370)
s(1481) =< s(1474)*s(1358)
s(1482) =< s(1474)*s(1371)
s(1483) =< s(1479)*s(1358)
s(1484) =< s(1481)* (1/2)
s(1485) =< s(1483)* (1/2)
s(1486) =< s(1475)
s(1487) =< s(1480)
s(1488) =< s(1481)
s(1489) =< s(1484)
s(1490) =< s(1488)*s(1372)
s(1491) =< s(1490)
s(1492) =< s(1482)
s(1493) =< s(1488)*s(1358)
s(1494) =< s(1488)*s(1392)
s(1495) =< s(1477)
s(1496) =< s(1376)
s(1497) =< s(1496)*aux(230)
s(1498) =< s(1496)*s(1358)
s(1499) =< s(1478)
s(1500) =< s(1496)*s(1372)
s(1501) =< s(1500)
s(1502) =< s(1483)
s(1503) =< s(1502)*s(1372)
s(1504) =< s(1503)
s(1505) =< s(1485)
s(1673) =< s(1348)*aux(229)
s(1675) =< s(1348)*s(1672)
with precondition: [V=2,V1>=0,V28>=1]
* Chain [63]: 2789*s(1851)+147*s(1854)+18*s(1855)+60*s(1857)+1389*s(1871)+6*s(1872)+20*s(1874)+1*s(1877)+32*s(1882)+1213*s(1883)+36*s(1884)+36*s(1886)+32*s(1888)+80*s(1889)+21*s(1894)+21*s(1895)+15*s(1912)+32*s(1923)+12*s(1924)+72*s(1926)+8*s(1927)+12*s(1928)+213*s(1929)+6*s(1930)+18*s(1932)+16*s(1933)+284*s(1934)+8*s(1935)+24*s(1937)+12*s(1938)+237*s(1939)+48*s(1940)+24*s(1941)+6*s(1942)+18*s(1944)+12*s(1945)+237*s(1946)+48*s(1947)+24*s(1948)+6*s(1949)+18*s(1951)+66*s(1952)+30*s(1954)+6*s(1955)+20*s(2002)+14*s(2003)+5*s(2008)+4*s(2015)+4*s(2016)+150*s(2017)+4*s(2018)+12*s(2020)+4*s(2021)+16*s(2022)+8*s(2023)+4*s(2024)+79*s(2025)+16*s(2026)+8*s(2027)+2*s(2028)+6*s(2030)+22*s(2031)+10*s(2033)+2*s(2034)+42*s(2041)+56*s(2043)+32*s(2051)+84*s(2057)+168*s(2058)+21*s(2063)+21*s(2064)+15*s(2081)+64*s(2092)+12*s(2093)+144*s(2095)+16*s(2096)+12*s(2097)+213*s(2098)+6*s(2099)+18*s(2101)+32*s(2102)+884*s(2103)+8*s(2104)+24*s(2106)+12*s(2107)+237*s(2108)+48*s(2109)+24*s(2110)+6*s(2111)+18*s(2113)+12*s(2114)+237*s(2115)+48*s(2116)+24*s(2117)+6*s(2118)+18*s(2120)+66*s(2121)+30*s(2123)+6*s(2124)+96*s(2171)+14*s(2172)+5*s(2177)+20*s(2184)+4*s(2185)+150*s(2186)+4*s(2187)+12*s(2189)+4*s(2190)+16*s(2191)+8*s(2192)+4*s(2193)+79*s(2194)+16*s(2195)+8*s(2196)+2*s(2197)+6*s(2199)+22*s(2200)+10*s(2202)+2*s(2203)+4*s(2262)+4*s(2264)+76*s(2272)+32*s(2294)+80*s(2295)+56*s(2300)+20*s(2318)+32*s(2329)+16*s(2330)+72*s(2332)+8*s(2333)+16*s(2334)+600*s(2335)+16*s(2336)+48*s(2338)+16*s(2339)+600*s(2340)+16*s(2341)+48*s(2343)+16*s(2344)+64*s(2346)+32*s(2347)+16*s(2351)+64*s(2353)+32*s(2354)+88*s(2358)+40*s(2360)+8*s(2361)+56*s(2485)+20*s(2503)+16*s(2519)+600*s(2520)+16*s(2521)+48*s(2523)+16*s(2526)+48*s(2528)+16*s(2529)+64*s(2531)+32*s(2532)+16*s(2536)+64*s(2538)+32*s(2539)+88*s(2543)+40*s(2545)+8*s(2546)+15
Such that:aux(234) =< V1+V28/2
s(1877) =< 2*V1
aux(235) =< 2*V1+V28
s(1870) =< V1/2+V28/2
aux(251) =< V1
aux(252) =< V1+V28
aux(253) =< V1/2
aux(254) =< V28
aux(255) =< V28/2
s(1851) =< aux(251)
s(2051) =< aux(253)
s(2041) =< aux(253)
s(2042) =< s(1851)*aux(253)
s(2043) =< s(2042)
s(2056) =< aux(251)
s(2057) =< s(1851)*aux(251)
s(2058) =< s(1851)*s(2056)
s(2063) =< aux(251)
s(2051) =< aux(251)
s(2064) =< aux(253)
s(2065) =< aux(253)
s(2066) =< aux(251)+1
s(2068) =< aux(251)-1
s(2069) =< aux(251)-2
s(2070) =< aux(251)* (1/2)
s(2065) =< aux(251)* (1/2)
s(2071) =< aux(251)* (1/2)
s(2072) =< s(2041)*aux(251)
s(2073) =< s(1851)*s(2066)
s(2074) =< s(2051)*s(2056)
s(2075) =< s(1851)*s(2068)
s(2076) =< s(1851)*s(2056)
s(2077) =< s(2041)*s(2069)
s(2078) =< s(2041)*s(2056)
s(2079) =< s(2076)* (1/2)
s(2080) =< s(2078)* (1/2)
s(2081) =< s(2073)+s(2074)+s(2073)+s(2072)+aux(251)
s(2064) =< s(2073)+s(2074)+s(2073)+s(2072)+aux(251)
s(2063) =< s(2073)+s(2074)+s(2073)+s(2072)+aux(251)
s(2082) =< s(2063)*s(2068)
s(2083) =< s(2063)*s(2056)
s(2084) =< s(2064)*s(2069)
s(2085) =< s(2064)*s(2056)
s(2086) =< s(2081)*s(2056)
s(2087) =< s(2083)* (1/2)
s(2088) =< s(2085)* (1/2)
s(2089) =< s(2086)* (1/2)
s(2090) =< s(2056)
s(2092) =< s(1851)*s(2090)
s(2093) =< s(2065)
s(2094) =< s(1851)*s(2070)
s(2095) =< s(2094)
s(2096) =< s(2071)
s(2097) =< s(2082)
s(2098) =< s(2083)
s(2099) =< s(2087)
s(2100) =< s(2098)*s(2070)
s(2101) =< s(2100)
s(2102) =< s(2075)
s(2103) =< s(2076)
s(2104) =< s(2079)
s(2105) =< s(2103)*s(2070)
s(2106) =< s(2105)
s(2107) =< s(2084)
s(2108) =< s(2085)
s(2109) =< s(2108)*s(2056)
s(2110) =< s(2108)*s(2090)
s(2111) =< s(2088)
s(2112) =< s(2108)*s(2070)
s(2113) =< s(2112)
s(2114) =< s(2077)
s(2115) =< s(2078)
s(2116) =< s(2115)*aux(251)
s(2117) =< s(2115)*s(2056)
s(2118) =< s(2080)
s(2119) =< s(2115)*s(2070)
s(2120) =< s(2119)
s(2121) =< s(2086)
s(2122) =< s(2121)*s(2070)
s(2123) =< s(2122)
s(2124) =< s(2089)
s(2170) =< s(1851)*aux(251)
s(2171) =< s(2170)
s(2172) =< aux(251)
s(2173) =< aux(251)
s(2173) =< aux(251)* (1/2)
s(2174) =< s(2051)*aux(251)
s(2175) =< s(2051)*s(2069)
s(2176) =< s(2074)* (1/2)
s(2177) =< s(2073)+s(2076)+s(2073)+s(2174)+aux(251)
s(2172) =< s(2073)+s(2076)+s(2073)+s(2174)+aux(251)
s(2178) =< s(2172)*s(2068)
s(2179) =< s(2172)*s(2056)
s(2180) =< s(2172)*s(2069)
s(2181) =< s(2177)*s(2056)
s(2182) =< s(2179)* (1/2)
s(2183) =< s(2181)* (1/2)
s(2184) =< s(2173)
s(2185) =< s(2178)
s(2186) =< s(2179)
s(2187) =< s(2182)
s(2188) =< s(2186)*s(2070)
s(2189) =< s(2188)
s(2190) =< s(2180)
s(2191) =< s(2186)*s(2056)
s(2192) =< s(2186)*s(2090)
s(2193) =< s(2175)
s(2194) =< s(2074)
s(2195) =< s(2194)*aux(251)
s(2196) =< s(2194)*s(2056)
s(2197) =< s(2176)
s(2198) =< s(2194)*s(2070)
s(2199) =< s(2198)
s(2200) =< s(2181)
s(2201) =< s(2200)*s(2070)
s(2202) =< s(2201)
s(2203) =< s(2183)
s(1871) =< aux(252)
s(2271) =< s(1871)*aux(252)
s(2272) =< s(2271)
s(2261) =< aux(252)
s(2262) =< s(1851)*aux(252)
s(2264) =< s(1851)*s(2261)
s(2294) =< s(1871)*aux(252)
s(2295) =< s(1871)*s(2261)
s(2300) =< aux(252)
s(2302) =< aux(252)
s(2303) =< aux(252)+1
s(2305) =< aux(252)-1
s(2306) =< aux(252)-2
s(2307) =< aux(252)* (1/2)
s(2302) =< aux(252)* (1/2)
s(2308) =< aux(252)* (1/2)
s(2310) =< s(1871)*s(2303)
s(2311) =< s(1871)*s(2261)
s(2312) =< s(1871)*s(2305)
s(2314) =< s(1871)*s(2306)
s(2316) =< s(2311)* (1/2)
s(2318) =< s(2310)+s(2311)+s(2310)+s(2271)+aux(252)
s(2300) =< s(2310)+s(2311)+s(2310)+s(2271)+aux(252)
s(2319) =< s(2300)*s(2305)
s(2320) =< s(2300)*s(2261)
s(2321) =< s(2300)*s(2306)
s(2323) =< s(2318)*s(2261)
s(2324) =< s(2320)* (1/2)
s(2326) =< s(2323)* (1/2)
s(2327) =< s(2261)
s(2329) =< s(1871)*s(2327)
s(2330) =< s(2302)
s(2331) =< s(1871)*s(2307)
s(2332) =< s(2331)
s(2333) =< s(2308)
s(2334) =< s(2319)
s(2335) =< s(2320)
s(2336) =< s(2324)
s(2337) =< s(2335)*s(2307)
s(2338) =< s(2337)
s(2339) =< s(2312)
s(2340) =< s(2311)
s(2341) =< s(2316)
s(2342) =< s(2340)*s(2307)
s(2343) =< s(2342)
s(2344) =< s(2321)
s(2346) =< s(2335)*s(2261)
s(2347) =< s(2335)*s(2327)
s(2351) =< s(2314)
s(2353) =< s(2340)*aux(252)
s(2354) =< s(2340)*s(2261)
s(2358) =< s(2323)
s(2359) =< s(2358)*s(2307)
s(2360) =< s(2359)
s(2361) =< s(2326)
s(2485) =< aux(251)
s(2499) =< s(1851)*s(2069)
s(2501) =< s(2076)* (1/2)
s(2503) =< s(2073)+s(2076)+s(2073)+s(2170)+aux(251)
s(2485) =< s(2073)+s(2076)+s(2073)+s(2170)+aux(251)
s(2504) =< s(2485)*s(2068)
s(2505) =< s(2485)*s(2056)
s(2506) =< s(2485)*s(2069)
s(2508) =< s(2503)*s(2056)
s(2509) =< s(2505)* (1/2)
s(2511) =< s(2508)* (1/2)
s(2519) =< s(2504)
s(2520) =< s(2505)
s(2521) =< s(2509)
s(2522) =< s(2520)*s(2070)
s(2523) =< s(2522)
s(2526) =< s(2501)
s(2527) =< s(2103)*s(2070)
s(2528) =< s(2527)
s(2529) =< s(2506)
s(2531) =< s(2520)*s(2056)
s(2532) =< s(2520)*s(2090)
s(2536) =< s(2499)
s(2538) =< s(2103)*aux(251)
s(2539) =< s(2103)*s(2056)
s(2543) =< s(2508)
s(2544) =< s(2543)*s(2070)
s(2545) =< s(2544)
s(2546) =< s(2511)
s(1854) =< aux(254)
s(1855) =< aux(255)
s(1856) =< s(1854)*aux(255)
s(1857) =< s(1856)
s(1882) =< aux(234)
s(1883) =< aux(235)
s(1884) =< aux(234)
s(1885) =< s(1883)*aux(234)
s(1886) =< s(1885)
s(1887) =< aux(235)
s(1888) =< s(1883)*aux(235)
s(1889) =< s(1883)*s(1887)
s(1894) =< aux(235)
s(1882) =< aux(235)
s(1895) =< aux(234)
s(1896) =< aux(234)
s(1897) =< aux(235)+1
s(1899) =< aux(235)-1
s(1900) =< aux(235)-2
s(1901) =< aux(235)* (1/2)
s(1896) =< aux(235)* (1/2)
s(1902) =< aux(235)* (1/2)
s(1903) =< s(1884)*aux(235)
s(1904) =< s(1883)*s(1897)
s(1905) =< s(1882)*s(1887)
s(1906) =< s(1883)*s(1899)
s(1907) =< s(1883)*s(1887)
s(1908) =< s(1884)*s(1900)
s(1909) =< s(1884)*s(1887)
s(1910) =< s(1907)* (1/2)
s(1911) =< s(1909)* (1/2)
s(1912) =< s(1904)+s(1905)+s(1904)+s(1903)+aux(235)
s(1895) =< s(1904)+s(1905)+s(1904)+s(1903)+aux(235)
s(1894) =< s(1904)+s(1905)+s(1904)+s(1903)+aux(235)
s(1913) =< s(1894)*s(1899)
s(1914) =< s(1894)*s(1887)
s(1915) =< s(1895)*s(1900)
s(1916) =< s(1895)*s(1887)
s(1917) =< s(1912)*s(1887)
s(1918) =< s(1914)* (1/2)
s(1919) =< s(1916)* (1/2)
s(1920) =< s(1917)* (1/2)
s(1921) =< s(1887)
s(1923) =< s(1883)*s(1921)
s(1924) =< s(1896)
s(1925) =< s(1883)*s(1901)
s(1926) =< s(1925)
s(1927) =< s(1902)
s(1928) =< s(1913)
s(1929) =< s(1914)
s(1930) =< s(1918)
s(1931) =< s(1929)*s(1901)
s(1932) =< s(1931)
s(1933) =< s(1906)
s(1934) =< s(1907)
s(1935) =< s(1910)
s(1936) =< s(1934)*s(1901)
s(1937) =< s(1936)
s(1938) =< s(1915)
s(1939) =< s(1916)
s(1940) =< s(1939)*s(1887)
s(1941) =< s(1939)*s(1921)
s(1942) =< s(1919)
s(1943) =< s(1939)*s(1901)
s(1944) =< s(1943)
s(1945) =< s(1908)
s(1946) =< s(1909)
s(1947) =< s(1946)*aux(235)
s(1948) =< s(1946)*s(1887)
s(1949) =< s(1911)
s(1950) =< s(1946)*s(1901)
s(1951) =< s(1950)
s(1952) =< s(1917)
s(1953) =< s(1952)*s(1901)
s(1954) =< s(1953)
s(1955) =< s(1920)
s(2001) =< s(1883)*aux(235)
s(2002) =< s(2001)
s(2003) =< aux(235)
s(2004) =< aux(235)
s(2004) =< aux(235)* (1/2)
s(2005) =< s(1882)*aux(235)
s(2006) =< s(1882)*s(1900)
s(2007) =< s(1905)* (1/2)
s(2008) =< s(1904)+s(1907)+s(1904)+s(2005)+aux(235)
s(2003) =< s(1904)+s(1907)+s(1904)+s(2005)+aux(235)
s(2009) =< s(2003)*s(1899)
s(2010) =< s(2003)*s(1887)
s(2011) =< s(2003)*s(1900)
s(2012) =< s(2008)*s(1887)
s(2013) =< s(2010)* (1/2)
s(2014) =< s(2012)* (1/2)
s(2015) =< s(2004)
s(2016) =< s(2009)
s(2017) =< s(2010)
s(2018) =< s(2013)
s(2019) =< s(2017)*s(1901)
s(2020) =< s(2019)
s(2021) =< s(2011)
s(2022) =< s(2017)*s(1887)
s(2023) =< s(2017)*s(1921)
s(2024) =< s(2006)
s(2025) =< s(1905)
s(2026) =< s(2025)*aux(235)
s(2027) =< s(2025)*s(1887)
s(2028) =< s(2007)
s(2029) =< s(2025)*s(1901)
s(2030) =< s(2029)
s(2031) =< s(2012)
s(2032) =< s(2031)*s(1901)
s(2033) =< s(2032)
s(2034) =< s(2014)
s(1872) =< s(1870)
s(1873) =< s(1871)*s(1870)
s(1874) =< s(1873)
with precondition: [V=2,V1>=1,V28>=0]
* Chain [62]: 10*s(2628)+2*s(2629)+4*s(2631)+3
Such that:aux(256) =< V1
aux(257) =< V1/2
s(2628) =< aux(256)
s(2629) =< aux(257)
s(2630) =< s(2628)*aux(257)
s(2631) =< s(2630)
with precondition: [V=2,V1>=2]
* Chain [61]: 1
with precondition: [V1=0,V>=1]
* Chain [60]: 1*s(2636)+1
Such that:s(2636) =< V1
with precondition: [V=V1,V>=1]
Closed-form bounds of start(V,V1,V28):
-------------------------------------
* Chain [68] with precondition: [V>=0]
- Upper bound: 268*V+11+24*V*V+2*V*nat(V1)+2*V*nat(-V+V1)+nat(V1)*28+nat(V1)*2*nat(V1)+nat(nat(V+V1)+ -2)*4*nat(V+V1)+nat(nat(V+V1)+ -2)*28*nat(V/2+V1/2)+nat(nat(V+V1)+ -1)*32*nat(V+V1)+nat(V+V1)*1115+nat(V+V1)*92*V+nat(V+V1)*1061*nat(V+V1)+nat(V+V1)*20*nat(V+V1)*V+nat(V+V1)*298*nat(V+V1)*nat(V+V1)+nat(V+V1)*45*nat(V+V1)*nat(V+V1)*nat(V+V1)+nat(V+V1)*35*nat(V+V1)*nat(V+V1)*nat(V/2+V1/2)+nat(V+V1)*350*nat(V+V1)*nat(V/2+V1/2)+nat(V+V1)*595*nat(V/2+V1/2)+nat(-V+V1)*6+nat(V/2+V1/2)*95+nat(V/2+V1/2)*18*nat(V+V1)+7*V+21*V*V
- Complexity: n^4
* Chain [67] with precondition: [V=1,V1>=0,V28>=1]
- Upper bound: 4*V1+3+2*V1*V28+2*V1*nat(-V1+V28)+24*V28+2*V28*V28+nat(-V1+V28)*6
- Complexity: n^2
* Chain [66] with precondition: [V=1,V1>=1,V28>=0]
- Upper bound: 250*V1+12+24*V1*V1+ (V1+V28)* (nat(V1+V28-2)*4)+ (V1/2+V28/2)* (nat(V1+V28-2)*28)+ (32*V1+32*V28-32)* (V1+V28)+ (1115*V1+1115*V28)+ (92*V1+92*V28)*V1+ (1061*V1+1061*V28)* (V1+V28)+ (20*V1+20*V28)* (V1+V28)*V1+ (V1+V28)* ((298*V1+298*V28)* (V1+V28))+ (V1+V28)* ((V1+V28)* ((45*V1+45*V28)* (V1+V28)))+ (V1/2+V28/2)* ((V1+V28)* ((35*V1+35*V28)* (V1+V28)))+ (V1/2+V28/2)* ((350*V1+350*V28)* (V1+V28))+ (V1/2+V28/2)* (595*V1+595*V28)+ (95/2*V1+95/2*V28)+ (9*V1+9*V28)* (V1+V28)+6*V1+19*V1*V1
- Complexity: n^4
* Chain [65] with precondition: [V=1,V1>=2]
- Upper bound: 11*V1+3+2*V1*V1
- Complexity: n^2
* Chain [64] with precondition: [V=2,V1>=0,V28>=1]
- Upper bound: 38*V1+15+6*V1*V1+2*V1*V28+2*V1*nat(-V1+V28)+3972*V28+3533*V28*V28+954*V28*V28*V28+135*V28*V28*V28*V28+V28/2* (105*V28*V28*V28)+V28/2* (1050*V28*V28)+V28/2* (1785*V28)+nat(V28-2)*12*V28+V28/2* (nat(V28-2)*84)+ (96*V28-96)*V28+nat(-V1+V28)*6+303/2*V28+54*V28*V28
- Complexity: n^4
* Chain [63] with precondition: [V=2,V1>=1,V28>=0]
- Upper bound: 3028*V1+15+3033*V1*V1+986*V1*V1*V1+125*V1*V1*V1*V1+V1/2* (35*V1*V1*V1)+V1/2* (350*V1*V1)+V1/2* (595*V1)+147*V28+nat(V1-2)*36*V1+V1/2* (nat(V1-2)*28)+ (V1+V28)* (nat(V1+V28-2)*32)+ (56*V1+28*V28-56)* (V1+V28/2)+ (8*V1+4*V28-8)* (2*V1+V28)+ (64*V1-64)*V1+ (32*V1+32*V28-32)* (V1+V28)+ (64*V1+32*V28-32)* (2*V1+V28)+2*V1+ (1525*V1+1525*V28)+ (8*V1+8*V28)*V1+ (1828*V1+1828*V28)* (V1+V28)+ (V1+V28)* ((668*V1+668*V28)* (V1+V28))+ (V1+V28)* ((V1+V28)* ((80*V1+80*V28)* (V1+V28)))+ (101*V1+101/2*V28)+ (36*V1+18*V28)* (2*V1+V28)+ (2632*V1+1316*V28)+ (1190*V1+595*V28)* (V1+V28/2)+ (2*V1+V28)* ((48*V1+24*V28)* (V1+V28/2))+ (2354*V1+1177*V28)* (2*V1+V28)+ (V1+V28/2)* ((652*V1+326*V28)* (2*V1+V28))+ (2*V1+V28)* ((636*V1+318*V28)* (2*V1+V28))+ (V1+V28/2)* ((2*V1+V28)* ((70*V1+35*V28)* (2*V1+V28)))+ (2*V1+V28)* ((2*V1+V28)* ((90*V1+45*V28)* (2*V1+V28)))+ (3*V1+3*V28)+ (10*V1+10*V28)* (V1+V28)+107/2*V1+28*V1*V1+9*V28+30*V28*V28
- Complexity: n^4
* Chain [62] with precondition: [V=2,V1>=2]
- Upper bound: 11*V1+3+2*V1*V1
- Complexity: n^2
* Chain [61] with precondition: [V1=0,V>=1]
- Upper bound: 1
- Complexity: constant
* Chain [60] with precondition: [V=V1,V>=1]
- Upper bound: V1+1
- Complexity: n
### Maximum cost of start(V,V1,V28): nat(V1)*3+2+max([nat(V1)*6+max([nat(V1/2)*4*nat(V1)+nat(V1/2)*2,nat(V1)*18+8+nat(V1)*2*nat(V1)+max([nat(V1)*10+1+nat(V1)*4*nat(V1)+max([nat(V1)*18*nat(V1)+nat(V1)*212+nat(nat(V1+V28)+ -2)*4*nat(V1+V28)+nat(nat(V1+V28)+ -1)*32*nat(V1+V28)+nat(V1+V28)*1115+nat(V1+V28)*8*nat(V1)+nat(V1+V28)*1061*nat(V1+V28)+nat(V1+V28)*298*nat(V1+V28)*nat(V1+V28)+nat(V1+V28)*45*nat(V1+V28)*nat(V1+V28)*nat(V1+V28)+nat(V1/2+V28/2)*6+nat(V1/2+V28/2)*18*nat(V1+V28)+nat(V1/2)*12+nat(V1/2)*38*nat(V1)+max([nat(nat(V1+V28)+ -2)*28*nat(V1/2+V28/2)+nat(V1+V28)*84*nat(V1)+nat(V1+V28)*20*nat(V1+V28)*nat(V1)+nat(V1+V28)*35*nat(V1+V28)*nat(V1+V28)*nat(V1/2+V28/2)+nat(V1+V28)*350*nat(V1+V28)*nat(V1/2+V28/2)+nat(V1+V28)*595*nat(V1/2+V28/2)+nat(V1/2+V28/2)*89,nat(V1)*2778+3+nat(V1)*3009*nat(V1)+nat(V1)*986*nat(V1)*nat(V1)+nat(V1)*125*nat(V1)*nat(V1)*nat(V1)+nat(V1)*35*nat(V1)*nat(V1)*nat(V1/2)+nat(V1)*350*nat(V1)*nat(V1/2)+nat(V1)*595*nat(V1/2)+nat(V28)*147+nat(nat(V1)+ -2)*36*nat(V1)+nat(nat(V1)+ -2)*28*nat(V1/2)+nat(nat(V1+V28)+ -2)*28*nat(V1+V28)+nat(nat(2*V1+V28)+ -2)*28*nat(V1+V28/2)+nat(nat(2*V1+V28)+ -2)*4*nat(2*V1+V28)+nat(nat(V1)+ -1)*64*nat(V1)+nat(nat(2*V1+V28)+ -1)*32*nat(2*V1+V28)+nat(2*V1)+nat(V1+V28)*410+nat(V1+V28)*767*nat(V1+V28)+nat(V1+V28)*370*nat(V1+V28)*nat(V1+V28)+nat(V1+V28)*35*nat(V1+V28)*nat(V1+V28)*nat(V1+V28)+nat(V1+V28/2)*101+nat(V1+V28/2)*36*nat(2*V1+V28)+nat(2*V1+V28)*1316+nat(2*V1+V28)*595*nat(V1+V28/2)+nat(2*V1+V28)*24*nat(V1+V28/2)*nat(2*V1+V28)+nat(2*V1+V28)*1177*nat(2*V1+V28)+nat(2*V1+V28)*326*nat(2*V1+V28)*nat(V1+V28/2)+nat(2*V1+V28)*318*nat(2*V1+V28)*nat(2*V1+V28)+nat(2*V1+V28)*35*nat(2*V1+V28)*nat(2*V1+V28)*nat(V1+V28/2)+nat(2*V1+V28)*45*nat(2*V1+V28)*nat(2*V1+V28)*nat(2*V1+V28)+nat(V1/2+V28/2)*2*nat(V1+V28)+nat(V1/2)*95+nat(V1/2)*18*nat(V1)+nat(V28/2)*18+nat(V28/2)*60*nat(V28)]),nat(V1)*2*nat(V28)+3+nat(V1)*2*nat(-V1+V28)+nat(V28)*3972+nat(V28)*3533*nat(V28)+nat(V28)*954*nat(V28)*nat(V28)+nat(V28)*135*nat(V28)*nat(V28)*nat(V28)+nat(V28)*105*nat(V28)*nat(V28)*nat(V28/2)+nat(V28)*1050*nat(V28)*nat(V28/2)+nat(V28)*1785*nat(V28/2)+nat(nat(V28)+ -2)*12*nat(V28)+nat(nat(V28)+ -2)*84*nat(V28/2)+nat(nat(V28)+ -1)*96*nat(V28)+nat(-V1+V28)*6+nat(V28/2)*303+nat(V28/2)*108*nat(V28)]),24*V*V+268*V+2*V*nat(V1)+2*V*nat(-V+V1)+nat(nat(V+V1)+ -2)*4*nat(V+V1)+nat(nat(V+V1)+ -2)*28*nat(V/2+V1/2)+nat(nat(V+V1)+ -1)*32*nat(V+V1)+nat(V+V1)*1115+nat(V+V1)*92*V+nat(V+V1)*1061*nat(V+V1)+nat(V+V1)*20*nat(V+V1)*V+nat(V+V1)*298*nat(V+V1)*nat(V+V1)+nat(V+V1)*45*nat(V+V1)*nat(V+V1)*nat(V+V1)+nat(V+V1)*35*nat(V+V1)*nat(V+V1)*nat(V/2+V1/2)+nat(V+V1)*350*nat(V+V1)*nat(V/2+V1/2)+nat(V+V1)*595*nat(V/2+V1/2)+nat(-V+V1)*6+nat(V/2+V1/2)*95+nat(V/2+V1/2)*18*nat(V+V1)+7*V+21*V*V])]),nat(V1)*2*nat(-V1+V28)+nat(V1)*2*nat(V28)+nat(V28)*24+nat(V28)*2*nat(V28)+nat(-V1+V28)*6])+nat(V1)+1
Asymptotic class: n^4
* Total analysis performed in 7902 ms.