The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

f(true, x, y, z) → f(gt(x, plus(y, z)), x, s(y), z)
f(true, x, y, z) → f(gt(x, plus(y, z)), x, y, s(z))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

f(true, x, y, z) → f(gt(x, plus(y, z)), x, s(y), z) [1]
f(true, x, y, z) → f(gt(x, plus(y, z)), x, y, s(z)) [1]
plus(n, 0) → n [1]
plus(n, s(m)) → s(plus(n, m)) [1]
gt(0, v) → false [1]
gt(s(u), 0) → true [1]
gt(s(u), s(v)) → gt(u, v) [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

f(true, x, y, z) → f(gt(x, plus(y, z)), x, s(y), z) [1]
f(true, x, y, z) → f(gt(x, plus(y, z)), x, y, s(z)) [1]
plus(n, 0) → n [1]
plus(n, s(m)) → s(plus(n, m)) [1]
gt(0, v) → false [1]
gt(s(u), 0) → true [1]
gt(s(u), s(v)) → gt(u, v) [1]

The TRS has the following type information:

f :: true:false → s:0 → s:0 → s:0 → f true :: true:false gt :: s:0 → s:0 → true:false plus :: s:0 → s:0 → s:0 s :: s:0 → s:0 0 :: s:0 false :: true:false

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

f(v0, v1, v2, v3) → null_f [0]

And the following fresh constants:

null_f

(6) Obligation:

Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: f(true, x, y, z) → f(gt(x, plus(y, z)), x, s(y), z) [1] f(true, x, y, z) → f(gt(x, plus(y, z)), x, y, s(z)) [1] plus(n, 0) → n [1] plus(n, s(m)) → s(plus(n, m)) [1] gt(0, v) → false [1] gt(s(u), 0) → true [1] gt(s(u), s(v)) → gt(u, v) [1] f(v0, v1, v2, v3) → null_f [0] The TRS has the following type information: f :: true:false → s:0 → s:0 → s:0 → null_f true :: true:false gt :: s:0 → s:0 → true:false plus :: s:0 → s:0 → s:0 s :: s:0 → s:0 0 :: s:0 false :: true:false null_f :: null_f Rewrite Strategy: INNERMOST

(7) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

true => 1
0 => 0
false => 0
null_f => 0

(8) Obligation:

Complexity RNTS consisting of the following rules:

f(z', z'', z1, z2) -{ 1 }→ f(gt(x, plus(y, z)), x, y, 1 + z) :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 1
f(z', z'', z1, z2) -{ 1 }→ f(gt(x, plus(y, z)), x, 1 + y, z) :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 1
f(z', z'', z1, z2) -{ 0 }→ 0 :|: z2 = v3, v0 >= 0, z1 = v2, v1 >= 0, z'' = v1, v2 >= 0, v3 >= 0, z' = v0
gt(z', z'') -{ 1 }→ gt(u, v) :|: v >= 0, z' = 1 + u, z'' = 1 + v, u >= 0
gt(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 1 + u, u >= 0
gt(z', z'') -{ 1 }→ 0 :|: z'' = v, v >= 0, z' = 0
plus(z', z'') -{ 1 }→ n :|: z'' = 0, n >= 0, z' = n
plus(z', z'') -{ 1 }→ 1 + plus(n, m) :|: n >= 0, z'' = 1 + m, z' = n, m >= 0

Only complete derivations are relevant for the runtime complexity.

(9) CompleteCoflocoProof (EQUIVALENT transformation)

Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V1, V2, V3),0,[f(V, V1, V2, V3, Out)],[V >= 0,V1 >= 0,V2 >= 0,V3 >= 0]). eq(start(V, V1, V2, V3),0,[plus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2, V3),0,[gt(V, V1, Out)],[V >= 0,V1 >= 0]). eq(f(V, V1, V2, V3, Out),1,[plus(V5, V6, Ret01),gt(V4, Ret01, Ret0),f(Ret0, V4, 1 + V5, V6, Ret)],[Out = Ret,V2 = V5,V6 >= 0,V3 = V6,V4 >= 0,V5 >= 0,V1 = V4,V = 1]). eq(f(V, V1, V2, V3, Out),1,[plus(V8, V9, Ret011),gt(V7, Ret011, Ret02),f(Ret02, V7, V8, 1 + V9, Ret1)],[Out = Ret1,V2 = V8,V9 >= 0,V3 = V9,V7 >= 0,V8 >= 0,V1 = V7,V = 1]). eq(plus(V, V1, Out),1,[],[Out = V10,V1 = 0,V10 >= 0,V = V10]). eq(plus(V, V1, Out),1,[plus(V11, V12, Ret11)],[Out = 1 + Ret11,V11 >= 0,V1 = 1 + V12,V = V11,V12 >= 0]). eq(gt(V, V1, Out),1,[],[Out = 0,V1 = V13,V13 >= 0,V = 0]). eq(gt(V, V1, Out),1,[],[Out = 1,V1 = 0,V = 1 + V14,V14 >= 0]). eq(gt(V, V1, Out),1,[gt(V15, V16, Ret2)],[Out = Ret2,V16 >= 0,V = 1 + V15,V1 = 1 + V16,V15 >= 0]). eq(f(V, V1, V2, V3, Out),0,[],[Out = 0,V3 = V17,V18 >= 0,V2 = V19,V20 >= 0,V1 = V20,V19 >= 0,V17 >= 0,V = V18]). input_output_vars(f(V,V1,V2,V3,Out),[V,V1,V2,V3],[Out]). input_output_vars(plus(V,V1,Out),[V,V1],[Out]). input_output_vars(gt(V,V1,Out),[V,V1],[Out]).

CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components
0. recursive : [gt/3]
1. recursive : [plus/3]
2. recursive : [f/5]
3. non_recursive : [start/4]

#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into gt/3
1. SCC is partially evaluated into plus/3
2. SCC is partially evaluated into f/5
3. SCC is partially evaluated into start/4

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations gt/3
* CE 12 is refined into CE [13]
* CE 11 is refined into CE [14]
* CE 10 is refined into CE [15]


### Cost equations --> "Loop" of gt/3
* CEs [14] --> Loop 10
* CEs [15] --> Loop 11
* CEs [13] --> Loop 12

### Ranking functions of CR gt(V,V1,Out)
* RF of phase [12]: [V,V1]

#### Partial ranking functions of CR gt(V,V1,Out)
* Partial RF of phase [12]:
- RF of loop [12:1]:
V
V1


### Specialization of cost equations plus/3
* CE 9 is refined into CE [16]
* CE 8 is refined into CE [17]


### Cost equations --> "Loop" of plus/3
* CEs [17] --> Loop 13
* CEs [16] --> Loop 14

### Ranking functions of CR plus(V,V1,Out)
* RF of phase [14]: [V1]

#### Partial ranking functions of CR plus(V,V1,Out)
* Partial RF of phase [14]:
- RF of loop [14:1]:
V1


### Specialization of cost equations f/5
* CE 7 is refined into CE [18]
* CE 6 is refined into CE [19,20,21,22,23,24,25]
* CE 5 is refined into CE [26,27,28,29,30,31,32]


### Cost equations --> "Loop" of f/5
* CEs [25] --> Loop 15
* CEs [32] --> Loop 16
* CEs [24] --> Loop 17
* CEs [31] --> Loop 18
* CEs [22] --> Loop 19
* CEs [29] --> Loop 20
* CEs [21] --> Loop 21
* CEs [28] --> Loop 22
* CEs [27] --> Loop 23
* CEs [20] --> Loop 24
* CEs [23] --> Loop 25
* CEs [30] --> Loop 26
* CEs [19] --> Loop 27
* CEs [26] --> Loop 28
* CEs [18] --> Loop 29

### Ranking functions of CR f(V,V1,V2,V3,Out)
* RF of phase [15,16]: [V1-V2-V3]
* RF of phase [20]: [V1-V2]

#### Partial ranking functions of CR f(V,V1,V2,V3,Out)
* Partial RF of phase [15,16]:
- RF of loop [15:1]:
V1-V3
- RF of loop [15:1,16:1]:
V1-V2-V3
- RF of loop [16:1]:
V1-V2-1
* Partial RF of phase [20]:
- RF of loop [20:1]:
V1-V2


### Specialization of cost equations start/4
* CE 2 is refined into CE [33,34,35,36,37,38,39,40]
* CE 3 is refined into CE [41,42]
* CE 4 is refined into CE [43,44,45,46]


### Cost equations --> "Loop" of start/4
* CEs [40] --> Loop 30
* CEs [39] --> Loop 31
* CEs [37] --> Loop 32
* CEs [38,42,45,46] --> Loop 33
* CEs [33,35,36] --> Loop 34
* CEs [34,41,44] --> Loop 35
* CEs [43] --> Loop 36

### Ranking functions of CR start(V,V1,V2,V3)

#### Partial ranking functions of CR start(V,V1,V2,V3)


Computing Bounds
=====================================

#### Cost of chains of gt(V,V1,Out):
* Chain [[12],11]: 1*it(12)+1
Such that:it(12) =< V

with precondition: [Out=0,V>=1,V1>=V]

* Chain [[12],10]: 1*it(12)+1
Such that:it(12) =< V1

with precondition: [Out=1,V1>=1,V>=V1+1]

* Chain [11]: 1
with precondition: [V=0,Out=0,V1>=0]

* Chain [10]: 1
with precondition: [V1=0,Out=1,V>=1]


#### Cost of chains of plus(V,V1,Out):
* Chain [[14],13]: 1*it(14)+1
Such that:it(14) =< V1

with precondition: [V+V1=Out,V>=0,V1>=1]

* Chain [13]: 1
with precondition: [V1=0,V=Out,V>=0]


#### Cost of chains of f(V,V1,V2,V3,Out):
* Chain [[20],29]: 3*it(20)+1*s(3)+0
Such that:aux(1) =< V1
it(20) =< V1-V2
s(3) =< it(20)*aux(1)

with precondition: [V=1,V3=0,Out=0,V2>=1,V1>=V2+1]

* Chain [[20],22,29]: 3*it(20)+1*s(3)+1*s(4)+3
Such that:it(20) =< V1-V2
aux(2) =< V1
s(4) =< aux(2)
s(3) =< it(20)*aux(2)

with precondition: [V=1,V3=0,Out=0,V2>=1,V1>=V2+1]

* Chain [[20],21,29]: 3*it(20)+1*s(3)+1*s(5)+3
Such that:it(20) =< V1-V2
aux(3) =< V1
s(5) =< aux(3)
s(3) =< it(20)*aux(3)

with precondition: [V=1,V3=0,Out=0,V2>=1,V1>=V2+1]

* Chain [[20],19,[15,16],29]: 7*it(15)+3*it(20)+1*s(3)+2*s(14)+1*s(16)+1*s(17)+3
Such that:it(20) =< V1-V2
aux(13) =< V1
it(15) =< aux(13)
aux(7) =< aux(13)-1
aux(6) =< aux(13)
s(14) =< it(15)*aux(13)
s(16) =< it(15)*aux(7)
s(17) =< it(15)*aux(6)
s(3) =< it(20)*aux(13)

with precondition: [V=1,V3=0,Out=0,V2>=1,V1>=V2+3]

* Chain [[20],19,[15,16],18,29]: 9*it(15)+3*it(20)+1*s(3)+2*s(14)+1*s(16)+1*s(17)+6
Such that:it(20) =< V1-V2
aux(18) =< V1
it(15) =< aux(18)
aux(7) =< aux(18)-1
aux(6) =< aux(18)
s(14) =< it(15)*aux(18)
s(16) =< it(15)*aux(7)
s(17) =< it(15)*aux(6)
s(3) =< it(20)*aux(18)

with precondition: [V=1,V3=0,Out=0,V2>=1,V1>=V2+3]

* Chain [[20],19,[15,16],17,29]: 5*it(15)+3*it(16)+3*it(20)+1*s(3)+2*s(14)+1*s(16)+1*s(17)+1*s(21)+6
Such that:aux(20) =< V1+1
it(20) =< V1-V2+1
aux(23) =< V1
it(15) =< aux(23)
it(16) =< aux(20)
s(21) =< aux(20)
it(16) =< aux(23)
aux(7) =< aux(23)-1
aux(6) =< aux(23)
s(14) =< it(15)*aux(23)
s(16) =< it(16)*aux(7)
s(17) =< it(16)*aux(6)
s(3) =< it(20)*aux(23)

with precondition: [V=1,V3=0,Out=0,V2>=1,V1>=V2+3]

* Chain [[20],19,29]: 3*it(20)+1*s(3)+1*s(18)+3
Such that:it(20) =< V1-V2
aux(24) =< V1
s(18) =< aux(24)
s(3) =< it(20)*aux(24)

with precondition: [V=1,V3=0,Out=0,V2>=1,V1>=V2+2]

* Chain [[20],19,18,29]: 3*it(20)+1*s(3)+2*s(18)+1*s(19)+6
Such that:s(19) =< 1
it(20) =< V1-V2
aux(25) =< V1
s(18) =< aux(25)
s(3) =< it(20)*aux(25)

with precondition: [V=1,V3=0,Out=0,V2>=1,V1>=V2+2]

* Chain [[20],19,17,29]: 3*it(20)+1*s(3)+2*s(18)+1*s(21)+6
Such that:s(21) =< 2
it(20) =< V1-V2
aux(26) =< V1
s(18) =< aux(26)
s(3) =< it(20)*aux(26)

with precondition: [V=1,V3=0,Out=0,V2>=1,V1>=V2+2]

* Chain [[15,16],29]: 3*it(15)+3*it(16)+1*s(14)+1*s(15)+1*s(16)+1*s(17)+0
Such that:aux(4) =< V1
aux(8) =< V1-V2
aux(11) =< V1-V2-V3
it(15) =< aux(11)
it(16) =< aux(11)
it(16) =< aux(8)
aux(7) =< aux(8)-1
aux(6) =< aux(4)
s(14) =< it(15)*aux(8)
s(15) =< it(15)*aux(4)
s(16) =< it(16)*aux(7)
s(17) =< it(16)*aux(6)

with precondition: [V=1,Out=0,V2>=0,V3>=1,V1>=V2+V3+1]

* Chain [[15,16],18,29]: 3*it(15)+3*it(16)+1*s(14)+1*s(15)+1*s(16)+1*s(17)+1*s(19)+1*s(20)+3
Such that:aux(14) =< V1
aux(15) =< V1-V2
aux(16) =< V1-V2-V3
s(20) =< aux(14)
it(16) =< aux(15)
s(19) =< aux(15)
it(15) =< aux(16)
it(16) =< aux(16)
aux(7) =< aux(15)-1
aux(6) =< aux(14)
s(14) =< it(15)*aux(15)
s(15) =< it(15)*aux(14)
s(16) =< it(16)*aux(7)
s(17) =< it(16)*aux(6)

with precondition: [V=1,Out=0,V2>=0,V3>=1,V1>=V2+V3+1]

* Chain [[15,16],17,29]: 3*it(15)+3*it(16)+1*s(14)+1*s(15)+1*s(16)+1*s(17)+1*s(21)+1*s(22)+3
Such that:aux(8) =< V1-V2
aux(19) =< V1
aux(20) =< V1-V2+1
aux(21) =< V1-V2-V3
s(22) =< aux(19)
it(16) =< aux(20)
s(21) =< aux(20)
it(15) =< aux(21)
it(16) =< aux(8)
it(16) =< aux(21)
aux(7) =< aux(8)-1
aux(6) =< aux(19)
s(14) =< it(15)*aux(8)
s(15) =< it(15)*aux(19)
s(16) =< it(16)*aux(7)
s(17) =< it(16)*aux(6)

with precondition: [V=1,Out=0,V2>=0,V3>=1,V1>=V2+V3+1]

* Chain [29]: 0
with precondition: [Out=0,V>=0,V1>=0,V2>=0,V3>=0]

* Chain [28,29]: 3
with precondition: [V=1,V1=0,V3=0,Out=0,V2>=0]

* Chain [27,29]: 3
with precondition: [V=1,V1=0,V3=0,Out=0,V2>=0]

* Chain [26,29]: 1*s(23)+3
Such that:s(23) =< V3

with precondition: [V=1,V1=0,Out=0,V2>=0,V3>=1]

* Chain [25,29]: 1*s(24)+3
Such that:s(24) =< V3+1

with precondition: [V=1,V1=0,Out=0,V2>=0,V3>=1]

* Chain [24,[15,16],29]: 6*it(15)+2*s(14)+1*s(16)+1*s(17)+3
Such that:aux(27) =< V1
it(15) =< aux(27)
aux(7) =< aux(27)-1
aux(6) =< aux(27)
s(14) =< it(15)*aux(27)
s(16) =< it(15)*aux(7)
s(17) =< it(15)*aux(6)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=2]

* Chain [24,[15,16],18,29]: 8*it(15)+2*s(14)+1*s(16)+1*s(17)+6
Such that:aux(28) =< V1
it(15) =< aux(28)
aux(7) =< aux(28)-1
aux(6) =< aux(28)
s(14) =< it(15)*aux(28)
s(16) =< it(15)*aux(7)
s(17) =< it(15)*aux(6)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=2]

* Chain [24,[15,16],17,29]: 4*it(15)+3*it(16)+2*s(14)+1*s(16)+1*s(17)+1*s(21)+6
Such that:aux(20) =< V1+1
aux(29) =< V1
it(15) =< aux(29)
it(16) =< aux(20)
s(21) =< aux(20)
it(16) =< aux(29)
aux(7) =< aux(29)-1
aux(6) =< aux(29)
s(14) =< it(15)*aux(29)
s(16) =< it(16)*aux(7)
s(17) =< it(16)*aux(6)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=2]

* Chain [24,29]: 3
with precondition: [V=1,V2=0,V3=0,Out=0,V1>=1]

* Chain [24,18,29]: 2*s(19)+6
Such that:aux(30) =< 1
s(19) =< aux(30)

with precondition: [V=1,V1=1,V2=0,V3=0,Out=0]

* Chain [24,17,29]: 1*s(21)+1*s(22)+6
Such that:s(22) =< 1
s(21) =< 2

with precondition: [V=1,V1=1,V2=0,V3=0,Out=0]

* Chain [23,[20],29]: 3*it(20)+1*s(3)+3
Such that:aux(31) =< V1
it(20) =< aux(31)
s(3) =< it(20)*aux(31)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=2]

* Chain [23,[20],22,29]: 4*it(20)+1*s(3)+6
Such that:aux(32) =< V1
it(20) =< aux(32)
s(3) =< it(20)*aux(32)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=2]

* Chain [23,[20],21,29]: 4*it(20)+1*s(3)+6
Such that:aux(33) =< V1
it(20) =< aux(33)
s(3) =< it(20)*aux(33)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=2]

* Chain [23,[20],19,[15,16],29]: 10*it(15)+3*s(3)+1*s(16)+1*s(17)+6
Such that:aux(34) =< V1
it(15) =< aux(34)
aux(7) =< aux(34)-1
aux(6) =< aux(34)
s(3) =< it(15)*aux(34)
s(16) =< it(15)*aux(7)
s(17) =< it(15)*aux(6)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=4]

