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), 18 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 445 ms)
↳10 BOUNDS(1, n^1)
a__eq(0, 0) → true
a__eq(s(X), s(Y)) → a__eq(X, Y)
a__eq(X, Y) → false
a__inf(X) → cons(X, inf(s(X)))
a__take(0, X) → nil
a__take(s(X), cons(Y, L)) → cons(Y, take(X, L))
a__length(nil) → 0
a__length(cons(X, L)) → s(length(L))
mark(eq(X1, X2)) → a__eq(X1, X2)
mark(inf(X)) → a__inf(mark(X))
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(length(X)) → a__length(mark(X))
mark(0) → 0
mark(true) → true
mark(s(X)) → s(X)
mark(false) → false
mark(cons(X1, X2)) → cons(X1, X2)
mark(nil) → nil
a__eq(X1, X2) → eq(X1, X2)
a__inf(X) → inf(X)
a__take(X1, X2) → take(X1, X2)
a__length(X) → length(X)
a__eq(0, 0) → true [1]
a__eq(s(X), s(Y)) → a__eq(X, Y) [1]
a__eq(X, Y) → false [1]
a__inf(X) → cons(X, inf(s(X))) [1]
a__take(0, X) → nil [1]
a__take(s(X), cons(Y, L)) → cons(Y, take(X, L)) [1]
a__length(nil) → 0 [1]
a__length(cons(X, L)) → s(length(L)) [1]
mark(eq(X1, X2)) → a__eq(X1, X2) [1]
mark(inf(X)) → a__inf(mark(X)) [1]
mark(take(X1, X2)) → a__take(mark(X1), mark(X2)) [1]
mark(length(X)) → a__length(mark(X)) [1]
mark(0) → 0 [1]
mark(true) → true [1]
mark(s(X)) → s(X) [1]
mark(false) → false [1]
mark(cons(X1, X2)) → cons(X1, X2) [1]
mark(nil) → nil [1]
a__eq(X1, X2) → eq(X1, X2) [1]
a__inf(X) → inf(X) [1]
a__take(X1, X2) → take(X1, X2) [1]
a__length(X) → length(X) [1]
a__eq(0, 0) → true [1]
a__eq(s(X), s(Y)) → a__eq(X, Y) [1]
a__eq(X, Y) → false [1]
a__inf(X) → cons(X, inf(s(X))) [1]
a__take(0, X) → nil [1]
a__take(s(X), cons(Y, L)) → cons(Y, take(X, L)) [1]
a__length(nil) → 0 [1]
a__length(cons(X, L)) → s(length(L)) [1]
mark(eq(X1, X2)) → a__eq(X1, X2) [1]
mark(inf(X)) → a__inf(mark(X)) [1]
mark(take(X1, X2)) → a__take(mark(X1), mark(X2)) [1]
mark(length(X)) → a__length(mark(X)) [1]
mark(0) → 0 [1]
mark(true) → true [1]
mark(s(X)) → s(X) [1]
mark(false) → false [1]
mark(cons(X1, X2)) → cons(X1, X2) [1]
mark(nil) → nil [1]
a__eq(X1, X2) → eq(X1, X2) [1]
a__inf(X) → inf(X) [1]
a__take(X1, X2) → take(X1, X2) [1]
a__length(X) → length(X) [1]
| a__eq :: 0:true:s:false:inf:cons:nil:take:length:eq → 0:true:s:false:inf:cons:nil:take:length:eq → 0:true:s:false:inf:cons:nil:take:length:eq 0 :: 0:true:s:false:inf:cons:nil:take:length:eq true :: 0:true:s:false:inf:cons:nil:take:length:eq s :: 0:true:s:false:inf:cons:nil:take:length:eq → 0:true:s:false:inf:cons:nil:take:length:eq false :: 0:true:s:false:inf:cons:nil:take:length:eq a__inf :: 0:true:s:false:inf:cons:nil:take:length:eq → 0:true:s:false:inf:cons:nil:take:length:eq cons :: 0:true:s:false:inf:cons:nil:take:length:eq → 0:true:s:false:inf:cons:nil:take:length:eq → 0:true:s:false:inf:cons:nil:take:length:eq inf :: 0:true:s:false:inf:cons:nil:take:length:eq → 0:true:s:false:inf:cons:nil:take:length:eq a__take :: 0:true:s:false:inf:cons:nil:take:length:eq → 0:true:s:false:inf:cons:nil:take:length:eq → 0:true:s:false:inf:cons:nil:take:length:eq nil :: 0:true:s:false:inf:cons:nil:take:length:eq take :: 0:true:s:false:inf:cons:nil:take:length:eq → 0:true:s:false:inf:cons:nil:take:length:eq → 0:true:s:false:inf:cons:nil:take:length:eq a__length :: 0:true:s:false:inf:cons:nil:take:length:eq → 0:true:s:false:inf:cons:nil:take:length:eq length :: 0:true:s:false:inf:cons:nil:take:length:eq → 0:true:s:false:inf:cons:nil:take:length:eq mark :: 0:true:s:false:inf:cons:nil:take:length:eq → 0:true:s:false:inf:cons:nil:take:length:eq eq :: 0:true:s:false:inf:cons:nil:take:length:eq → 0:true:s:false:inf:cons:nil:take:length:eq → 0:true:s:false:inf:cons:nil:take:length:eq |
| 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 => 3
false => 1
nil => 2
a__eq(z, z') -{ 1 }→ a__eq(X, Y) :|: z = 1 + X, Y >= 0, z' = 1 + Y, X >= 0
a__eq(z, z') -{ 1 }→ 3 :|: z = 0, z' = 0
a__eq(z, z') -{ 1 }→ 1 :|: z' = Y, Y >= 0, X >= 0, z = X
a__eq(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
a__inf(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
a__inf(z) -{ 1 }→ 1 + X + (1 + (1 + X)) :|: X >= 0, z = X
a__length(z) -{ 1 }→ 0 :|: z = 2
a__length(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
a__length(z) -{ 1 }→ 1 + (1 + L) :|: z = 1 + X + L, X >= 0, L >= 0
a__take(z, z') -{ 1 }→ 2 :|: z' = X, X >= 0, z = 0
a__take(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
a__take(z, z') -{ 1 }→ 1 + Y + (1 + X + L) :|: z = 1 + X, Y >= 0, X >= 0, L >= 0, z' = 1 + Y + L
mark(z) -{ 1 }→ a__take(mark(X1), mark(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
mark(z) -{ 1 }→ a__length(mark(X)) :|: z = 1 + X, X >= 0
mark(z) -{ 1 }→ a__inf(mark(X)) :|: z = 1 + X, X >= 0
mark(z) -{ 1 }→ a__eq(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
mark(z) -{ 1 }→ 3 :|: z = 3
mark(z) -{ 1 }→ 2 :|: z = 2
mark(z) -{ 1 }→ 1 :|: z = 1
mark(z) -{ 1 }→ 0 :|: z = 0
mark(z) -{ 1 }→ 1 + X :|: z = 1 + X, X >= 0
mark(z) -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
| eq(start(V, V1),0,[fun(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[fun1(V, Out)],[V >= 0]). eq(start(V, V1),0,[fun2(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[fun3(V, Out)],[V >= 0]). eq(start(V, V1),0,[mark(V, Out)],[V >= 0]). eq(fun(V, V1, Out),1,[],[Out = 3,V = 0,V1 = 0]). eq(fun(V, V1, Out),1,[fun(X3, Y1, Ret)],[Out = Ret,V = 1 + X3,Y1 >= 0,V1 = 1 + Y1,X3 >= 0]). eq(fun(V, V1, Out),1,[],[Out = 1,V1 = Y2,Y2 >= 0,X4 >= 0,V = X4]). eq(fun1(V, Out),1,[],[Out = 3 + 2*X5,X5 >= 0,V = X5]). eq(fun2(V, V1, Out),1,[],[Out = 2,V1 = X6,X6 >= 0,V = 0]). eq(fun2(V, V1, Out),1,[],[Out = 2 + L1 + X7 + Y3,V = 1 + X7,Y3 >= 0,X7 >= 0,L1 >= 0,V1 = 1 + L1 + Y3]). eq(fun3(V, Out),1,[],[Out = 0,V = 2]). eq(fun3(V, Out),1,[],[Out = 2 + L2,V = 1 + L2 + X8,X8 >= 0,L2 >= 0]). eq(mark(V, Out),1,[fun(X11, X21, Ret1)],[Out = Ret1,X11 >= 0,X21 >= 0,V = 1 + X11 + X21]). eq(mark(V, Out),1,[mark(X9, Ret0),fun1(Ret0, Ret2)],[Out = Ret2,V = 1 + X9,X9 >= 0]). eq(mark(V, Out),1,[mark(X12, Ret01),mark(X22, Ret11),fun2(Ret01, Ret11, Ret3)],[Out = Ret3,X12 >= 0,X22 >= 0,V = 1 + X12 + X22]). eq(mark(V, Out),1,[mark(X10, Ret02),fun3(Ret02, Ret4)],[Out = Ret4,V = 1 + X10,X10 >= 0]). eq(mark(V, Out),1,[],[Out = 0,V = 0]). eq(mark(V, Out),1,[],[Out = 3,V = 3]). eq(mark(V, Out),1,[],[Out = 1 + X13,V = 1 + X13,X13 >= 0]). eq(mark(V, Out),1,[],[Out = 1,V = 1]). eq(mark(V, Out),1,[],[Out = 1 + X14 + X23,X14 >= 0,X23 >= 0,V = 1 + X14 + X23]). eq(mark(V, Out),1,[],[Out = 2,V = 2]). eq(fun(V, V1, Out),1,[],[Out = 1 + X15 + X24,X15 >= 0,X24 >= 0,V = X15,V1 = X24]). eq(fun1(V, Out),1,[],[Out = 1 + X16,X16 >= 0,V = X16]). eq(fun2(V, V1, Out),1,[],[Out = 1 + X17 + X25,X17 >= 0,X25 >= 0,V = X17,V1 = X25]). eq(fun3(V, Out),1,[],[Out = 1 + X18,X18 >= 0,V = X18]). input_output_vars(fun(V,V1,Out),[V,V1],[Out]). input_output_vars(fun1(V,Out),[V],[Out]). input_output_vars(fun2(V,V1,Out),[V,V1],[Out]). input_output_vars(fun3(V,Out),[V],[Out]). input_output_vars(mark(V,Out),[V],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [fun/3]
1. non_recursive : [fun1/2]
2. non_recursive : [fun2/3]
3. non_recursive : [fun3/2]
4. recursive [non_tail,multiple] : [mark/2]
5. non_recursive : [start/2]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into fun/3
1. SCC is partially evaluated into fun1/2
2. SCC is partially evaluated into fun2/3
3. SCC is partially evaluated into fun3/2
4. SCC is partially evaluated into mark/2
5. SCC is partially evaluated into start/2
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations fun/3
* CE 10 is refined into CE [25]
* CE 9 is refined into CE [26]
* CE 7 is refined into CE [27]
* CE 8 is refined into CE [28]
### Cost equations --> "Loop" of fun/3
* CEs [28] --> Loop 18
* CEs [25] --> Loop 19
* CEs [26] --> Loop 20
* CEs [27] --> Loop 21
### Ranking functions of CR fun(V,V1,Out)
* RF of phase [18]: [V,V1]
#### Partial ranking functions of CR fun(V,V1,Out)
* Partial RF of phase [18]:
- RF of loop [18:1]:
V
V1
### Specialization of cost equations fun1/2
* CE 11 is refined into CE [29]
* CE 12 is refined into CE [30]
### Cost equations --> "Loop" of fun1/2
* CEs [29] --> Loop 22
* CEs [30] --> Loop 23
### Ranking functions of CR fun1(V,Out)
#### Partial ranking functions of CR fun1(V,Out)
### Specialization of cost equations fun2/3
* CE 14 is refined into CE [31]
* CE 15 is refined into CE [32]
* CE 13 is refined into CE [33]
### Cost equations --> "Loop" of fun2/3
* CEs [31] --> Loop 24
* CEs [32] --> Loop 25
* CEs [33] --> Loop 26
### Ranking functions of CR fun2(V,V1,Out)
#### Partial ranking functions of CR fun2(V,V1,Out)
### Specialization of cost equations fun3/2
* CE 17 is refined into CE [34]
* CE 18 is refined into CE [35]
* CE 16 is refined into CE [36]
### Cost equations --> "Loop" of fun3/2
* CEs [34] --> Loop 27
* CEs [35] --> Loop 28
* CEs [36] --> Loop 29
### Ranking functions of CR fun3(V,Out)
#### Partial ranking functions of CR fun3(V,Out)
### Specialization of cost equations mark/2
* CE 19 is refined into CE [37,38,39,40,41]
* CE 24 is refined into CE [42]
* CE 23 is refined into CE [43]
* CE 20 is refined into CE [44,45]
* CE 22 is refined into CE [46,47,48]
* CE 21 is refined into CE [49,50,51]
### Cost equations --> "Loop" of mark/2
* CEs [51] --> Loop 30
* CEs [50] --> Loop 31
* CEs [49] --> Loop 32
* CEs [48] --> Loop 33
* CEs [44,47] --> Loop 34
* CEs [45] --> Loop 35
* CEs [46] --> Loop 36
* CEs [41] --> Loop 37
* CEs [40,42] --> Loop 38
* CEs [39] --> Loop 39
* CEs [38] --> Loop 40
* CEs [37] --> Loop 41
* CEs [43] --> Loop 42
### Ranking functions of CR mark(V,Out)
* RF of phase [30,31,32,33,34,35,36]: [V]
#### Partial ranking functions of CR mark(V,Out)
* Partial RF of phase [30,31,32,33,34,35,36]:
- RF of loop [30:1,30:2,31:1,31:2,32:1,32:2,33:1,34:1,35:1,36:1]:
V
### Specialization of cost equations start/2
* CE 2 is refined into CE [52,53,54,55,56]
* CE 3 is refined into CE [57,58]
* CE 4 is refined into CE [59,60,61]
* CE 5 is refined into CE [62,63,64]
* CE 6 is refined into CE [65,66,67,68,69]
### Cost equations --> "Loop" of start/2
* CEs [54] --> Loop 43
* CEs [62] --> Loop 44
* CEs [52,53,55,56,57,58,59,60,61,63,64,65,66,67,68,69] --> Loop 45
### Ranking functions of CR start(V,V1)
#### Partial ranking functions of CR start(V,V1)
Computing Bounds
=====================================
#### Cost of chains of fun(V,V1,Out):
* Chain [[18],21]: 1*it(18)+1
Such that:it(18) =< V
with precondition: [Out=3,V=V1,V>=1]
* Chain [[18],20]: 1*it(18)+1
Such that:it(18) =< V1
with precondition: [Out=1,V>=1,V1>=1]
* Chain [[18],19]: 1*it(18)+1
Such that:it(18) =< V/2+V1/2-Out/2+1/2
with precondition: [Out+V1>=V+1,Out+V>=V1+1,V+V1>=Out+1]
* Chain [21]: 1
with precondition: [V=0,V1=0,Out=3]
* Chain [20]: 1
with precondition: [Out=1,V>=0,V1>=0]
* Chain [19]: 1
with precondition: [V+V1+1=Out,V>=0,V1>=0]
#### Cost of chains of fun1(V,Out):
* Chain [23]: 1
with precondition: [V+1=Out,V>=0]
* Chain [22]: 1
with precondition: [2*V+3=Out,V>=0]
#### Cost of chains of fun2(V,V1,Out):
* Chain [26]: 1
with precondition: [V=0,Out=2,V1>=0]
* Chain [25]: 1
with precondition: [V+V1+1=Out,V>=0,V1>=0]
* Chain [24]: 1
with precondition: [V+V1=Out,V>=1,V1>=1]
#### Cost of chains of fun3(V,Out):
* Chain [29]: 1
with precondition: [V=2,Out=0]
* Chain [28]: 1
with precondition: [V+1=Out,V>=0]
* Chain [27]: 1
with precondition: [Out>=2,V+1>=Out]
#### Cost of chains of mark(V,Out):
* Chain [42]: 1
with precondition: [V=0,Out=0]
* Chain [41]: 2
with precondition: [V=1,Out=3]
* Chain [40]: 1*s(2)+2
Such that:s(2) =< V
with precondition: [Out=1,V>=1]
* Chain [39]: 1*s(3)+2
Such that:s(3) =< V/2
with precondition: [Out=3,V>=3]
* Chain [38]: 2
with precondition: [V=Out,V>=1]
* Chain [37]: 1*s(4)+2
Such that:s(4) =< V/2
with precondition: [Out>=1,V>=Out+2]
* Chain [multiple([30,31,32,33,34,35,36],[[42],[41],[40],[39],[38],[37]])]: 14*it(30)+2*it([37])+4*it([38])+2*it([39])+2*it([41])+2*it([42])+2*s(6)+0
Such that:aux(1) =< V
aux(2) =< V+1
aux(3) =< V/2+1/2
aux(4) =< V/4+1/4
it(30) =< aux(1)
it([37]) =< aux(1)
it([38]) =< aux(1)
it([39]) =< aux(1)
it([41]) =< aux(1)
it([41]) =< aux(2)
it([42]) =< aux(2)
it([38]) =< aux(3)
it([39]) =< aux(3)
it([41]) =< aux(3)
s(6) =< aux(3)
it([37]) =< aux(4)
it([39]) =< aux(4)
with precondition: [V>=1,Out>=0]
#### Cost of chains of start(V,V1):
* Chain [45]: 2*s(20)+2*s(24)+15*s(27)+2*s(28)+4*s(29)+2*s(30)+2*s(31)+2*s(32)+2*s(33)+2
Such that:s(23) =< V+1
s(25) =< V/2+1/2
s(26) =< V/4+1/4
aux(5) =< V
aux(6) =< V/2
aux(7) =< V1
s(27) =< aux(5)
s(24) =< aux(6)
s(20) =< aux(7)
s(28) =< aux(5)
s(29) =< aux(5)
s(30) =< aux(5)
s(31) =< aux(5)
s(31) =< s(23)
s(32) =< s(23)
s(29) =< s(25)
s(30) =< s(25)
s(31) =< s(25)
s(33) =< s(25)
s(28) =< s(26)
s(30) =< s(26)
with precondition: [V>=0]
* Chain [44]: 1
with precondition: [V=2]
* Chain [43]: 1*s(36)+1
Such that:s(36) =< V1
with precondition: [V=V1,V>=1]
Closed-form bounds of start(V,V1):
-------------------------------------
* Chain [45] with precondition: [V>=0]
- Upper bound: 25*V+2+nat(V1)*2+ (2*V+2)+ (V+1)+V
- Complexity: n
* Chain [44] with precondition: [V=2]
- Upper bound: 1
- Complexity: constant
* Chain [43] with precondition: [V=V1,V>=1]
- Upper bound: V1+1
- Complexity: n
### Maximum cost of start(V,V1): 25*V+1+nat(V1)+ (2*V+2)+ (V+1)+V+nat(V1)+1
Asymptotic class: n
* Total analysis performed in 371 ms.