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

(0) Obligation:

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


The TRS R consists of the following rules:

isort(Cons(x, xs), r) → isort(xs, insert(x, r))
isort(Nil, r) → Nil
insert(S(x), r) → insert[Ite](<(S(x), x), S(x), r)
inssort(xs) → isort(xs, Nil)

The (relative) TRS S consists of the following rules:

<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
insert[Ite](False, x', Cons(x, xs)) → Cons(x, insert(x', xs))
insert[Ite](True, x, r) → Cons(x, r)

Rewrite Strategy: INNERMOST

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

Transformed relative 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:

isort(Cons(x, xs), r) → isort(xs, insert(x, r)) [1]
isort(Nil, r) → Nil [1]
insert(S(x), r) → insert[Ite](<(S(x), x), S(x), r) [1]
inssort(xs) → isort(xs, Nil) [1]
<(S(x), S(y)) → <(x, y) [0]
<(0, S(y)) → True [0]
<(x, 0) → False [0]
insert[Ite](False, x', Cons(x, xs)) → Cons(x, insert(x', xs)) [0]
insert[Ite](True, x, r) → Cons(x, r) [0]

Rewrite Strategy: INNERMOST

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

Renamed defined symbols to avoid conflicts with arithmetic symbols:

< => lt

(4) 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:

isort(Cons(x, xs), r) → isort(xs, insert(x, r)) [1]
isort(Nil, r) → Nil [1]
insert(S(x), r) → insert[Ite](lt(S(x), x), S(x), r) [1]
inssort(xs) → isort(xs, Nil) [1]
lt(S(x), S(y)) → lt(x, y) [0]
lt(0, S(y)) → True [0]
lt(x, 0) → False [0]
insert[Ite](False, x', Cons(x, xs)) → Cons(x, insert(x', xs)) [0]
insert[Ite](True, x, r) → Cons(x, r) [0]

Rewrite Strategy: INNERMOST

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

Infered types.

(6) Obligation:

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

isort(Cons(x, xs), r) → isort(xs, insert(x, r)) [1]
isort(Nil, r) → Nil [1]
insert(S(x), r) → insert[Ite](lt(S(x), x), S(x), r) [1]
inssort(xs) → isort(xs, Nil) [1]
lt(S(x), S(y)) → lt(x, y) [0]
lt(0, S(y)) → True [0]
lt(x, 0) → False [0]
insert[Ite](False, x', Cons(x, xs)) → Cons(x, insert(x', xs)) [0]
insert[Ite](True, x, r) → Cons(x, r) [0]

The TRS has the following type information:

isort :: Cons:Nil → Cons:Nil → Cons:Nil Cons :: S:0 → Cons:Nil → Cons:Nil insert :: S:0 → Cons:Nil → Cons:Nil Nil :: Cons:Nil S :: S:0 → S:0 insert[Ite] :: True:False → S:0 → Cons:Nil → Cons:Nil lt :: S:0 → S:0 → True:False inssort :: Cons:Nil → Cons:Nil 0 :: S:0 True :: True:False False :: True:False

Rewrite Strategy: INNERMOST

(7) 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:

lt(v0, v1) → null_lt [0]
insert[Ite](v0, v1, v2) → null_insert[Ite] [0]
isort(v0, v1) → null_isort [0]
insert(v0, v1) → null_insert [0]

And the following fresh constants:

null_lt, null_insert[Ite], null_isort, null_insert