* Chain [23,[20],19,[15,16],18,29]: 12*it(15)+3*s(3)+1*s(16)+1*s(17)+9
Such that:aux(35) =< V1
it(15) =< aux(35)
aux(7) =< aux(35)-1
aux(6) =< aux(35)
s(3) =< it(15)*aux(35)
s(16) =< it(15)*aux(7)
s(17) =< it(15)*aux(6)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=4]

* Chain [23,[20],19,[15,16],17,29]: 8*it(15)+3*it(16)+3*s(3)+1*s(16)+1*s(17)+1*s(21)+9
Such that:aux(20) =< V1+1
aux(36) =< V1
it(15) =< aux(36)
it(16) =< aux(20)
s(21) =< aux(20)
it(16) =< aux(36)
aux(7) =< aux(36)-1
aux(6) =< aux(36)
s(3) =< it(15)*aux(36)
s(16) =< it(16)*aux(7)
s(17) =< it(16)*aux(6)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=4]

* Chain [23,[20],19,29]: 4*it(20)+1*s(3)+6
Such that:aux(37) =< V1
it(20) =< aux(37)
s(3) =< it(20)*aux(37)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=3]

* Chain [23,[20],19,18,29]: 5*it(20)+1*s(3)+1*s(19)+9
Such that:s(19) =< 1
aux(38) =< V1
it(20) =< aux(38)
s(3) =< it(20)*aux(38)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=3]

