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), 19 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 865 ms)
↳10 BOUNDS(1, n^1)
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
logarithm(x) → ifa(lt(0, x), x)
ifa(true, x) → help(x, 1)
ifa(false, x) → logZeroError
help(x, y) → ifb(lt(y, x), x, y)
ifb(true, x, y) → help(half(x), s(y))
ifb(false, x, y) → y
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
lt(0, s(x)) → true [1]
lt(x, 0) → false [1]
lt(s(x), s(y)) → lt(x, y) [1]
logarithm(x) → ifa(lt(0, x), x) [1]
ifa(true, x) → help(x, 1) [1]
ifa(false, x) → logZeroError [1]
help(x, y) → ifb(lt(y, x), x, y) [1]
ifb(true, x, y) → help(half(x), s(y)) [1]
ifb(false, x, y) → y [1]
half(0) → 0 [1]
half(s(0)) → 0 [1]
half(s(s(x))) → s(half(x)) [1]
lt(0, s(x)) → true [1]
lt(x, 0) → false [1]
lt(s(x), s(y)) → lt(x, y) [1]
logarithm(x) → ifa(lt(0, x), x) [1]
ifa(true, x) → help(x, 1) [1]
ifa(false, x) → logZeroError [1]
help(x, y) → ifb(lt(y, x), x, y) [1]
ifb(true, x, y) → help(half(x), s(y)) [1]
ifb(false, x, y) → y [1]
half(0) → 0 [1]
half(s(0)) → 0 [1]
half(s(s(x))) → s(half(x)) [1]
| lt :: 0:s:1:logZeroError → 0:s:1:logZeroError → true:false 0 :: 0:s:1:logZeroError s :: 0:s:1:logZeroError → 0:s:1:logZeroError true :: true:false false :: true:false logarithm :: 0:s:1:logZeroError → 0:s:1:logZeroError ifa :: true:false → 0:s:1:logZeroError → 0:s:1:logZeroError help :: 0:s:1:logZeroError → 0:s:1:logZeroError → 0:s:1:logZeroError 1 :: 0:s:1:logZeroError logZeroError :: 0:s:1:logZeroError ifb :: true:false → 0:s:1:logZeroError → 0:s:1:logZeroError → 0:s:1:logZeroError half :: 0:s:1:logZeroError → 0:s:1:logZeroError |
lt(v0, v1) → null_lt [0]
half(v0) → null_half [0]
ifa(v0, v1) → null_ifa [0]
ifb(v0, v1, v2) → null_ifb [0]
null_lt, null_half, null_ifa, null_ifb
| 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
1 => 1
logZeroError => 2
null_lt => 0
null_half => 0
null_ifa => 0
null_ifb => 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
half(z) -{ 1 }→ 1 + half(x) :|: x >= 0, z = 1 + (1 + x)
help(z, z') -{ 1 }→ ifb(lt(y, x), x, y) :|: x >= 0, y >= 0, z = x, z' = y
ifa(z, z') -{ 1 }→ help(x, 1) :|: z = 2, z' = x, x >= 0
ifa(z, z') -{ 1 }→ 2 :|: z' = x, z = 1, x >= 0
ifa(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
ifb(z, z', z'') -{ 1 }→ y :|: z' = x, z'' = y, z = 1, x >= 0, y >= 0
ifb(z, z', z'') -{ 1 }→ help(half(x), 1 + y) :|: z = 2, z' = x, z'' = y, x >= 0, y >= 0
ifb(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
logarithm(z) -{ 1 }→ ifa(lt(0, x), x) :|: x >= 0, z = x
lt(z, z') -{ 1 }→ lt(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
lt(z, z') -{ 1 }→ 2 :|: z' = 1 + x, x >= 0, z = 0
lt(z, z') -{ 1 }→ 1 :|: x >= 0, z = x, z' = 0
lt(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
| eq(start(V, V1, V11),0,[lt(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V11),0,[logarithm(V, Out)],[V >= 0]). eq(start(V, V1, V11),0,[ifa(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V11),0,[help(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V11),0,[ifb(V, V1, V11, Out)],[V >= 0,V1 >= 0,V11 >= 0]). eq(start(V, V1, V11),0,[half(V, Out)],[V >= 0]). eq(lt(V, V1, Out),1,[],[Out = 2,V1 = 1 + V2,V2 >= 0,V = 0]). eq(lt(V, V1, Out),1,[],[Out = 1,V3 >= 0,V = V3,V1 = 0]). eq(lt(V, V1, Out),1,[lt(V4, V5, Ret)],[Out = Ret,V1 = 1 + V5,V4 >= 0,V5 >= 0,V = 1 + V4]). eq(logarithm(V, Out),1,[lt(0, V6, Ret0),ifa(Ret0, V6, Ret1)],[Out = Ret1,V6 >= 0,V = V6]). eq(ifa(V, V1, Out),1,[help(V7, 1, Ret2)],[Out = Ret2,V = 2,V1 = V7,V7 >= 0]). eq(ifa(V, V1, Out),1,[],[Out = 2,V1 = V8,V = 1,V8 >= 0]). eq(help(V, V1, Out),1,[lt(V9, V10, Ret01),ifb(Ret01, V10, V9, Ret3)],[Out = Ret3,V10 >= 0,V9 >= 0,V = V10,V1 = V9]). eq(ifb(V, V1, V11, Out),1,[half(V12, Ret02),help(Ret02, 1 + V13, Ret4)],[Out = Ret4,V = 2,V1 = V12,V11 = V13,V12 >= 0,V13 >= 0]). eq(ifb(V, V1, V11, Out),1,[],[Out = V14,V1 = V15,V11 = V14,V = 1,V15 >= 0,V14 >= 0]). eq(half(V, Out),1,[],[Out = 0,V = 0]). eq(half(V, Out),1,[],[Out = 0,V = 1]). eq(half(V, Out),1,[half(V16, Ret11)],[Out = 1 + Ret11,V16 >= 0,V = 2 + V16]). eq(lt(V, V1, Out),0,[],[Out = 0,V17 >= 0,V18 >= 0,V = V17,V1 = V18]). eq(half(V, Out),0,[],[Out = 0,V19 >= 0,V = V19]). eq(ifa(V, V1, Out),0,[],[Out = 0,V20 >= 0,V21 >= 0,V = V20,V1 = V21]). eq(ifb(V, V1, V11, Out),0,[],[Out = 0,V22 >= 0,V11 = V23,V24 >= 0,V = V22,V1 = V24,V23 >= 0]). input_output_vars(lt(V,V1,Out),[V,V1],[Out]). input_output_vars(logarithm(V,Out),[V],[Out]). input_output_vars(ifa(V,V1,Out),[V,V1],[Out]). input_output_vars(help(V,V1,Out),[V,V1],[Out]). input_output_vars(ifb(V,V1,V11,Out),[V,V1,V11],[Out]). input_output_vars(half(V,Out),[V],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [half/2]
1. recursive : [lt/3]
2. recursive : [help/3,ifb/4]
3. non_recursive : [ifa/3]
4. non_recursive : [logarithm/2]
5. non_recursive : [start/3]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into half/2
1. SCC is partially evaluated into lt/3
2. SCC is partially evaluated into help/3
3. SCC is partially evaluated into ifa/3
4. SCC is partially evaluated into logarithm/2
5. SCC is partially evaluated into start/3
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations half/2
* CE 11 is refined into CE [25]
* CE 10 is refined into CE [26]
* CE 13 is refined into CE [27]
* CE 12 is refined into CE [28]
### Cost equations --> "Loop" of half/2
* CEs [28] --> Loop 17
* CEs [25] --> Loop 18
* CEs [26,27] --> Loop 19
### Ranking functions of CR half(V,Out)
* RF of phase [17]: [V-1]
#### Partial ranking functions of CR half(V,Out)
* Partial RF of phase [17]:
- RF of loop [17:1]:
V-1
### Specialization of cost equations lt/3
* CE 20 is refined into CE [29]
* CE 18 is refined into CE [30]
* CE 17 is refined into CE [31]
* CE 19 is refined into CE [32]
### Cost equations --> "Loop" of lt/3
* CEs [32] --> Loop 20
* CEs [29] --> Loop 21
* CEs [30] --> Loop 22
* CEs [31] --> Loop 23
### Ranking functions of CR lt(V,V1,Out)
* RF of phase [20]: [V,V1]
#### Partial ranking functions of CR lt(V,V1,Out)
* Partial RF of phase [20]:
- RF of loop [20:1]:
V
V1
### Specialization of cost equations help/3
* CE 16 is refined into CE [33,34,35,36]
* CE 15 is refined into CE [37,38]
* CE 14 is refined into CE [39,40,41,42,43]
### Cost equations --> "Loop" of help/3
* CEs [38] --> Loop 24
* CEs [39] --> Loop 25
* CEs [37] --> Loop 26
* CEs [40,41,42,43] --> Loop 27
* CEs [36] --> Loop 28
* CEs [35] --> Loop 29
* CEs [34] --> Loop 30
* CEs [33] --> Loop 31
### Ranking functions of CR help(V,V1,Out)
* RF of phase [28]: [V-1,V/2-V1/2]
#### Partial ranking functions of CR help(V,V1,Out)
* Partial RF of phase [28]:
- RF of loop [28:1]:
V-1
V/2-V1/2
### Specialization of cost equations ifa/3
* CE 24 is refined into CE [44]
* CE 22 is refined into CE [45,46,47,48]
* CE 23 is refined into CE [49]
### Cost equations --> "Loop" of ifa/3
* CEs [47] --> Loop 32
* CEs [44,46] --> Loop 33
* CEs [48] --> Loop 34
* CEs [45] --> Loop 35
* CEs [49] --> Loop 36
### Ranking functions of CR ifa(V,V1,Out)
#### Partial ranking functions of CR ifa(V,V1,Out)
### Specialization of cost equations logarithm/2
* CE 21 is refined into CE [50,51,52,53,54,55]
### Cost equations --> "Loop" of logarithm/2
* CEs [51] --> Loop 37
* CEs [50] --> Loop 38
* CEs [53] --> Loop 39
* CEs [52,54,55] --> Loop 40
### Ranking functions of CR logarithm(V,Out)
#### Partial ranking functions of CR logarithm(V,Out)
### Specialization of cost equations start/3
* CE 4 is refined into CE [56,57,58,59,60]
* CE 2 is refined into CE [61]
* CE 3 is refined into CE [62]
* CE 5 is refined into CE [63,64,65,66,67]
* CE 6 is refined into CE [68,69,70,71]
* CE 7 is refined into CE [72,73,74,75,76]
* CE 8 is refined into CE [77,78,79,80,81,82]
* CE 9 is refined into CE [83,84]
### Cost equations --> "Loop" of start/3
* CEs [75] --> Loop 41
* CEs [56,57,58,59,60] --> Loop 42
* CEs [74] --> Loop 43
* CEs [64,73,79,80] --> Loop 44
* CEs [62,69,72] --> Loop 45
* CEs [61,63,65,66,67,68,70,71,76,77,78,81,82,83,84] --> Loop 46
### Ranking functions of CR start(V,V1,V11)
#### Partial ranking functions of CR start(V,V1,V11)
Computing Bounds
=====================================
#### Cost of chains of half(V,Out):
* Chain [[17],19]: 1*it(17)+1
Such that:it(17) =< 2*Out
with precondition: [Out>=1,V>=2*Out]
* Chain [[17],18]: 1*it(17)+1
Such that:it(17) =< 2*Out
with precondition: [V=2*Out+1,V>=3]
* Chain [19]: 1
with precondition: [Out=0,V>=0]
* Chain [18]: 1
with precondition: [V=1,Out=0]
#### Cost of chains of lt(V,V1,Out):
* Chain [[20],23]: 1*it(20)+1
Such that:it(20) =< V
with precondition: [Out=2,V>=1,V1>=V+1]
* Chain [[20],22]: 1*it(20)+1
Such that:it(20) =< V1
with precondition: [Out=1,V1>=1,V>=V1]
* Chain [[20],21]: 1*it(20)+0
Such that:it(20) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [23]: 1
with precondition: [V=0,Out=2,V1>=1]
* Chain [22]: 1
with precondition: [V1=0,Out=1,V>=0]
* Chain [21]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of help(V,V1,Out):
* Chain [[28],29,27]: 4*it(28)+4*s(6)+1*s(14)+6
Such that:s(14) =< 3*V+V1+1
it(28) =< V/2-V1/2
aux(4) =< 2*V-V1
s(6) =< aux(4)
with precondition: [Out=0,V1>=1,V>=2*V1+4]
* Chain [[28],29,26]: 4*it(28)+1*s(7)+1*s(14)+2*s(15)+7
Such that:s(16) =< 2*V-V1-Out
s(14) =< 3*V+V1-4*Out+1
it(28) =< V/2-V1/2
s(7) =< Out
s(15) =< s(16)
with precondition: [V1>=1,Out>=V1+2,V+8*V1+16>=10*Out]
* Chain [[28],27]: 4*it(28)+4*s(4)+2*s(15)+2
Such that:it(28) =< 4*V
s(16) =< 5*V
aux(5) =< 3*V+V1
s(4) =< aux(5)
s(15) =< s(16)
with precondition: [Out=0,V1>=1,V>=V1+1]
* Chain [[28],24]: 4*it(28)+2*s(14)+2*s(15)+3
Such that:s(16) =< 2*V-V1+Out
it(28) =< V/2-V1/2
aux(6) =< 3*V+V1-Out
s(14) =< aux(6)
s(15) =< s(16)
with precondition: [V1>=1,Out>=V1+1,V+3*V1+3>=4*Out]
* Chain [31,27]: 1*s(6)+6
Such that:s(6) =< 1
with precondition: [V1=0,Out=0,V>=1]
* Chain [31,26]: 7
with precondition: [V1=0,Out=1,V>=1]
* Chain [30,[28],29,27]: 4*it(28)+6*s(6)+1*s(14)+10
Such that:it(28) =< V/4
s(14) =< 3/2*V+2
aux(7) =< V
s(6) =< aux(7)
with precondition: [V1=0,Out=0,V>=12]
* Chain [30,[28],29,26]: 4*it(28)+1*s(7)+1*s(14)+2*s(15)+2*s(19)+11
Such that:s(18) =< V
s(16) =< V-Out
it(28) =< V/4
s(14) =< 3/2*V-4*Out+2
s(7) =< Out
s(15) =< s(16)
s(19) =< s(18)
with precondition: [V1=0,Out>=3,V+48>=20*Out]
* Chain [30,[28],27]: 4*it(28)+4*s(4)+2*s(15)+2*s(19)+6
Such that:s(18) =< V
it(28) =< 2*V
aux(5) =< 3/2*V+1
s(16) =< 5/2*V
s(4) =< aux(5)
s(15) =< s(16)
s(19) =< s(18)
with precondition: [V1=0,Out=0,V>=4]
* Chain [30,[28],24]: 4*it(28)+2*s(14)+2*s(15)+2*s(19)+7
Such that:s(18) =< V
s(16) =< V+Out
it(28) =< V/4
aux(6) =< 3/2*V-Out+1
s(14) =< aux(6)
s(15) =< s(16)
s(19) =< s(18)
with precondition: [V1=0,Out>=2,V+12>=8*Out]
* Chain [30,29,27]: 2*s(6)+2*s(19)+10
Such that:aux(3) =< 2
s(18) =< V
s(6) =< aux(3)
s(19) =< s(18)
with precondition: [V1=0,Out=0,V>=4]
* Chain [30,29,26]: 1*s(7)+2*s(19)+11
Such that:s(7) =< 2
s(18) =< V
s(19) =< s(18)
with precondition: [V1=0,Out=2,V>=4]
* Chain [30,27]: 2*s(4)+1*s(6)+2*s(19)+6
Such that:s(6) =< 1
s(18) =< V
aux(2) =< V/2
s(4) =< aux(2)
s(19) =< s(18)
with precondition: [V1=0,Out=0,V>=2]
* Chain [30,24]: 1*s(17)+2*s(19)+7
Such that:s(17) =< 1
s(18) =< 2
s(19) =< s(18)
with precondition: [V1=0,Out=1,V>=2]
* Chain [29,27]: 2*s(6)+6
Such that:aux(3) =< V1+1
s(6) =< aux(3)
with precondition: [Out=0,V1>=1,V>=V1+1]
* Chain [29,26]: 1*s(7)+7
Such that:s(7) =< Out
with precondition: [V1+1=Out,V1>=1,V>=V1+1]
* Chain [27]: 2*s(4)+1*s(6)+2
Such that:s(6) =< V1
aux(2) =< V
s(4) =< aux(2)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [26]: 3
with precondition: [V=0,V1=Out,V1>=0]
* Chain [25]: 2
with precondition: [V1=0,Out=0,V>=1]
* Chain [24]: 1*s(17)+3
Such that:s(17) =< V
with precondition: [V1=Out,V>=1,V1>=V]
#### Cost of chains of ifa(V,V1,Out):
* Chain [36]: 1
with precondition: [V=1,Out=2,V1>=0]
* Chain [35]: 4
with precondition: [V=2,V1=0,Out=1]
* Chain [34]: 1*s(86)+4
Such that:s(86) =< 1
with precondition: [V=2,V1=1,Out=1]
* Chain [33]: 8*s(88)+1*s(91)+4*s(92)+6*s(95)+4*s(96)+1*s(98)+3*s(100)+14*s(106)+4*s(107)+4*s(108)+2*s(109)+4*s(111)+2*s(112)+11
Such that:aux(14) =< 1
aux(15) =< 2
s(103) =< V1
aux(16) =< 2*V1
s(90) =< 3*V1+1
s(91) =< 3*V1+2
s(92) =< 4*V1
s(93) =< 5*V1
aux(17) =< V1/2
s(96) =< V1/4
s(97) =< 3/2*V1+1
s(98) =< 3/2*V1+2
s(99) =< 5/2*V1
s(100) =< aux(14)
s(88) =< aux(16)
s(95) =< aux(17)
s(106) =< s(103)
s(107) =< aux(15)
s(108) =< s(97)
s(109) =< s(99)
s(111) =< s(90)
s(112) =< s(93)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [32]: 3*s(116)+8*s(120)+2*s(122)+2*s(123)+2*s(124)+8
Such that:s(114) =< 4*V1
s(117) =< 5*V1
s(115) =< 11*V1
s(118) =< V1/2
aux(18) =< 3*V1+2
s(116) =< aux(18)
s(120) =< s(118)
s(122) =< s(114)
s(123) =< s(117)
s(124) =< s(115)
with precondition: [V=2,Out>=2,V1+6>=4*Out]
#### Cost of chains of logarithm(V,Out):
* Chain [40]: 2*s(130)+8*s(131)+8*s(134)+2*s(136)+17*s(138)+16*s(139)+12*s(140)+29*s(141)+14*s(142)+8*s(143)+4*s(144)+8*s(145)+4*s(146)+13
Such that:aux(23) =< 1
aux(24) =< 2
aux(25) =< V
aux(26) =< 2*V
aux(27) =< 3*V+1
aux(28) =< 3*V+2
aux(29) =< 4*V
aux(30) =< 5*V
aux(31) =< V/2
aux(32) =< V/4
aux(33) =< 3/2*V+1
aux(34) =< 3/2*V+2
aux(35) =< 5/2*V
s(130) =< aux(28)
s(131) =< aux(29)
s(134) =< aux(32)
s(136) =< aux(34)
s(142) =< aux(24)
s(138) =< aux(23)
s(139) =< aux(26)
s(140) =< aux(31)
s(141) =< aux(25)
s(143) =< aux(33)
s(144) =< aux(35)
s(145) =< aux(27)
s(146) =< aux(30)
with precondition: [Out=0,V>=0]
* Chain [39]: 3
with precondition: [V=0,Out=2]
* Chain [38]: 1*s(192)+6
Such that:s(192) =< 1
with precondition: [V=1,Out=1]
* Chain [37]: 3*s(198)+8*s(199)+2*s(200)+2*s(201)+2*s(202)+10
Such that:s(197) =< 3*V+2
s(193) =< 4*V
s(194) =< 5*V
s(195) =< 11*V
s(196) =< V/2
s(198) =< s(197)
s(199) =< s(196)
s(200) =< s(193)
s(201) =< s(194)
s(202) =< s(195)
with precondition: [Out>=2,V+6>=4*Out]
#### Cost of chains of start(V,V1,V11):
* Chain [46]: 17*s(203)+47*s(205)+5*s(219)+14*s(220)+12*s(221)+3*s(222)+20*s(223)+22*s(224)+20*s(225)+22*s(226)+12*s(228)+6*s(229)+8*s(230)+10*s(231)+2*s(241)+1*s(247)+4*s(248)+4*s(251)+1*s(253)+8*s(256)+6*s(257)+4*s(260)+2*s(261)+4*s(262)+2*s(263)+4*s(268)+12*s(272)+4*s(287)+4*s(288)+2*s(290)+2*s(299)+2*s(301)+13
Such that:s(266) =< 2*V-V1
s(210) =< 3*V+1
s(267) =< 3*V+V1
s(291) =< 4*V-2*V1
s(235) =< 11*V
s(292) =< 11*V-3*V1+1
s(278) =< V1+1
s(245) =< 2*V1
s(246) =< 3*V1+1
s(247) =< 3*V1+2
s(248) =< 4*V1
s(249) =< 5*V1
s(250) =< V1/2
s(251) =< V1/4
s(252) =< 3/2*V1+1
s(253) =< 3/2*V1+2
s(254) =< 5/2*V1
aux(37) =< 1
aux(38) =< 2
aux(39) =< V
aux(40) =< 2*V
aux(41) =< 3*V+2
aux(42) =< 3*V+V1+1
aux(43) =< 4*V
aux(44) =< 5*V
aux(45) =< V/2
aux(46) =< V/2-V1/2
aux(47) =< V/4
aux(48) =< 3/2*V+1
aux(49) =< 3/2*V+2
aux(50) =< 5/2*V
aux(51) =< V1
s(205) =< aux(39)
s(225) =< aux(40)
s(268) =< aux(42)
s(220) =< aux(43)
s(272) =< aux(46)
s(221) =< aux(47)
s(222) =< aux(49)
s(203) =< aux(51)
s(219) =< aux(41)
s(223) =< aux(38)
s(224) =< aux(37)
s(226) =< aux(45)
s(228) =< aux(48)
s(229) =< aux(50)
s(230) =< s(210)
s(231) =< aux(44)
s(256) =< s(245)
s(257) =< s(250)
s(260) =< s(252)
s(261) =< s(254)
s(262) =< s(246)
s(263) =< s(249)
s(287) =< s(266)
s(288) =< s(267)
s(290) =< s(278)
s(241) =< s(235)
s(299) =< s(291)
s(301) =< s(292)
with precondition: [V>=0]
* Chain [45]: 7
with precondition: [V=1]
* Chain [44]: 1*s(306)+2*s(309)+8*s(314)+6*s(315)+2*s(316)+2*s(317)+2*s(318)+12
Such that:s(306) =< 2
s(312) =< V
s(307) =< 2*V
s(313) =< V/4
aux(52) =< 3/2*V+2
s(310) =< 5/2*V+1
s(308) =< 11/2*V+2
s(309) =< aux(52)
s(314) =< s(313)
s(315) =< s(312)
s(316) =< s(310)
s(317) =< s(308)
s(318) =< s(307)
with precondition: [V1=0,V>=0]
* Chain [43]: 1*s(319)+4
Such that:s(319) =< 1
with precondition: [V=2,V1=1]
* Chain [42]: 5*s(324)+4*s(328)+5*s(331)+7*s(333)+8*s(337)+4*s(343)+8*s(348)+4*s(353)+4*s(354)+12*s(357)+4*s(358)+1*s(360)+2*s(367)+14*s(368)+4*s(370)+2*s(371)+4*s(372)+4*s(373)+4*s(374)+2*s(386)+2*s(388)+2*s(390)+12
Such that:s(351) =< V1-V11
s(354) =< 2*V1
s(378) =< 2*V1-2*V11
s(365) =< V1/2
s(356) =< V1/4
s(358) =< V1/8
s(352) =< 3/2*V1+V11+1
s(359) =< 3/4*V1+1
s(360) =< 3/4*V1+2
s(361) =< 5/4*V1
s(379) =< 11/2*V1-3*V11
s(322) =< -V11
s(389) =< 2*V11+2
s(328) =< -V11/2
aux(60) =< 1
aux(61) =< 2
aux(62) =< V1
aux(63) =< V1/4-V11/2
aux(64) =< 3/2*V1+V11+2
aux(65) =< 5/2*V1
aux(66) =< V11+1
aux(67) =< V11+2
s(357) =< aux(63)
s(353) =< aux(64)
s(333) =< aux(66)
s(348) =< aux(62)
s(337) =< aux(60)
s(367) =< s(356)
s(368) =< s(365)
s(331) =< aux(61)
s(370) =< s(359)
s(371) =< s(361)
s(372) =< s(351)
s(373) =< s(352)
s(374) =< aux(65)
s(324) =< aux(67)
s(386) =< s(378)
s(388) =< s(379)
s(343) =< s(322)
s(390) =< s(389)
with precondition: [V=2,V1>=0,V11>=0]
* Chain [41]: 3*s(397)+8*s(398)+2*s(399)+2*s(400)+2*s(401)+8
Such that:s(396) =< 3*V1+2
s(392) =< 4*V1
s(393) =< 5*V1
s(394) =< 11*V1
s(395) =< V1/2
s(397) =< s(396)
s(398) =< s(395)
s(399) =< s(392)
s(400) =< s(393)
s(401) =< s(394)
with precondition: [V=2,V1>=2]
Closed-form bounds of start(V,V1,V11):
-------------------------------------
* Chain [46] with precondition: [V>=0]
- Upper bound: 47*V+75+nat(V1)*17+40*V+nat(2*V1)*8+56*V+nat(4*V1)*4+50*V+nat(5*V1)*2+22*V+15*V+nat(5/2*V1)*2+nat(V1+1)*2+nat(3*V+V1)*4+ (24*V+8)+ (15*V+10)+nat(3*V1+1)*4+nat(3*V1+2)+ (18*V+12)+ (9/2*V+6)+nat(3/2*V1+1)*4+nat(3/2*V1+2)+nat(3*V+V1+1)*4+nat(11*V-3*V1+1)*2+nat(2*V-V1)*4+nat(4*V-2*V1)*2+nat(V/2-V1/2)*12+11*V+3*V+nat(V1/2)*6+nat(V1/4)*4
- Complexity: n
* Chain [45] with precondition: [V=1]
- Upper bound: 7
- Complexity: constant
* Chain [44] with precondition: [V1=0,V>=0]
- Upper bound: 31*V+24
- Complexity: n
* Chain [43] with precondition: [V=2,V1=1]
- Upper bound: 5
- Complexity: constant
* Chain [42] with precondition: [V=2,V1>=0,V11>=0]
- Upper bound: V1/2+ (V1/2+ (177/4*V1+24*V11+69+nat(V1-V11)*4+nat(2*V1-2*V11)*2+nat(11/2*V1-3*V11)*2+nat(V1/4-V11/2)*12+7*V1))
- Complexity: n
* Chain [41] with precondition: [V=2,V1>=2]
- Upper bound: 53*V1+14
- Complexity: n
### Maximum cost of start(V,V1,V11): max([31*V+19,nat(V1/2)*6+3+max([nat(5*V1)*2+nat(4*V1)*2+nat(11*V1)*2+nat(3*V1+2)*3+nat(V1/2)*2,nat(V1)*8+22+nat(2*V1)*4+nat(5/2*V1)*2+nat(V1/4)*2+max([nat(5/4*V1)*2+nat(5/2*V1)*2+nat(V11+1)*7+nat(V11+2)*5+nat(2*V11+2)*2+nat(3/4*V1+1)*4+nat(3/4*V1+2)+nat(3/2*V1+V11+1)*4+nat(3/2*V1+V11+2)*4+nat(V1-V11)*4+nat(2*V1-2*V11)*2+nat(11/2*V1-3*V11)*2+nat(V1/4-V11/2)*12+nat(V1/2)*8+nat(V1/8)*4,47*V+45+nat(V1)*9+40*V+nat(2*V1)*4+56*V+nat(4*V1)*4+50*V+nat(5*V1)*2+22*V+15*V+nat(V1+1)*2+nat(3*V+V1)*4+ (24*V+8)+ (15*V+10)+nat(3*V1+1)*4+nat(3*V1+2)+ (18*V+12)+ (9/2*V+6)+nat(3/2*V1+1)*4+nat(3/2*V1+2)+nat(3*V+V1+1)*4+nat(11*V-3*V1+1)*2+nat(2*V-V1)*4+nat(4*V-2*V1)*2+nat(V/2-V1/2)*12+11*V+3*V+nat(V1/4)*2])])])+5
Asymptotic class: n
* Total analysis performed in 767 ms.