0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 4907 ms)
↳10 BOUNDS(1, n^1)
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil)
if(false, c, x, y, z) → z
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
min(0, y) → 0 [1]
min(s(x), 0) → 0 [1]
min(s(x), s(y)) → min(x, y) [1]
len(nil) → 0 [1]
len(cons(x, xs)) → s(len(xs)) [1]
sum(x, 0) → x [1]
sum(x, s(y)) → s(sum(x, y)) [1]
le(0, x) → true [1]
le(s(x), 0) → false [1]
le(s(x), s(y)) → le(x, y) [1]
take(0, cons(y, ys)) → y [1]
take(s(x), cons(y, ys)) → take(x, ys) [1]
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil) [1]
if(false, c, x, y, z) → z [1]
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)) [1]
min(0, y) → 0 [1]
min(s(x), 0) → 0 [1]
min(s(x), s(y)) → min(x, y) [1]
len(nil) → 0 [1]
len(cons(x, xs)) → s(len(xs)) [1]
sum(x, 0) → x [1]
sum(x, s(y)) → s(sum(x, y)) [1]
le(0, x) → true [1]
le(s(x), 0) → false [1]
le(s(x), s(y)) → le(x, y) [1]
take(0, cons(y, ys)) → y [1]
take(s(x), cons(y, ys)) → take(x, ys) [1]
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil) [1]
if(false, c, x, y, z) → z [1]
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)) [1]
| min :: 0:s → 0:s → 0:s 0 :: 0:s s :: 0:s → 0:s len :: nil:cons → 0:s nil :: nil:cons cons :: 0:s → nil:cons → nil:cons sum :: 0:s → 0:s → 0:s le :: 0:s → 0:s → true:false true :: true:false false :: true:false take :: 0:s → nil:cons → 0:s addList :: nil:cons → nil:cons → nil:cons if :: true:false → 0:s → nil:cons → nil:cons → nil:cons → nil:cons |
take(v0, v1) → null_take [0]
min(v0, v1) → null_min [0]
sum(v0, v1) → null_sum [0]
le(v0, v1) → null_le [0]
if(v0, v1, v2, v3, v4) → null_if [0]
len(v0) → null_len [0]
null_take, null_min, null_sum, null_le, null_if, null_len
| 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
null_take => 0
null_min => 0
null_sum => 0
null_le => 0
null_if => 0
null_len => 0
addList(z', z'') -{ 1 }→ if(le(0, min(len(x), len(y))), 0, x, y, 0) :|: z' = x, z'' = y, x >= 0, y >= 0
if(z', z'', z1, z2, z3) -{ 1 }→ z :|: z2 = y, z >= 0, c >= 0, z3 = z, x >= 0, y >= 0, z' = 1, z'' = c, z1 = x
if(z', z'', z1, z2, z3) -{ 1 }→ if(le(1 + c, min(len(xs), len(ys))), 1 + c, xs, ys, 1 + sum(take(c, xs), take(c, ys)) + z) :|: z2 = ys, xs >= 0, z >= 0, z' = 2, c >= 0, ys >= 0, z3 = z, z'' = c, z1 = xs
if(z', z'', z1, z2, z3) -{ 0 }→ 0 :|: z2 = v3, v0 >= 0, v4 >= 0, z1 = v2, v1 >= 0, z'' = v1, z3 = v4, v2 >= 0, v3 >= 0, z' = v0
le(z', z'') -{ 1 }→ le(x, y) :|: z' = 1 + x, x >= 0, y >= 0, z'' = 1 + y
le(z', z'') -{ 1 }→ 2 :|: x >= 0, z'' = x, z' = 0
le(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 1 + x, x >= 0
le(z', z'') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z'' = v1, z' = v0
len(z') -{ 1 }→ 0 :|: z' = 0
len(z') -{ 0 }→ 0 :|: v0 >= 0, z' = v0
len(z') -{ 1 }→ 1 + len(xs) :|: xs >= 0, z' = 1 + x + xs, x >= 0
min(z', z'') -{ 1 }→ min(x, y) :|: z' = 1 + x, x >= 0, y >= 0, z'' = 1 + y
min(z', z'') -{ 1 }→ 0 :|: z'' = y, y >= 0, z' = 0
min(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' = 1 + x, x >= 0
min(z', z'') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z'' = v1, z' = v0
sum(z', z'') -{ 1 }→ x :|: z'' = 0, z' = x, x >= 0
sum(z', z'') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z'' = v1, z' = v0
sum(z', z'') -{ 1 }→ 1 + sum(x, y) :|: z' = x, x >= 0, y >= 0, z'' = 1 + y
take(z', z'') -{ 1 }→ y :|: z'' = 1 + y + ys, ys >= 0, y >= 0, z' = 0
take(z', z'') -{ 1 }→ take(x, ys) :|: z' = 1 + x, z'' = 1 + y + ys, ys >= 0, x >= 0, y >= 0
take(z', z'') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z'' = v1, z' = v0
| eq(start(V, V1, V22, V23, V24),0,[min(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V22, V23, V24),0,[len(V, Out)],[V >= 0]). eq(start(V, V1, V22, V23, V24),0,[sum(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V22, V23, V24),0,[le(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V22, V23, V24),0,[take(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V22, V23, V24),0,[addList(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V22, V23, V24),0,[if(V, V1, V22, V23, V24, Out)],[V >= 0,V1 >= 0,V22 >= 0,V23 >= 0,V24 >= 0]). eq(min(V, V1, Out),1,[],[Out = 0,V1 = V2,V2 >= 0,V = 0]). eq(min(V, V1, Out),1,[],[Out = 0,V1 = 0,V = 1 + V3,V3 >= 0]). eq(min(V, V1, Out),1,[min(V4, V5, Ret)],[Out = Ret,V = 1 + V4,V4 >= 0,V5 >= 0,V1 = 1 + V5]). eq(len(V, Out),1,[],[Out = 0,V = 0]). eq(len(V, Out),1,[len(V6, Ret1)],[Out = 1 + Ret1,V6 >= 0,V = 1 + V6 + V7,V7 >= 0]). eq(sum(V, V1, Out),1,[],[Out = V8,V1 = 0,V = V8,V8 >= 0]). eq(sum(V, V1, Out),1,[sum(V9, V10, Ret11)],[Out = 1 + Ret11,V = V9,V9 >= 0,V10 >= 0,V1 = 1 + V10]). eq(le(V, V1, Out),1,[],[Out = 2,V11 >= 0,V1 = V11,V = 0]). eq(le(V, V1, Out),1,[],[Out = 1,V1 = 0,V = 1 + V12,V12 >= 0]). eq(le(V, V1, Out),1,[le(V13, V14, Ret2)],[Out = Ret2,V = 1 + V13,V13 >= 0,V14 >= 0,V1 = 1 + V14]). eq(take(V, V1, Out),1,[],[Out = V15,V1 = 1 + V15 + V16,V16 >= 0,V15 >= 0,V = 0]). eq(take(V, V1, Out),1,[take(V17, V18, Ret3)],[Out = Ret3,V = 1 + V17,V1 = 1 + V18 + V19,V18 >= 0,V17 >= 0,V19 >= 0]). eq(addList(V, V1, Out),1,[len(V20, Ret010),len(V21, Ret011),min(Ret010, Ret011, Ret01),le(0, Ret01, Ret0),if(Ret0, 0, V20, V21, 0, Ret4)],[Out = Ret4,V = V20,V1 = V21,V20 >= 0,V21 >= 0]). eq(if(V, V1, V22, V23, V24, Out),1,[],[Out = V25,V23 = V26,V25 >= 0,V27 >= 0,V24 = V25,V28 >= 0,V26 >= 0,V = 1,V1 = V27,V22 = V28]). eq(if(V, V1, V22, V23, V24, Out),1,[len(V30, Ret0101),len(V31, Ret0111),min(Ret0101, Ret0111, Ret012),le(1 + V29, Ret012, Ret02),take(V29, V30, Ret4010),take(V29, V31, Ret4011),sum(Ret4010, Ret4011, Ret401),if(Ret02, 1 + V29, V30, V31, 1 + Ret401 + V32, Ret5)],[Out = Ret5,V23 = V31,V30 >= 0,V32 >= 0,V = 2,V29 >= 0,V31 >= 0,V24 = V32,V1 = V29,V22 = V30]). eq(take(V, V1, Out),0,[],[Out = 0,V33 >= 0,V34 >= 0,V1 = V34,V = V33]). eq(min(V, V1, Out),0,[],[Out = 0,V35 >= 0,V36 >= 0,V1 = V36,V = V35]). eq(sum(V, V1, Out),0,[],[Out = 0,V37 >= 0,V38 >= 0,V1 = V38,V = V37]). eq(le(V, V1, Out),0,[],[Out = 0,V39 >= 0,V40 >= 0,V1 = V40,V = V39]). eq(if(V, V1, V22, V23, V24, Out),0,[],[Out = 0,V23 = V41,V42 >= 0,V43 >= 0,V22 = V44,V45 >= 0,V1 = V45,V24 = V43,V44 >= 0,V41 >= 0,V = V42]). eq(len(V, Out),0,[],[Out = 0,V46 >= 0,V = V46]). input_output_vars(min(V,V1,Out),[V,V1],[Out]). input_output_vars(len(V,Out),[V],[Out]). input_output_vars(sum(V,V1,Out),[V,V1],[Out]). input_output_vars(le(V,V1,Out),[V,V1],[Out]). input_output_vars(take(V,V1,Out),[V,V1],[Out]). input_output_vars(addList(V,V1,Out),[V,V1],[Out]). input_output_vars(if(V,V1,V22,V23,V24,Out),[V,V1,V22,V23,V24],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [le/3]
1. recursive : [len/2]
2. recursive : [min/3]
3. recursive : [sum/3]
4. recursive : [take/3]
5. recursive : [if/6]
6. non_recursive : [addList/3]
7. non_recursive : [start/5]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into le/3
1. SCC is partially evaluated into len/2
2. SCC is partially evaluated into min/3
3. SCC is partially evaluated into sum/3
4. SCC is partially evaluated into take/3
5. SCC is partially evaluated into if/6
6. SCC is partially evaluated into addList/3
7. SCC is partially evaluated into start/5
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations le/3
* CE 22 is refined into CE [30]
* CE 20 is refined into CE [31]
* CE 19 is refined into CE [32]
* CE 21 is refined into CE [33]
### Cost equations --> "Loop" of le/3
* CEs [33] --> Loop 21
* CEs [30] --> Loop 22
* CEs [31] --> Loop 23
* CEs [32] --> Loop 24
### Ranking functions of CR le(V,V1,Out)
* RF of phase [21]: [V,V1]
#### Partial ranking functions of CR le(V,V1,Out)
* Partial RF of phase [21]:
- RF of loop [21:1]:
V
V1
### Specialization of cost equations len/2
* CE 13 is refined into CE [34]
* CE 15 is refined into CE [35]
* CE 14 is refined into CE [36]
### Cost equations --> "Loop" of len/2
* CEs [36] --> Loop 25
* CEs [34,35] --> Loop 26
### Ranking functions of CR len(V,Out)
* RF of phase [25]: [V]
#### Partial ranking functions of CR len(V,Out)
* Partial RF of phase [25]:
- RF of loop [25:1]:
V
### Specialization of cost equations min/3
* CE 10 is refined into CE [37]
* CE 9 is refined into CE [38]
* CE 12 is refined into CE [39]
* CE 11 is refined into CE [40]
### Cost equations --> "Loop" of min/3
* CEs [40] --> Loop 27
* CEs [37] --> Loop 28
* CEs [38,39] --> Loop 29
### Ranking functions of CR min(V,V1,Out)
* RF of phase [27]: [V,V1]
#### Partial ranking functions of CR min(V,V1,Out)
* Partial RF of phase [27]:
- RF of loop [27:1]:
V
V1
### Specialization of cost equations sum/3
* CE 18 is refined into CE [41]
* CE 16 is refined into CE [42]
* CE 17 is refined into CE [43]
### Cost equations --> "Loop" of sum/3
* CEs [43] --> Loop 30
* CEs [41] --> Loop 31
* CEs [42] --> Loop 32
### Ranking functions of CR sum(V,V1,Out)
* RF of phase [30]: [V1]
#### Partial ranking functions of CR sum(V,V1,Out)
* Partial RF of phase [30]:
- RF of loop [30:1]:
V1
### Specialization of cost equations take/3
* CE 25 is refined into CE [44]
* CE 23 is refined into CE [45]
* CE 24 is refined into CE [46]
### Cost equations --> "Loop" of take/3
* CEs [46] --> Loop 33
* CEs [44] --> Loop 34
* CEs [45] --> Loop 35
### Ranking functions of CR take(V,V1,Out)
* RF of phase [33]: [V,V1]
#### Partial ranking functions of CR take(V,V1,Out)
* Partial RF of phase [33]:
- RF of loop [33:1]:
V
V1
### Specialization of cost equations if/6
* CE 29 is refined into CE [47]
* CE 27 is refined into CE [48]
* CE 28 is refined into CE [49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,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,99,100,101,102,103,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,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224]
### Cost equations --> "Loop" of if/6
* CEs [69,113,157,201] --> Loop 36
* CEs [65,67,109,111,153,155,197,199] --> Loop 37
* CEs [63,64,70,107,108,114,151,152,158,195,196,202] --> Loop 38
* CEs [91,135,179,223] --> Loop 39
* CEs [87,89,131,133,175,177,219,221] --> Loop 40
* CEs [85,86,92,129,130,136,173,174,180,217,218,224] --> Loop 41
* CEs [51,95,139,183] --> Loop 42
* CEs [52,57,58,96,101,102,140,145,146,184,189,190] --> Loop 43
* CEs [49,53,54,93,97,137,141,142,181,185] --> Loop 44
* CEs [50,55,56,59,60,61,62,66,68,94,98,99,100,103,104,105,106,110,112,138,143,144,147,148,149,150,154,156,182,186,187,188,191,192,193,194,198,200] --> Loop 45
* CEs [73,117,161,205] --> Loop 46
* CEs [74,79,80,118,123,124,162,167,168,206,211,212] --> Loop 47
* CEs [71,75,76,115,119,159,163,164,203,207] --> Loop 48
* CEs [72,77,78,81,82,83,84,88,90,116,120,121,122,125,126,127,128,132,134,160,165,166,169,170,171,172,176,178,204,208,209,210,213,214,215,216,220,222] --> Loop 49
* CEs [47] --> Loop 50
* CEs [48] --> Loop 51
### Ranking functions of CR if(V,V1,V22,V23,V24,Out)
#### Partial ranking functions of CR if(V,V1,V22,V23,V24,Out)
### Specialization of cost equations addList/3
* CE 26 is refined into CE [225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252]
### Cost equations --> "Loop" of addList/3
* CEs [229,236,243,250] --> Loop 52
* CEs [228,235,242,249] --> Loop 53
* CEs [227,234,241,248] --> Loop 54
* CEs [230,237,244,251] --> Loop 55
* CEs [225,226,231,232,233,238,239,240,245,246,247,252] --> Loop 56
### Ranking functions of CR addList(V,V1,Out)
#### Partial ranking functions of CR addList(V,V1,Out)
### Specialization of cost equations start/5
* CE 2 is refined into CE [253]
* CE 3 is refined into CE [254,255]
* CE 4 is refined into CE [256,257,258,259]
* CE 5 is refined into CE [260,261,262,263,264]
* CE 6 is refined into CE [265,266,267]
* CE 7 is refined into CE [268,269,270,271,272]
* CE 8 is refined into CE [273,274,275,276,277,278,279,280,281,282]
### Cost equations --> "Loop" of start/5
* CEs [256,261,275,278] --> Loop 57
* CEs [276,277,279,280,281,282] --> Loop 58
* CEs [273] --> Loop 59
* CEs [253,254,255,257,258,259,260,262,263,264,265,266,267,268,269,270,271,272,274] --> Loop 60
### Ranking functions of CR start(V,V1,V22,V23,V24)
#### Partial ranking functions of CR start(V,V1,V22,V23,V24)
Computing Bounds
=====================================
#### Cost of chains of le(V,V1,Out):
* Chain [[21],24]: 1*it(21)+1
Such that:it(21) =< V
with precondition: [Out=2,V>=1,V1>=V]
* Chain [[21],23]: 1*it(21)+1
Such that:it(21) =< V1
with precondition: [Out=1,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=2,V1>=0]
* Chain [23]: 1
with precondition: [V1=0,Out=1,V>=1]
* Chain [22]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of len(V,Out):
* Chain [[25],26]: 1*it(25)+1
Such that:it(25) =< V
with precondition: [Out>=1,V>=Out]
* Chain [26]: 1
with precondition: [Out=0,V>=0]
#### Cost of chains of min(V,V1,Out):
* Chain [[27],29]: 1*it(27)+1
Such that:it(27) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [[27],28]: 1*it(27)+1
Such that:it(27) =< V1
with precondition: [Out=0,V1>=1,V>=V1+1]
* Chain [29]: 1
with precondition: [Out=0,V>=0,V1>=0]
* Chain [28]: 1
with precondition: [V1=0,Out=0,V>=1]
#### Cost of chains of sum(V,V1,Out):
* Chain [[30],32]: 1*it(30)+1
Such that:it(30) =< V1
with precondition: [V+V1=Out,V>=0,V1>=1]
* Chain [[30],31]: 1*it(30)+0
Such that:it(30) =< Out
with precondition: [V>=0,Out>=1,V1>=Out]
* Chain [32]: 1
with precondition: [V1=0,V=Out,V>=0]
* Chain [31]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of take(V,V1,Out):
* Chain [[33],35]: 1*it(33)+1
Such that:it(33) =< V
with precondition: [V>=1,Out>=0,V1>=Out+V+1]
* Chain [[33],34]: 1*it(33)+0
Such that:it(33) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [35]: 1
with precondition: [V=0,Out>=0,V1>=Out+1]
* Chain [34]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of if(V,V1,V22,V23,V24,Out):
* Chain [51]: 1
with precondition: [V=1,V24=Out,V1>=0,V22>=0,V23>=0,V24>=0]
* Chain [50]: 0
with precondition: [Out=0,V>=0,V1>=0,V22>=0,V23>=0,V24>=0]
* Chain [49,50]: 43*s(11)+74*s(20)+17*s(30)+3*s(207)+6
Such that:aux(56) =< V1
aux(59) =< V1+1
aux(62) =< V22
aux(63) =< V23
s(207) =< aux(56)
s(11) =< aux(62)
s(20) =< aux(63)
s(30) =< aux(59)
with precondition: [V=2,Out=0,V1>=0,V22>=0,V23>=0,V24>=0]
* Chain [48,50]: 18*s(222)+5*s(236)+7
Such that:aux(74) =< V22
aux(76) =< V23
s(222) =< aux(76)
s(236) =< aux(74)
with precondition: [V=2,V1=0,Out=0,V22>=1,V23>=0,V24>=0]
* Chain [47,50]: 30*s(264)+14*s(268)+6
Such that:aux(98) =< V22
aux(99) =< V23
s(268) =< aux(98)
s(264) =< aux(99)
with precondition: [V=2,V1=0,Out=0,V22>=0,V23>=2,V24>=0]
* Chain [46,50]: 4*s(332)+6*s(333)+2*s(338)+7
Such that:aux(104) =< V22+V23
aux(105) =< V23
aux(106) =< V22
s(338) =< aux(106)
s(332) =< aux(104)
s(333) =< aux(105)
with precondition: [V=2,V1=0,Out=0,V22>=1,V23>=2,V24>=0]
* Chain [45,51]: 43*s(353)+74*s(360)+20*s(368)+8
Such that:aux(144) =< V1+1
aux(146) =< V23
aux(147) =< V22
s(368) =< aux(144)
s(353) =< aux(147)
s(360) =< aux(146)
with precondition: [V=2,Out=V24+1,V1>=0,V22>=0,V23>=0,Out>=1]
* Chain [45,50]: 43*s(353)+74*s(360)+20*s(368)+7
Such that:aux(144) =< V1+1
aux(146) =< V23
aux(148) =< V22
s(368) =< aux(144)
s(353) =< aux(148)
s(360) =< aux(146)
with precondition: [V=2,Out=0,V1>=0,V22>=0,V23>=0,V24>=0]
* Chain [44,51]: 18*s(526)+5*s(537)+9
Such that:aux(153) =< V22
aux(154) =< V23
s(537) =< aux(153)
s(526) =< aux(154)
with precondition: [V=2,V1=0,V23>=0,V24>=0,Out>=V24+1,V22+V24>=Out]
* Chain [44,50]: 18*s(526)+5*s(537)+8
Such that:aux(153) =< V22
aux(154) =< V23
s(537) =< aux(153)
s(526) =< aux(154)
with precondition: [V=2,V1=0,Out=0,V22>=1,V23>=0,V24>=0]
* Chain [43,51]: 12*s(559)+14*s(562)+18*s(568)+8
Such that:aux(168) =< V23
aux(166) =< -V24+Out
aux(169) =< V22
s(559) =< aux(166)
s(562) =< aux(169)
s(568) =< aux(168)
with precondition: [V=2,V1=0,V22>=0,V24>=0,Out>=V24+2,V23+V24>=Out]
* Chain [43,50]: 30*s(559)+14*s(562)+7
Such that:aux(170) =< V22
aux(171) =< V23
s(559) =< aux(171)
s(562) =< aux(170)
with precondition: [V=2,V1=0,Out=0,V22>=0,V23>=2,V24>=0]
* Chain [42,51]: 4*s(615)+6*s(616)+2*s(620)+9
Such that:aux(175) =< V22
aux(176) =< V23
aux(174) =< -V24+Out
s(615) =< aux(174)
s(620) =< aux(175)
s(616) =< aux(176)
with precondition: [V=2,V1=0,V22>=1,V23>=2,V24>=0,Out>=V24+2,V22+V23+V24>=Out+1]
* Chain [42,50]: 4*s(615)+6*s(616)+2*s(620)+8
Such that:aux(175) =< V22
aux(174) =< V22+V23
aux(176) =< V23
s(615) =< aux(174)
s(620) =< aux(175)
s(616) =< aux(176)
with precondition: [V=2,V1=0,Out=0,V22>=1,V23>=2,V24>=0]
* Chain [41,50]: 14*s(632)+6*s(633)+12*s(634)+10*s(644)+18*s(647)+6
Such that:aux(200) =< -V1+V23
aux(197) =< V1
aux(201) =< V1+1
aux(204) =< V22
aux(205) =< V23
s(644) =< aux(197)
s(632) =< aux(204)
s(634) =< aux(200)
s(633) =< aux(201)
s(647) =< aux(205)
with precondition: [V=2,Out=0,V1>=1,V22>=0,V24>=0,V23>=V1+2]
* Chain [40,50]: 4*s(716)+16*s(717)+8*s(733)+4*s(735)+7
Such that:aux(218) =< V1
aux(221) =< V1+1
aux(224) =< V22
aux(225) =< V23
s(733) =< aux(218)
s(735) =< aux(224)
s(716) =< aux(221)
s(717) =< aux(225)
with precondition: [V=2,Out=0,V1>=1,V23>=0,V24>=0,V22>=V1+1]
* Chain [39,50]: 4*s(764)+2*s(766)+6*s(767)+4*s(771)+2*s(773)+2*s(774)+7
Such that:aux(237) =< -2*V1+V22+V23
aux(234) =< -V1+V23
aux(235) =< V1
aux(238) =< V1+1
aux(236) =< V22
aux(239) =< V23
s(766) =< aux(234)
s(774) =< aux(236)
s(773) =< aux(237)
s(764) =< aux(235)
s(767) =< aux(239)
s(771) =< aux(238)
with precondition: [V=2,Out=0,V1>=1,V24>=0,V22>=V1+1,V23>=V1+2]
* Chain [38,51]: 14*s(791)+10*s(792)+12*s(793)+18*s(804)+6*s(808)+8
Such that:aux(254) =< V1
aux(258) =< V1+1
aux(257) =< -V24+Out
aux(261) =< V22
aux(262) =< V23
s(808) =< aux(254)
s(791) =< aux(261)
s(793) =< aux(257)
s(792) =< aux(258)
s(804) =< aux(262)
with precondition: [V=2,V1>=1,V22>=0,V24>=0,Out>=V24+2,V23+V24>=Out+V1]
* Chain [38,50]: 14*s(791)+10*s(792)+12*s(793)+18*s(804)+6*s(808)+7
Such that:aux(257) =< -V1+V23
aux(254) =< V1
aux(258) =< V1+1
aux(263) =< V22
aux(264) =< V23
s(808) =< aux(254)
s(791) =< aux(263)
s(793) =< aux(257)
s(792) =< aux(258)
s(804) =< aux(264)
with precondition: [V=2,Out=0,V1>=1,V22>=0,V24>=0,V23>=V1+2]
* Chain [37,51]: 9*s(863)+16*s(864)+4*s(879)+3*s(893)+9
Such that:aux(273) =< V1
aux(274) =< V1+1
aux(275) =< V22
aux(276) =< V23
s(893) =< aux(273)
s(863) =< aux(274)
s(879) =< aux(275)
s(864) =< aux(276)
with precondition: [V=2,V1>=1,V23>=0,V24>=0,Out>=V24+1,V22+V24>=Out+V1]
* Chain [37,50]: 9*s(863)+16*s(864)+4*s(879)+3*s(893)+8
Such that:aux(273) =< V1
aux(274) =< V1+1
aux(275) =< V22
aux(276) =< V23
s(893) =< aux(273)
s(863) =< aux(274)
s(879) =< aux(275)
s(864) =< aux(276)
with precondition: [V=2,Out=0,V1>=1,V23>=0,V24>=0,V22>=V1+1]
* Chain [36,51]: 4*s(903)+4*s(905)+6*s(906)+4*s(909)+2*s(912)+9
Such that:aux(283) =< V1
aux(286) =< V1+1
aux(284) =< V22
aux(285) =< -V24+Out
aux(287) =< V23
s(912) =< aux(284)
s(905) =< aux(285)
s(909) =< aux(283)
s(906) =< aux(287)
s(903) =< aux(286)
with precondition: [V=2,V1>=1,V24>=0,V22>=V1+1,V23>=V1+2,Out>=V24+2,V22+V23+V24>=2*V1+Out+1]
* Chain [36,50]: 4*s(903)+4*s(905)+6*s(906)+4*s(909)+2*s(912)+8
Such that:aux(285) =< -2*V1+V22+V23
aux(283) =< V1
aux(286) =< V1+1
aux(284) =< V22
aux(288) =< V23
s(912) =< aux(284)
s(905) =< aux(285)
s(909) =< aux(283)
s(906) =< aux(288)
s(903) =< aux(286)
with precondition: [V=2,Out=0,V1>=1,V24>=0,V22>=V1+1,V23>=V1+2]
#### Cost of chains of addList(V,V1,Out):
* Chain [56]: 1310*s(1034)+112*s(1035)+2770*s(1037)+592*s(1038)+13
Such that:aux(328) =< 1
aux(329) =< V
aux(330) =< V+V1
aux(331) =< V1
s(1034) =< aux(329)
s(1035) =< aux(330)
s(1037) =< aux(331)
s(1038) =< aux(328)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [55]: 80*s(1198)+174*s(1199)+302*s(1200)+13
Such that:aux(336) =< 1
aux(337) =< V
aux(338) =< V1
s(1198) =< aux(336)
s(1199) =< aux(337)
s(1200) =< aux(338)
with precondition: [Out=1,V>=0,V1>=0]
* Chain [54]: 126*s(1234)+58*s(1235)+13
Such that:aux(345) =< V
aux(346) =< V1
s(1235) =< aux(345)
s(1234) =< aux(346)
with precondition: [V>=0,Out>=2,V1>=Out]
* Chain [53]: 16*s(1270)+10*s(1271)+30*s(1272)+14
Such that:aux(351) =< V
aux(352) =< V+V1
aux(353) =< V1
s(1270) =< aux(352)
s(1271) =< aux(351)
s(1272) =< aux(353)
with precondition: [V>=1,V1>=2,Out>=2,V+V1>=Out+1]
* Chain [52]: 22*s(1305)+78*s(1306)+14
Such that:aux(358) =< V
aux(359) =< V1
s(1305) =< aux(358)
s(1306) =< aux(359)
with precondition: [V1>=0,Out>=1,V>=Out]
#### Cost of chains of start(V,V1,V22,V23,V24):
* Chain [60]: 3351*s(1330)+1577*s(1331)+128*s(1344)+672*s(1346)+158*s(1374)+6*s(1375)+300*s(1377)+74*s(1378)+26*s(1379)+8*s(1380)+14
Such that:s(1367) =< -2*V1+V22+V23
s(1368) =< -V1+V23
s(1370) =< V1+1
s(1371) =< V22
s(1372) =< V22+V23
s(1373) =< V23
aux(360) =< 1
aux(361) =< V
aux(362) =< V+V1
aux(363) =< V1
s(1331) =< aux(361)
s(1330) =< aux(363)
s(1344) =< aux(362)
s(1346) =< aux(360)
s(1374) =< s(1371)
s(1375) =< s(1367)
s(1377) =< s(1373)
s(1378) =< s(1370)
s(1379) =< s(1368)
s(1380) =< s(1372)
with precondition: [V>=0]
* Chain [59]: 1
with precondition: [V=1,V1>=0,V22>=0,V23>=0,V24>=0]
* Chain [58]: 150*s(1384)+79*s(1385)+4*s(1390)+43*s(1396)+13*s(1404)+12*s(1406)+4*s(1423)+9
Such that:s(1420) =< -2*V1+V22+V23
s(1401) =< -V1+V23
s(1389) =< V22+V23
aux(365) =< V1
aux(366) =< V1+1
aux(367) =< V22
aux(368) =< V23
s(1385) =< aux(367)
s(1423) =< s(1420)
s(1404) =< aux(365)
s(1384) =< aux(368)
s(1396) =< aux(366)
s(1406) =< s(1401)
s(1390) =< s(1389)
with precondition: [V=2,V1>=0,V22>=0,V23>=0,V24>=0]
* Chain [57]: 15*s(1429)+54*s(1430)+9
Such that:aux(369) =< V22
aux(370) =< V23
s(1429) =< aux(369)
s(1430) =< aux(370)
with precondition: [V1=0,V>=0]
Closed-form bounds of start(V,V1,V22,V23,V24):
-------------------------------------
* Chain [60] with precondition: [V>=0]
- Upper bound: 1577*V+686+nat(V1)*3351+nat(V22)*158+nat(V23)*300+nat(V+V1)*128+nat(V1+1)*74+nat(V22+V23)*8+nat(-V1+V23)*26+nat(-2*V1+V22+V23)*6
- Complexity: n
* Chain [59] with precondition: [V=1,V1>=0,V22>=0,V23>=0,V24>=0]
- Upper bound: 1
- Complexity: constant
* Chain [58] with precondition: [V=2,V1>=0,V22>=0,V23>=0,V24>=0]
- Upper bound: 56*V1+83*V22+154*V23+52+nat(-V1+V23)*12+nat(-2*V1+V22+V23)*4
- Complexity: n
* Chain [57] with precondition: [V1=0,V>=0]
- Upper bound: nat(V22)*15+9+nat(V23)*54
- Complexity: n
### Maximum cost of start(V,V1,V22,V23,V24): 1577*V+677+nat(V1)*3338+nat(V22)*79+nat(V23)*150+nat(V+V1)*128+nat(V1+1)*31+nat(V22+V23)*4+nat(-V1+V23)*14+nat(-2*V1+V22+V23)*2+ (nat(V22)*64+nat(V1)*13+nat(V23)*96+nat(V1+1)*43+nat(V22+V23)*4+nat(-V1+V23)*12+nat(-2*V1+V22+V23)*4)+ (nat(V22)*15+8+nat(V23)*54)+1
Asymptotic class: n
* Total analysis performed in 4256 ms.