* Chain [23,[20],19,17,29]: 5*it(20)+1*s(3)+1*s(21)+9
Such that:s(21) =< 2
aux(39) =< V1
it(20) =< aux(39)
s(3) =< it(20)*aux(39)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=3]

* Chain [23,29]: 3
with precondition: [V=1,V2=0,V3=0,Out=0,V1>=1]

* Chain [23,22,29]: 1*s(4)+6
Such that:s(4) =< 1

with precondition: [V=1,V1=1,V2=0,V3=0,Out=0]

* Chain [23,21,29]: 1*s(5)+6
Such that:s(5) =< 1

with precondition: [V=1,V1=1,V2=0,V3=0,Out=0]

* Chain [23,19,[15,16],29]: 6*it(15)+2*s(14)+1*s(16)+1*s(17)+1*s(18)+6
Such that:s(18) =< 1
aux(40) =< V1
it(15) =< aux(40)
aux(7) =< aux(40)-1
aux(6) =< aux(40)
s(14) =< it(15)*aux(40)
s(16) =< it(15)*aux(7)
s(17) =< it(15)*aux(6)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=3]

* Chain [23,19,[15,16],18,29]: 8*it(15)+2*s(14)+1*s(16)+1*s(17)+1*s(18)+9
Such that:s(18) =< 1
aux(41) =< V1
it(15) =< aux(41)
aux(7) =< aux(41)-1
aux(6) =< aux(41)
s(14) =< it(15)*aux(41)
s(16) =< it(15)*aux(7)
s(17) =< it(15)*aux(6)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=3]

