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:

half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(0) → 0
inc(s(x)) → s(inc(x))
log(x) → log2(x, 0)
log2(x, y) → if(le(x, s(0)), x, inc(y))
if(true, x, s(y)) → y
if(false, x, y) → log2(half(x), y)

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:

half(0) → 0 [1]
half(s(0)) → 0 [1]
half(s(s(x))) → s(half(x)) [1]
le(0, y) → true [1]
le(s(x), 0) → false [1]
le(s(x), s(y)) → le(x, y) [1]
inc(0) → 0 [1]
inc(s(x)) → s(inc(x)) [1]
log(x) → log2(x, 0) [1]
log2(x, y) → if(le(x, s(0)), x, inc(y)) [1]
if(true, x, s(y)) → y [1]
if(false, x, y) → log2(half(x), y) [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:

half(0) → 0 [1]
half(s(0)) → 0 [1]
half(s(s(x))) → s(half(x)) [1]
le(0, y) → true [1]
le(s(x), 0) → false [1]
le(s(x), s(y)) → le(x, y) [1]
inc(0) → 0 [1]
inc(s(x)) → s(inc(x)) [1]
log(x) → log2(x, 0) [1]
log2(x, y) → if(le(x, s(0)), x, inc(y)) [1]
if(true, x, s(y)) → y [1]
if(false, x, y) → log2(half(x), y) [1]

The TRS has the following type information:

half :: 0:s → 0:s 0 :: 0:s s :: 0:s → 0:s le :: 0:s → 0:s → true:false true :: true:false false :: true:false inc :: 0:s → 0:s log :: 0:s → 0:s log2 :: 0:s → 0:s → 0:s if :: true:false → 0:s → 0:s → 0:s

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:

if(v0, v1, v2) → null_if [0]
half(v0) → null_half [0]
le(v0, v1) → null_le [0]
inc(v0) → null_inc [0]

And the following fresh constants:

null_if, null_half, null_le, null_inc

(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: half(0) → 0 [1] half(s(0)) → 0 [1] half(s(s(x))) → s(half(x)) [1] le(0, y) → true [1] le(s(x), 0) → false [1] le(s(x), s(y)) → le(x, y) [1] inc(0) → 0 [1] inc(s(x)) → s(inc(x)) [1] log(x) → log2(x, 0) [1] log2(x, y) → if(le(x, s(0)), x, inc(y)) [1] if(true, x, s(y)) → y [1] if(false, x, y) → log2(half(x), y) [1] if(v0, v1, v2) → null_if [0] half(v0) → null_half [0] le(v0, v1) → null_le [0] inc(v0) → null_inc [0] The TRS has the following type information: half :: 0:s:null_if:null_half:null_inc → 0:s:null_if:null_half:null_inc 0 :: 0:s:null_if:null_half:null_inc s :: 0:s:null_if:null_half:null_inc → 0:s:null_if:null_half:null_inc le :: 0:s:null_if:null_half:null_inc → 0:s:null_if:null_half:null_inc → true:false:null_le true :: true:false:null_le false :: true:false:null_le inc :: 0:s:null_if:null_half:null_inc → 0:s:null_if:null_half:null_inc log :: 0:s:null_if:null_half:null_inc → 0:s:null_if:null_half:null_inc log2 :: 0:s:null_if:null_half:null_inc → 0:s:null_if:null_half:null_inc → 0:s:null_if:null_half:null_inc if :: true:false:null_le → 0:s:null_if:null_half:null_inc → 0:s:null_if:null_half:null_inc → 0:s:null_if:null_half:null_inc null_if :: 0:s:null_if:null_half:null_inc null_half :: 0:s:null_if:null_half:null_inc null_le :: true:false:null_le null_inc :: 0:s:null_if:null_half:null_inc 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:

0 => 0
true => 2
false => 1
null_if => 0
null_half => 0
null_le => 0
null_inc => 0

(8) Obligation:

Complexity RNTS consisting of the following rules:

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)
if(z, z', z'') -{ 1 }→ y :|: z = 2, z' = x, x >= 0, y >= 0, z'' = 1 + y
if(z, z', z'') -{ 1 }→ log2(half(x), y) :|: z' = x, z'' = y, z = 1, x >= 0, y >= 0
if(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
inc(z) -{ 1 }→ 0 :|: z = 0
inc(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
inc(z) -{ 1 }→ 1 + inc(x) :|: x >= 0, z = 1 + x
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
log(z) -{ 1 }→ log2(x, 0) :|: x >= 0, z = x
log2(z, z') -{ 1 }→ if(le(x, 1 + 0), x, inc(y)) :|: x >= 0, y >= 0, z = x, z' = y

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, V2, V11),0,[half(V, Out)],[V >= 0]). eq(start(V, V2, V11),0,[le(V, V2, Out)],[V >= 0,V2 >= 0]). eq(start(V, V2, V11),0,[inc(V, Out)],[V >= 0]). eq(start(V, V2, V11),0,[log(V, Out)],[V >= 0]). eq(start(V, V2, V11),0,[log2(V, V2, Out)],[V >= 0,V2 >= 0]). eq(start(V, V2, V11),0,[if(V, V2, V11, Out)],[V >= 0,V2 >= 0,V11 >= 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(V1, Ret1)],[Out = 1 + Ret1,V1 >= 0,V = 2 + V1]). eq(le(V, V2, Out),1,[],[Out = 2,V3 >= 0,V = 0,V2 = V3]). eq(le(V, V2, Out),1,[],[Out = 1,V4 >= 0,V = 1 + V4,V2 = 0]). eq(le(V, V2, Out),1,[le(V5, V6, Ret)],[Out = Ret,V2 = 1 + V6,V5 >= 0,V6 >= 0,V = 1 + V5]). eq(inc(V, Out),1,[],[Out = 0,V = 0]). eq(inc(V, Out),1,[inc(V7, Ret11)],[Out = 1 + Ret11,V7 >= 0,V = 1 + V7]). eq(log(V, Out),1,[log2(V8, 0, Ret2)],[Out = Ret2,V8 >= 0,V = V8]). eq(log2(V, V2, Out),1,[le(V9, 1 + 0, Ret0),inc(V10, Ret21),if(Ret0, V9, Ret21, Ret3)],[Out = Ret3,V9 >= 0,V10 >= 0,V = V9,V2 = V10]). eq(if(V, V2, V11, Out),1,[],[Out = V12,V = 2,V2 = V13,V13 >= 0,V12 >= 0,V11 = 1 + V12]). eq(if(V, V2, V11, Out),1,[half(V14, Ret01),log2(Ret01, V15, Ret4)],[Out = Ret4,V2 = V14,V11 = V15,V = 1,V14 >= 0,V15 >= 0]). eq(if(V, V2, V11, Out),0,[],[Out = 0,V16 >= 0,V11 = V17,V18 >= 0,V = V16,V2 = V18,V17 >= 0]). eq(half(V, Out),0,[],[Out = 0,V19 >= 0,V = V19]). eq(le(V, V2, Out),0,[],[Out = 0,V20 >= 0,V21 >= 0,V = V20,V2 = V21]). eq(inc(V, Out),0,[],[Out = 0,V22 >= 0,V = V22]). input_output_vars(half(V,Out),[V],[Out]). input_output_vars(le(V,V2,Out),[V,V2],[Out]). input_output_vars(inc(V,Out),[V],[Out]). input_output_vars(log(V,Out),[V],[Out]). input_output_vars(log2(V,V2,Out),[V,V2],[Out]). input_output_vars(if(V,V2,V11,Out),[V,V2,V11],[Out]).

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

#### Computed strongly connected components
0. recursive : [half/2]
1. recursive : [inc/2]
2. recursive : [le/3]
3. recursive : [if/4,log2/3]
4. non_recursive : [log/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 inc/2
2. SCC is partially evaluated into le/3
3. SCC is partially evaluated into log2/3
4. SCC is completely evaluated into other SCCs
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 [24]
* CE 10 is refined into CE [25]
* CE 13 is refined into CE [26]
* CE 12 is refined into CE [27]


### Cost equations --> "Loop" of half/2
* CEs [27] --> Loop 14
* CEs [24] --> Loop 15
* CEs [25,26] --> Loop 16

### Ranking functions of CR half(V,Out)
* RF of phase [14]: [V-1]

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


### Specialization of cost equations inc/2
* CE 21 is refined into CE [28]
* CE 23 is refined into CE [29]
* CE 22 is refined into CE [30]


### Cost equations --> "Loop" of inc/2
* CEs [30] --> Loop 17
* CEs [28,29] --> Loop 18

### Ranking functions of CR inc(V,Out)
* RF of phase [17]: [V]

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


### Specialization of cost equations le/3
* CE 20 is refined into CE [31]
* CE 18 is refined into CE [32]
* CE 17 is refined into CE [33]
* CE 19 is refined into CE [34]


### Cost equations --> "Loop" of le/3
* CEs [34] --> Loop 19
* CEs [31] --> Loop 20
* CEs [32] --> Loop 21
* CEs [33] --> Loop 22

### Ranking functions of CR le(V,V2,Out)
* RF of phase [19]: [V,V2]

#### Partial ranking functions of CR le(V,V2,Out)
* Partial RF of phase [19]:
- RF of loop [19:1]:
V
V2


### Specialization of cost equations log2/3
* CE 14 is refined into CE [35,36,37,38,39,40,41,42]
* CE 16 is refined into CE [43,44]
* CE 15 is refined into CE [45,46,47,48]


### Cost equations --> "Loop" of log2/3
* CEs [48] --> Loop 23
* CEs [46] --> Loop 24
* CEs [47] --> Loop 25
* CEs [45] --> Loop 26
* CEs [44] --> Loop 27
* CEs [41,42] --> Loop 28
* CEs [43] --> Loop 29
* CEs [35,36,37,38,39,40] --> Loop 30

### Ranking functions of CR log2(V,V2,Out)
* RF of phase [23]: [V-1]
* RF of phase [24]: [V-1]

#### Partial ranking functions of CR log2(V,V2,Out)
* Partial RF of phase [23]:
- RF of loop [23:1]:
V-1
* Partial RF of phase [24]:
- RF of loop [24:1]:
V-1


### Specialization of cost equations start/3
* CE 4 is refined into CE [49]
* CE 2 is refined into CE [50]
* CE 3 is refined into CE [51,52,53,54,55]
* CE 5 is refined into CE [56,57]
* CE 6 is refined into CE [58,59,60,61,62]
* CE 7 is refined into CE [63,64]
* CE 8 is refined into CE [65]
* CE 9 is refined into CE [66,67,68,69]


### Cost equations --> "Loop" of start/3
* CEs [59] --> Loop 31
* CEs [49] --> Loop 32
* CEs [68] --> Loop 33
* CEs [51,52,53,54,55] --> Loop 34
* CEs [50,56,57,58,60,61,62,63,64,65,66,67,69] --> Loop 35

### Ranking functions of CR start(V,V2,V11)

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


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

#### Cost of chains of half(V,Out):
* Chain [[14],16]: 1*it(14)+1
Such that:it(14) =< 2*Out

with precondition: [Out>=1,V>=2*Out]

* Chain [[14],15]: 1*it(14)+1
Such that:it(14) =< 2*Out

with precondition: [V=2*Out+1,V>=3]

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

* Chain [15]: 1
with precondition: [V=1,Out=0]


#### Cost of chains of inc(V,Out):
* Chain [[17],18]: 1*it(17)+1
Such that:it(17) =< Out

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

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


#### Cost of chains of le(V,V2,Out):
* Chain [[19],22]: 1*it(19)+1
Such that:it(19) =< V

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

* Chain [[19],21]: 1*it(19)+1
Such that:it(19) =< V2

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

* Chain [[19],20]: 1*it(19)+0
Such that:it(19) =< V2

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

* Chain [22]: 1
with precondition: [V=0,Out=2,V2>=0]

* Chain [21]: 1
with precondition: [V2=0,Out=1,V>=1]

* Chain [20]: 0
with precondition: [Out=0,V>=0,V2>=0]


#### Cost of chains of log2(V,V2,Out):
* Chain [[24],30]: 6*it(24)+4*s(5)+2*s(18)+3
Such that:aux(2) =< 1
s(19) =< 2*V
aux(7) =< V
s(5) =< aux(2)
it(24) =< aux(7)
s(18) =< s(19)

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

* Chain [[24],28]: 6*it(24)+2*s(18)+2*s(20)+3
Such that:aux(8) =< 1
s(19) =< 2*V
aux(9) =< V
s(20) =< aux(8)
it(24) =< aux(9)
s(18) =< s(19)

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

* Chain [[24],26,30]: 6*it(24)+5*s(5)+2*s(18)+8
Such that:aux(10) =< 1
s(19) =< 2*V
aux(11) =< V
s(5) =< aux(10)
it(24) =< aux(11)
s(18) =< s(19)

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

* Chain [[23],[24],30]: 6*it(23)+10*it(24)+4*s(5)+1*s(33)+3
Such that:aux(2) =< 1
aux(13) =< V2
aux(16) =< V
aux(17) =< 2*V
s(5) =< aux(2)
it(24) =< aux(17)
it(23) =< aux(16)
s(33) =< it(23)*aux(13)

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

* Chain [[23],[24],28]: 6*it(23)+10*it(24)+2*s(20)+1*s(33)+3
Such that:aux(8) =< 1
aux(13) =< V2
aux(18) =< V
aux(19) =< 2*V
s(20) =< aux(8)
it(24) =< aux(19)
it(23) =< aux(18)
s(33) =< it(23)*aux(13)

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

* Chain [[23],[24],26,30]: 6*it(23)+10*it(24)+5*s(5)+1*s(33)+8
Such that:aux(10) =< 1
aux(13) =< V2
aux(20) =< V
aux(21) =< 2*V
s(5) =< aux(10)
it(24) =< aux(21)
it(23) =< aux(20)
s(33) =< it(23)*aux(13)

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

* Chain [[23],30]: 6*it(23)+3*s(4)+4*s(5)+1*s(33)+2*s(34)+3
Such that:aux(2) =< 1
s(35) =< 2*V
aux(22) =< V
aux(23) =< V2
s(5) =< aux(2)
s(4) =< aux(23)
it(23) =< aux(22)
s(33) =< it(23)*aux(23)
s(34) =< s(35)

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

* Chain [[23],28]: 6*it(23)+2*s(20)+1*s(22)+1*s(33)+2*s(34)+3
Such that:aux(8) =< 1
s(35) =< 2*V
aux(24) =< V
aux(25) =< V2
s(22) =< aux(25)
s(20) =< aux(8)
it(23) =< aux(24)
s(33) =< it(23)*aux(25)
s(34) =< s(35)

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

* Chain [[23],27]: 6*it(23)+1*s(33)+2*s(34)+1*s(36)+1*s(37)+4
Such that:s(36) =< 1
s(35) =< 2*V
aux(26) =< V
aux(27) =< V2
s(37) =< aux(27)
it(23) =< aux(26)
s(33) =< it(23)*aux(27)
s(34) =< s(35)

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

* Chain [[23],26,30]: 6*it(23)+5*s(5)+1*s(33)+2*s(34)+8
Such that:aux(10) =< 1
s(35) =< 2*V
aux(13) =< V2
aux(28) =< V
s(5) =< aux(10)
it(23) =< aux(28)
s(33) =< it(23)*aux(13)
s(34) =< s(35)

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

* Chain [[23],25,30]: 6*it(23)+4*s(4)+5*s(5)+1*s(33)+2*s(34)+8
Such that:aux(29) =< 1
s(35) =< 2*V
aux(31) =< V
aux(32) =< V2
s(5) =< aux(29)
s(4) =< aux(32)
it(23) =< aux(31)
s(33) =< it(23)*aux(32)
s(34) =< s(35)

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

* Chain [[23],25,29]: 6*it(23)+1*s(33)+2*s(34)+1*s(38)+2*s(39)+9
Such that:s(38) =< 1
s(35) =< 2*V
aux(34) =< V
aux(35) =< V2
s(39) =< aux(35)
it(23) =< aux(34)
s(33) =< it(23)*aux(35)
s(34) =< s(35)

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

* Chain [30]: 3*s(4)+4*s(5)+3
Such that:aux(2) =< 1
aux(3) =< V2
s(5) =< aux(2)
s(4) =< aux(3)

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

* Chain [29]: 1*s(40)+4
Such that:s(40) =< V2

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

* Chain [28]: 2*s(20)+1*s(22)+3
Such that:s(22) =< V2
aux(8) =< 1
s(20) =< aux(8)

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

* Chain [27]: 1*s(36)+1*s(37)+4
Such that:s(36) =< 1
s(37) =< V2

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

* Chain [26,30]: 5*s(5)+8
Such that:aux(10) =< 1
s(5) =< aux(10)

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

* Chain [25,30]: 4*s(4)+5*s(5)+8
Such that:aux(29) =< 1
aux(30) =< V2
s(5) =< aux(29)
s(4) =< aux(30)

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

* Chain [25,29]: 1*s(38)+2*s(39)+9
Such that:s(38) =< 1
aux(33) =< V2
s(39) =< aux(33)

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


#### Cost of chains of start(V,V2,V11):
* Chain [35]: 136*s(151)+24*s(152)+111*s(161)+92*s(164)+9*s(173)+9
Such that:aux(44) =< 1
aux(45) =< V
aux(46) =< 2*V
aux(47) =< V2
s(151) =< aux(45)
s(152) =< aux(47)
s(161) =< aux(44)
s(164) =< aux(46)
s(173) =< s(151)*aux(47)

with precondition: [V>=0]

* Chain [34]: 39*s(184)+112*s(190)+52*s(195)+72*s(202)+9*s(203)+2*s(206)+11
Such that:s(205) =< 2
aux(51) =< 1
aux(52) =< V2
aux(53) =< V2/2
aux(54) =< V11
s(190) =< aux(51)
s(184) =< aux(54)
s(202) =< aux(53)
s(203) =< s(202)*aux(54)
s(195) =< aux(52)
s(206) =< s(205)

with precondition: [V=1,V2>=0,V11>=0]

* Chain [33]: 1*s(220)+1*s(221)+4
Such that:s(220) =< 1
s(221) =< V2

with precondition: [V=1,V2>=1]

* Chain [32]: 1
with precondition: [V=2,V2>=0,V11>=1]

* Chain [31]: 1
with precondition: [V2=0,V>=1]


Closed-form bounds of start(V,V2,V11):
-------------------------------------
* Chain [35] with precondition: [V>=0]
- Upper bound: 136*V+120+nat(V2)*24+nat(V2)*9*V+184*V
- Complexity: n^2
* Chain [34] with precondition: [V=1,V2>=0,V11>=0]
- Upper bound: 52*V2+39*V11+127+V2/2* (9*V11)+36*V2
- Complexity: n^2
* Chain [33] with precondition: [V=1,V2>=1]
- Upper bound: V2+5
- Complexity: n
* Chain [32] with precondition: [V=2,V2>=0,V11>=1]
- Upper bound: 1
- Complexity: constant
* Chain [31] with precondition: [V2=0,V>=1]
- Upper bound: 1
- Complexity: constant

### Maximum cost of start(V,V2,V11): nat(V2)*23+115+max([nat(V2)*9*V+136*V+184*V,nat(V2)*28+7+nat(V11)*39+nat(V11)*9*nat(V2/2)+nat(V2/2)*72])+ (nat(V2)+4)+1
Asymptotic class: n^2
* Total analysis performed in 517 ms.

(10) BOUNDS(1, n^2)