(8) 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: isort(Cons(x, xs), r) → isort(xs, insert(x, r)) [1] isort(Nil, r) → Nil [1] insert(S(x), r) → insert[Ite](lt(S(x), x), S(x), r) [1] inssort(xs) → isort(xs, Nil) [1] lt(S(x), S(y)) → lt(x, y) [0] lt(0, S(y)) → True [0] lt(x, 0) → False [0] insert[Ite](False, x', Cons(x, xs)) → Cons(x, insert(x', xs)) [0] insert[Ite](True, x, r) → Cons(x, r) [0] lt(v0, v1) → null_lt [0] insert[Ite](v0, v1, v2) → null_insert[Ite] [0] isort(v0, v1) → null_isort [0] insert(v0, v1) → null_insert [0] The TRS has the following type information: isort :: Cons:Nil:null_insert[Ite]:null_isort:null_insert → Cons:Nil:null_insert[Ite]:null_isort:null_insert → Cons:Nil:null_insert[Ite]:null_isort:null_insert Cons :: S:0 → Cons:Nil:null_insert[Ite]:null_isort:null_insert → Cons:Nil:null_insert[Ite]:null_isort:null_insert insert :: S:0 → Cons:Nil:null_insert[Ite]:null_isort:null_insert → Cons:Nil:null_insert[Ite]:null_isort:null_insert Nil :: Cons:Nil:null_insert[Ite]:null_isort:null_insert S :: S:0 → S:0 insert[Ite] :: True:False:null_lt → S:0 → Cons:Nil:null_insert[Ite]:null_isort:null_insert → Cons:Nil:null_insert[Ite]:null_isort:null_insert lt :: S:0 → S:0 → True:False:null_lt inssort :: Cons:Nil:null_insert[Ite]:null_isort:null_insert → Cons:Nil:null_insert[Ite]:null_isort:null_insert 0 :: S:0 True :: True:False:null_lt False :: True:False:null_lt null_lt :: True:False:null_lt null_insert[Ite] :: Cons:Nil:null_insert[Ite]:null_isort:null_insert null_isort :: Cons:Nil:null_insert[Ite]:null_isort:null_insert null_insert :: Cons:Nil:null_insert[Ite]:null_isort:null_insert Rewrite Strategy: INNERMOST

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

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

Nil => 0
0 => 0
True => 2
False => 1
null_lt => 0
null_insert[Ite] => 0
null_isort => 0
null_insert => 0

(10) Obligation:

Complexity RNTS consisting of the following rules:

insert(z, z') -{ 1 }→ insert[Ite](lt(1 + x, x), 1 + x, r) :|: r >= 0, x >= 0, z = 1 + x, z' = r
insert(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
insert[Ite](z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
insert[Ite](z, z', z'') -{ 0 }→ 1 + x + r :|: z = 2, z'' = r, r >= 0, z' = x, x >= 0
insert[Ite](z, z', z'') -{ 0 }→ 1 + x + insert(x', xs) :|: z' = x', xs >= 0, z = 1, x' >= 0, x >= 0, z'' = 1 + x + xs
inssort(z) -{ 1 }→ isort(xs, 0) :|: xs >= 0, z = xs
isort(z, z') -{ 1 }→ isort(xs, insert(x, r)) :|: z = 1 + x + xs, xs >= 0, r >= 0, x >= 0, z' = r
isort(z, z') -{ 1 }→ 0 :|: r >= 0, z = 0, z' = r
isort(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
lt(z, z') -{ 0 }→ lt(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
lt(z, z') -{ 0 }→ 2 :|: z' = 1 + y, y >= 0, z = 0
lt(z, z') -{ 0 }→ 1 :|: x >= 0, z = x, z' = 0
lt(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1

Only complete derivations are relevant for the runtime complexity.

(11) CompleteCoflocoProof (EQUIVALENT transformation)

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

eq(start(V, V1, V13),0,[isort(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V13),0,[insert(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V13),0,[inssort(V, Out)],[V >= 0]). eq(start(V, V1, V13),0,[lt(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V13),0,[fun(V, V1, V13, Out)],[V >= 0,V1 >= 0,V13 >= 0]). eq(isort(V, V1, Out),1,[insert(V3, V4, Ret1),isort(V2, Ret1, Ret)],[Out = Ret,V = 1 + V2 + V3,V2 >= 0,V4 >= 0,V3 >= 0,V1 = V4]). eq(isort(V, V1, Out),1,[],[Out = 0,V5 >= 0,V = 0,V1 = V5]). eq(insert(V, V1, Out),1,[lt(1 + V6, V6, Ret0),fun(Ret0, 1 + V6, V7, Ret2)],[Out = Ret2,V7 >= 0,V6 >= 0,V = 1 + V6,V1 = V7]). eq(inssort(V, Out),1,[isort(V8, 0, Ret3)],[Out = Ret3,V8 >= 0,V = V8]). eq(lt(V, V1, Out),0,[lt(V9, V10, Ret4)],[Out = Ret4,V1 = 1 + V10,V9 >= 0,V10 >= 0,V = 1 + V9]). eq(lt(V, V1, Out),0,[],[Out = 2,V1 = 1 + V11,V11 >= 0,V = 0]). eq(lt(V, V1, Out),0,[],[Out = 1,V12 >= 0,V = V12,V1 = 0]). eq(fun(V, V1, V13, Out),0,[insert(V15, V16, Ret11)],[Out = 1 + Ret11 + V14,V1 = V15,V16 >= 0,V = 1,V15 >= 0,V14 >= 0,V13 = 1 + V14 + V16]). eq(fun(V, V1, V13, Out),0,[],[Out = 1 + V17 + V18,V = 2,V13 = V18,V18 >= 0,V1 = V17,V17 >= 0]). eq(lt(V, V1, Out),0,[],[Out = 0,V19 >= 0,V20 >= 0,V = V19,V1 = V20]). eq(fun(V, V1, V13, Out),0,[],[Out = 0,V21 >= 0,V13 = V22,V23 >= 0,V = V21,V1 = V23,V22 >= 0]). eq(isort(V, V1, Out),0,[],[Out = 0,V24 >= 0,V25 >= 0,V = V24,V1 = V25]). eq(insert(V, V1, Out),0,[],[Out = 0,V26 >= 0,V27 >= 0,V = V26,V1 = V27]). input_output_vars(isort(V,V1,Out),[V,V1],[Out]). input_output_vars(insert(V,V1,Out),[V,V1],[Out]). input_output_vars(inssort(V,Out),[V],[Out]). input_output_vars(lt(V,V1,Out),[V,V1],[Out]). input_output_vars(fun(V,V1,V13,Out),[V,V1,V13],[Out]).

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

#### Computed strongly connected components
0. recursive : [lt/3]
1. recursive : [fun/4,insert/3]
2. recursive : [isort/3]
3. non_recursive : [inssort/2]
4. non_recursive : [start/3]

#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into lt/3
1. SCC is partially evaluated into insert/3
2. SCC is partially evaluated into isort/3
3. SCC is completely evaluated into other SCCs
4. SCC is partially evaluated into start/3

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

### Specialization of cost equations lt/3
* CE 18 is refined into CE [19]
* CE 17 is refined into CE [20]
* CE 16 is refined into CE [21]
* CE 15 is refined into CE [22]


### Cost equations --> "Loop" of lt/3
* CEs [22] --> Loop 11
* CEs [19] --> Loop 12
* CEs [20] --> Loop 13
* CEs [21] --> Loop 14

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

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


### Specialization of cost equations insert/3
* CE 9 is discarded (unfeasible)
* CE 8 is refined into CE [23,24,25]
* CE 11 is refined into CE [26]
* CE 10 is refined into CE [27,28]


### Cost equations --> "Loop" of insert/3
* CEs [28] --> Loop 15
* CEs [27] --> Loop 16
* CEs [23,24,25,26] --> Loop 17

### Ranking functions of CR insert(V,V1,Out)
* RF of phase [15]: [V1]
* RF of phase [16]: [V1]

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


### Specialization of cost equations isort/3
* CE 13 is refined into CE [29]
* CE 14 is refined into CE [30]
* CE 12 is refined into CE [31,32,33]


### Cost equations --> "Loop" of isort/3
* CEs [33] --> Loop 18
* CEs [31] --> Loop 19
* CEs [32] --> Loop 20
* CEs [29,30] --> Loop 21

### Ranking functions of CR isort(V,V1,Out)
* RF of phase [18,19]: [V/2-1/2]
* RF of phase [20]: [V]

#### Partial ranking functions of CR isort(V,V1,Out)
* Partial RF of phase [18,19]:
- RF of loop [18:1]:
V/3-2/3
- RF of loop [19:1]:
V/2-1/2
* Partial RF of phase [20]:
- RF of loop [20:1]:
V


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


### Cost equations --> "Loop" of start/3
* CEs [44] --> Loop 22
* CEs [39] --> Loop 23
* CEs [35,36,37] --> Loop 24
* CEs [34,38,40,41,42,43,45,46,47] --> Loop 25

### Ranking functions of CR start(V,V1,V13)

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


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

#### Cost of chains of lt(V,V1,Out):
* Chain [[11],14]: 0
with precondition: [Out=2,V>=1,V1>=V+1]

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

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

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

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

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


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

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

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

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

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


#### Cost of chains of isort(V,V1,Out):
* Chain [[20],21]: 2*it(20)+1
Such that:it(20) =< V

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

* Chain [[18,19],[20],21]: 4*it(18)+2*it(20)+1*s(5)+1*s(6)+1
Such that:aux(3) =< V/2
aux(1) =< V1
aux(5) =< V
it(18) =< aux(5)
it(20) =< aux(5)
it(18) =< aux(3)
aux(2) =< aux(1)
s(5) =< it(18)*aux(1)
s(6) =< it(18)*aux(2)

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

* Chain [[18,19],21]: 2*it(18)+2*it(19)+1*s(5)+1*s(6)+1
Such that:it(18) =< V/3
aux(1) =< V1
aux(6) =< V/2
it(18) =< aux(6)
it(19) =< aux(6)
aux(2) =< aux(1)
s(5) =< it(18)*aux(1)
s(6) =< it(19)*aux(2)

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

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


#### Cost of chains of start(V,V1,V13):
* Chain [25]: 4*s(23)+8*s(27)+8*s(28)+1*s(30)+1*s(31)+4*s(32)+1*s(33)+1*s(34)+1*s(35)+2
Such that:aux(10) =< V
aux(11) =< V/2
aux(12) =< V/3
aux(13) =< V1
s(23) =< aux(12)
s(35) =< aux(13)
s(27) =< aux(10)
s(28) =< aux(10)
s(28) =< aux(11)
s(29) =< aux(13)
s(30) =< s(28)*aux(13)
s(31) =< s(28)*s(29)
s(23) =< aux(11)
s(32) =< aux(11)
s(33) =< s(23)*aux(13)
s(34) =< s(32)*s(29)

with precondition: [V>=0]

* Chain [24]: 2*s(48)+1
Such that:aux(14) =< V13
s(48) =< aux(14)

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

* Chain [23]: 1*s(50)+1
Such that:s(50) =< V1

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

* Chain [22]: 0
with precondition: [V1=0,V>=0]


Closed-form bounds of start(V,V1,V13):
-------------------------------------
* Chain [25] with precondition: [V>=0]
- Upper bound: 16*V+2+nat(V1)+nat(V1)*2*V+V/2*nat(V1)+V/3*nat(V1)+2*V+4/3*V
- Complexity: n^2
* Chain [24] with precondition: [V=1,V1>=0,V13>=1]
- Upper bound: 2*V13+1
- Complexity: n
* Chain [23] with precondition: [V=1,V1>=1]
- Upper bound: V1+1
- Complexity: n
* Chain [22] with precondition: [V1=0,V>=0]
- Upper bound: 0
- Complexity: constant

### Maximum cost of start(V,V1,V13): max([nat(V13)*2+1,16*V+1+nat(V1)*2*V+V/2*nat(V1)+V/3*nat(V1)+2*V+4/3*V+ (nat(V1)+1)])
Asymptotic class: n^2
* Total analysis performed in 308 ms.

(12) BOUNDS(1, n^2)