* Chain [23,19,[15,16],17,29]: 8*it(15)+2*s(14)+1*s(16)+1*s(17)+1*s(18)+9
Such that:s(18) =< 1
aux(42) =< V1
it(15) =< aux(42)
aux(7) =< aux(42)-1
aux(6) =< aux(42)
s(14) =< it(15)*aux(42)
s(16) =< it(15)*aux(7)
s(17) =< it(15)*aux(6)

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=3]

* Chain [23,19,29]: 1*s(18)+6
Such that:s(18) =< 1

with precondition: [V=1,V2=0,V3=0,Out=0,V1>=2]

* Chain [23,19,18,29]: 2*s(18)+1*s(20)+9
Such that:s(20) =< 2
aux(43) =< 1
s(18) =< aux(43)

with precondition: [V=1,V1=2,V2=0,V3=0,Out=0]

* Chain [23,19,17,29]: 1*s(18)+2*s(21)+9
Such that:s(18) =< 1
aux(44) =< 2
s(21) =< aux(44)

with precondition: [V=1,V1=2,V2=0,V3=0,Out=0]

* Chain [22,29]: 1*s(4)+3
Such that:s(4) =< V1

with precondition: [V=1,V3=0,Out=0,V1>=1,V2>=V1]

* Chain [21,29]: 1*s(5)+3
Such that:s(5) =< V1

with precondition: [V=1,V3=0,Out=0,V1>=1,V2>=V1]

* Chain [19,[15,16],29]: 6*it(15)+1*s(14)+1*s(15)+1*s(16)+1*s(17)+1*s(18)+3
Such that:aux(4) =< V1
s(18) =< V2
aux(12) =< V1-V2
it(15) =< aux(12)
aux(7) =< aux(12)-1
aux(6) =< aux(4)
s(14) =< it(15)*aux(12)
s(15) =< it(15)*aux(4)
s(16) =< it(15)*aux(7)
s(17) =< it(15)*aux(6)

with precondition: [V=1,V3=0,Out=0,V2>=1,V1>=V2+2]

* Chain [19,[15,16],18,29]: 7*it(15)+1*s(14)+1*s(15)+1*s(16)+1*s(17)+1*s(18)+1*s(20)+6
Such that:aux(14) =< V1
s(18) =< V2
aux(17) =< V1-V2
s(20) =< aux(14)
it(15) =< aux(17)
aux(7) =< aux(17)-1
aux(6) =< aux(14)
s(14) =< it(15)*aux(17)
s(15) =< it(15)*aux(14)
s(16) =< it(15)*aux(7)
s(17) =< it(15)*aux(6)

with precondition: [V=1,V3=0,Out=0,V2>=1,V1>=V2+2]

* Chain [19,[15,16],17,29]: 3*it(15)+3*it(16)+1*s(14)+1*s(15)+1*s(16)+1*s(17)+1*s(18)+1*s(21)+1*s(22)+6
Such that:aux(19) =< V1
aux(20) =< V1-V2+1
s(18) =< V2
aux(22) =< V1-V2
s(22) =< aux(19)
it(16) =< aux(20)
s(21) =< aux(20)
it(15) =< aux(22)
it(16) =< aux(22)
aux(7) =< aux(22)-1
aux(6) =< aux(19)
s(14) =< it(15)*aux(22)
s(15) =< it(15)*aux(19)
s(16) =< it(16)*aux(7)
s(17) =< it(16)*aux(6)

with precondition: [V=1,V3=0,Out=0,V2>=1,V1>=V2+2]

* Chain [19,29]: 1*s(18)+3
Such that:s(18) =< V2

with precondition: [V=1,V3=0,Out=0,V2>=1,V1>=V2+1]

* Chain [19,18,29]: 1*s(18)+1*s(19)+1*s(20)+6
Such that:s(19) =< 1
s(18) =< V2
s(20) =< V2+1

with precondition: [V=1,V3=0,Out=0,V1=V2+1,V1>=2]

* Chain [19,17,29]: 1*s(18)+1*s(21)+1*s(22)+6
Such that:s(21) =< 2
s(18) =< V2
s(22) =< V2+1

with precondition: [V=1,V3=0,Out=0,V1=V2+1,V1>=2]

* Chain [18,29]: 1*s(19)+1*s(20)+3
Such that:s(20) =< V1
s(19) =< V3

with precondition: [V=1,Out=0,V1>=1,V2>=0,V3>=1,V2+V3>=V1]

* Chain [17,29]: 1*s(21)+1*s(22)+3
Such that:s(22) =< V1
s(21) =< V3+1

with precondition: [V=1,Out=0,V1>=1,V2>=0,V3>=1,V2+V3>=V1]


#### Cost of chains of start(V,V1,V2,V3):
* Chain [36]: 1
with precondition: [V=0,V1>=0]

* Chain [35]: 1*s(273)+1*s(274)+3
Such that:s(273) =< V3
s(274) =< V3+1

with precondition: [V1=0,V>=0]

* Chain [34]: 10*s(279)+2*s(280)+95*s(281)+27*s(284)+7*s(285)+7*s(286)+6*s(287)+2*s(288)+2*s(289)+2*s(290)+18
Such that:s(275) =< 1
s(276) =< 2
s(277) =< V1
s(278) =< V1+1
s(279) =< s(275)
s(280) =< s(276)
s(281) =< s(277)
s(282) =< s(277)-1
s(283) =< s(277)
s(284) =< s(281)*s(277)
s(285) =< s(281)*s(282)
s(286) =< s(281)*s(283)
s(287) =< s(278)
s(288) =< s(278)
s(287) =< s(277)
s(289) =< s(287)*s(282)
s(290) =< s(287)*s(283)

with precondition: [V>=0,V1>=0,V2>=0,V3>=0]

* Chain [33]: 4*s(292)+1*s(294)+3
Such that:s(294) =< V
aux(63) =< V1
s(292) =< aux(63)

with precondition: [V>=0,V1>=1]

* Chain [32]: 2*s(304)+2*s(305)+40*s(306)+4*s(307)+6*s(308)+2*s(309)+30*s(310)+11*s(311)+3*s(312)+3*s(315)+1*s(316)+1*s(317)+2*s(318)+2*s(319)+3*s(320)+1*s(321)+6*s(323)+1*s(324)+1*s(325)+1*s(326)+2*s(327)+2*s(328)+6
Such that:s(297) =< 1
s(298) =< 2
s(299) =< V1
s(296) =< V1+1
s(300) =< V1-V2
s(301) =< V1-V2+1
s(302) =< V2
s(303) =< V2+1
s(304) =< s(297)
s(305) =< s(298)
s(306) =< s(300)
s(307) =< s(301)
s(308) =< s(302)
s(309) =< s(303)
s(310) =< s(299)
s(311) =< s(306)*s(299)
s(312) =< s(301)
s(312) =< s(300)
s(313) =< s(300)-1
s(314) =< s(299)
s(315) =< s(306)*s(300)
s(316) =< s(312)*s(313)
s(317) =< s(312)*s(314)
s(318) =< s(306)*s(313)
s(319) =< s(306)*s(314)
s(320) =< s(296)
s(321) =< s(296)
s(320) =< s(299)
s(322) =< s(299)-1
s(323) =< s(310)*s(299)
s(324) =< s(320)*s(322)
s(325) =< s(320)*s(314)
s(326) =< s(307)*s(299)
s(327) =< s(310)*s(322)
s(328) =< s(310)*s(314)

with precondition: [V=1,V3=0,V2>=1,V1>=V2+1]

* Chain [31]: 1*s(329)+1*s(330)+2*s(332)+3
Such that:s(331) =< V1
s(329) =< V3
s(330) =< V3+1
s(332) =< s(331)

with precondition: [V=1,V1>=1,V2>=0,V3>=1,V2+V3>=V1]

* Chain [30]: 2*s(337)+6*s(338)+1*s(339)+9*s(340)+3*s(343)+3*s(344)+2*s(345)+2*s(346)+3*s(347)+1*s(348)+1*s(349)+1*s(350)+3
Such that:s(334) =< V1
s(335) =< V1-V2
s(333) =< V1-V2+1
s(336) =< V1-V2-V3
s(337) =< s(334)
s(338) =< s(335)
s(339) =< s(335)
s(340) =< s(336)
s(338) =< s(336)
s(341) =< s(335)-1
s(342) =< s(334)
s(343) =< s(340)*s(335)
s(344) =< s(340)*s(334)
s(345) =< s(338)*s(341)
s(346) =< s(338)*s(342)
s(347) =< s(333)
s(348) =< s(333)
s(347) =< s(335)
s(347) =< s(336)
s(349) =< s(347)*s(341)
s(350) =< s(347)*s(342)

with precondition: [V=1,V2>=0,V3>=1,V1>=V2+V3+1]


Closed-form bounds of start(V,V1,V2,V3):
-------------------------------------
* Chain [36] with precondition: [V=0,V1>=0]
- Upper bound: 1
- Complexity: constant
* Chain [35] with precondition: [V1=0,V>=0]
- Upper bound: nat(V3)+3+nat(V3+1)
- Complexity: n
* Chain [34] with precondition: [V>=0,V1>=0,V2>=0,V3>=0]
- Upper bound: 95*V1+32+34*V1*V1+ (V1+1)* (2*V1)+nat(V1-1)*7*V1+ (V1+1)* (nat(V1-1)*2)+ (8*V1+8)
- Complexity: n^2
* Chain [33] with precondition: [V>=0,V1>=1]
- Upper bound: V+4*V1+3
- Complexity: n
* Chain [32] with precondition: [V=1,V3=0,V2>=1,V1>=V2+1]
- Upper bound: 40*V1-40*V2+ (7*V1-7*V2+7+ (30*V1+12+8*V1*V1+ (V1+1)*V1+ (V1-V2+1)* (2*V1)+ (V1-V2)* (13*V1)+6*V2+ (2*V1-2)*V1+ (V1-1)* (V1+1)+ (V1-V2-1)* (V1-V2+1)+ (2*V1-2*V2-2)* (V1-V2)+ (4*V1+4)+ (2*V2+2)))+ (3*V1-3*V2)* (V1-V2)
- Complexity: n^2
* Chain [31] with precondition: [V=1,V1>=1,V2>=0,V3>=1,V2+V3>=V1]
- Upper bound: 2*V1+2*V3+4
- Complexity: n
* Chain [30] with precondition: [V=1,V2>=0,V3>=1,V1>=V2+V3+1]
- Upper bound: 9*V1-9*V2-9*V3+ (7*V1-7*V2+ (4*V1-4*V2+4+ (2*V1+3+ (V1-V2+1)*V1+ (V1-V2)* (2*V1)+ (V1-V2-V3)* (3*V1)+ (V1-V2-1)* (V1-V2+1)+ (2*V1-2*V2-2)* (V1-V2)))+ (V1-V2-V3)* (3*V1-3*V2))
- Complexity: n^2

### Maximum cost of start(V,V1,V2,V3): max([nat(V3)+2+nat(V3+1),2*V1+2+max([max([nat(V3+1)+nat(V3),2*V1*nat(V1-V2)+nat(V1-V2+1)*V1+3*V1*nat(V1-V2-V3)+nat(V1-V2+1)*nat(nat(V1-V2)+ -1)+nat(nat(V1-V2)+ -1)*2*nat(V1-V2)+nat(V1-V2+1)*4+nat(V1-V2)*7+nat(V1-V2)*3*nat(V1-V2-V3)+nat(V1-V2-V3)*9]),2*V1+max([V,26*V1+9+8*V1*V1+ (V1+1)*V1+nat(V1-1)*2*V1+ (V1+1)*nat(V1-1)+ (4*V1+4)+max([65*V1+20+26*V1*V1+ (V1+1)*V1+nat(V1-1)*5*V1+ (V1+1)*nat(V1-1)+ (4*V1+4),13*V1*nat(V1-V2)+2*V1*nat(V1-V2+1)+nat(V2)*6+nat(V1-V2+1)*nat(nat(V1-V2)+ -1)+nat(nat(V1-V2)+ -1)*2*nat(V1-V2)+nat(V2+1)*2+nat(V1-V2+1)*7+nat(V1-V2)*40+nat(V1-V2)*3*nat(V1-V2)])])])])+1
Asymptotic class: n^2
* Total analysis performed in 1289 ms.

(10) BOUNDS(1, n^2)