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), 19 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 493 ms)
↳10 BOUNDS(1, n^1)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y))
if_mod(true, s(x), s(y)) → mod(minus(x, y), s(y))
if_mod(false, s(x), s(y)) → s(x)
le(0, y) → true [1]
le(s(x), 0) → false [1]
le(s(x), s(y)) → le(x, y) [1]
pred(s(x)) → x [1]
minus(x, 0) → x [1]
minus(x, s(y)) → pred(minus(x, y)) [1]
mod(0, y) → 0 [1]
mod(s(x), 0) → 0 [1]
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y)) [1]
if_mod(true, s(x), s(y)) → mod(minus(x, y), s(y)) [1]
if_mod(false, s(x), s(y)) → s(x) [1]
le(0, y) → true [1]
le(s(x), 0) → false [1]
le(s(x), s(y)) → le(x, y) [1]
pred(s(x)) → x [1]
minus(x, 0) → x [1]
minus(x, s(y)) → pred(minus(x, y)) [1]
mod(0, y) → 0 [1]
mod(s(x), 0) → 0 [1]
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y)) [1]
if_mod(true, s(x), s(y)) → mod(minus(x, y), s(y)) [1]
if_mod(false, s(x), s(y)) → s(x) [1]
| le :: 0:s → 0:s → true:false 0 :: 0:s true :: true:false s :: 0:s → 0:s false :: true:false pred :: 0:s → 0:s minus :: 0:s → 0:s → 0:s mod :: 0:s → 0:s → 0:s if_mod :: true:false → 0:s → 0:s → 0:s |
pred(v0) → null_pred [0]
if_mod(v0, v1, v2) → null_if_mod [0]
le(v0, v1) → null_le [0]
minus(v0, v1) → null_minus [0]
mod(v0, v1) → null_mod [0]
null_pred, null_if_mod, null_le, null_minus, null_mod
| 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
null_pred => 0
null_if_mod => 0
null_le => 0
null_minus => 0
null_mod => 0
if_mod(z, z', z'') -{ 1 }→ mod(minus(x, y), 1 + y) :|: z = 2, z' = 1 + x, x >= 0, y >= 0, z'' = 1 + y
if_mod(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
if_mod(z, z', z'') -{ 1 }→ 1 + x :|: z' = 1 + x, z = 1, x >= 0, y >= 0, z'' = 1 + y
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
minus(z, z') -{ 1 }→ x :|: x >= 0, z = x, z' = 0
minus(z, z') -{ 1 }→ pred(minus(x, y)) :|: z' = 1 + y, x >= 0, y >= 0, z = x
minus(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
mod(z, z') -{ 1 }→ if_mod(le(y, x), 1 + x, 1 + y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
mod(z, z') -{ 1 }→ 0 :|: y >= 0, z = 0, z' = y
mod(z, z') -{ 1 }→ 0 :|: x >= 0, z = 1 + x, z' = 0
mod(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
pred(z) -{ 1 }→ x :|: x >= 0, z = 1 + x
pred(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
| eq(start(V, V1, V14),0,[le(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V14),0,[pred(V, Out)],[V >= 0]). eq(start(V, V1, V14),0,[minus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V14),0,[mod(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V14),0,[fun(V, V1, V14, Out)],[V >= 0,V1 >= 0,V14 >= 0]). eq(le(V, V1, Out),1,[],[Out = 2,V2 >= 0,V = 0,V1 = V2]). eq(le(V, V1, Out),1,[],[Out = 1,V3 >= 0,V = 1 + V3,V1 = 0]). eq(le(V, V1, Out),1,[le(V4, V5, Ret)],[Out = Ret,V1 = 1 + V5,V4 >= 0,V5 >= 0,V = 1 + V4]). eq(pred(V, Out),1,[],[Out = V6,V6 >= 0,V = 1 + V6]). eq(minus(V, V1, Out),1,[],[Out = V7,V7 >= 0,V = V7,V1 = 0]). eq(minus(V, V1, Out),1,[minus(V8, V9, Ret0),pred(Ret0, Ret1)],[Out = Ret1,V1 = 1 + V9,V8 >= 0,V9 >= 0,V = V8]). eq(mod(V, V1, Out),1,[],[Out = 0,V10 >= 0,V = 0,V1 = V10]). eq(mod(V, V1, Out),1,[],[Out = 0,V11 >= 0,V = 1 + V11,V1 = 0]). eq(mod(V, V1, Out),1,[le(V12, V13, Ret01),fun(Ret01, 1 + V13, 1 + V12, Ret2)],[Out = Ret2,V1 = 1 + V12,V13 >= 0,V12 >= 0,V = 1 + V13]). eq(fun(V, V1, V14, Out),1,[minus(V15, V16, Ret02),mod(Ret02, 1 + V16, Ret3)],[Out = Ret3,V = 2,V1 = 1 + V15,V15 >= 0,V16 >= 0,V14 = 1 + V16]). eq(fun(V, V1, V14, Out),1,[],[Out = 1 + V17,V1 = 1 + V17,V = 1,V17 >= 0,V18 >= 0,V14 = 1 + V18]). eq(pred(V, Out),0,[],[Out = 0,V19 >= 0,V = V19]). eq(fun(V, V1, V14, Out),0,[],[Out = 0,V20 >= 0,V14 = V21,V22 >= 0,V = V20,V1 = V22,V21 >= 0]). eq(le(V, V1, Out),0,[],[Out = 0,V23 >= 0,V24 >= 0,V = V23,V1 = V24]). eq(minus(V, V1, Out),0,[],[Out = 0,V25 >= 0,V26 >= 0,V = V25,V1 = V26]). eq(mod(V, V1, Out),0,[],[Out = 0,V27 >= 0,V28 >= 0,V = V27,V1 = V28]). input_output_vars(le(V,V1,Out),[V,V1],[Out]). input_output_vars(pred(V,Out),[V],[Out]). input_output_vars(minus(V,V1,Out),[V,V1],[Out]). input_output_vars(mod(V,V1,Out),[V,V1],[Out]). input_output_vars(fun(V,V1,V14,Out),[V,V1,V14],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. non_recursive : [pred/2]
1. recursive [non_tail] : [minus/3]
2. recursive : [le/3]
3. recursive : [fun/4, (mod)/3]
4. non_recursive : [start/3]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into pred/2
1. SCC is partially evaluated into minus/3
2. SCC is partially evaluated into le/3
3. SCC is partially evaluated into (mod)/3
4. SCC is partially evaluated into start/3
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations pred/2
* CE 22 is refined into CE [24]
* CE 23 is refined into CE [25]
### Cost equations --> "Loop" of pred/2
* CEs [24] --> Loop 16
* CEs [25] --> Loop 17
### Ranking functions of CR pred(V,Out)
#### Partial ranking functions of CR pred(V,Out)
### Specialization of cost equations minus/3
* CE 11 is refined into CE [26]
* CE 9 is refined into CE [27]
* CE 10 is refined into CE [28,29]
### Cost equations --> "Loop" of minus/3
* CEs [29] --> Loop 18
* CEs [28] --> Loop 19
* CEs [26] --> Loop 20
* CEs [27] --> Loop 21
### Ranking functions of CR minus(V,V1,Out)
* RF of phase [18]: [V1]
* RF of phase [19]: [V1]
#### Partial ranking functions of CR minus(V,V1,Out)
* Partial RF of phase [18]:
- RF of loop [18:1]:
V1
* Partial RF of phase [19]:
- RF of loop [19:1]:
V1
### Specialization of cost equations le/3
* CE 21 is refined into CE [30]
* CE 19 is refined into CE [31]
* CE 18 is refined into CE [32]
* CE 20 is refined into CE [33]
### Cost equations --> "Loop" of le/3
* CEs [33] --> Loop 22
* CEs [30] --> Loop 23
* CEs [31] --> Loop 24
* CEs [32] --> Loop 25
### Ranking functions of CR le(V,V1,Out)
* RF of phase [22]: [V,V1]
#### Partial ranking functions of CR le(V,V1,Out)
* Partial RF of phase [22]:
- RF of loop [22:1]:
V
V1
### Specialization of cost equations (mod)/3
* CE 13 is refined into CE [34,35]
* CE 16 is refined into CE [36]
* CE 12 is refined into CE [37,38,39,40,41]
* CE 15 is refined into CE [42]
* CE 17 is refined into CE [43]
* CE 14 is refined into CE [44,45,46,47]
### Cost equations --> "Loop" of (mod)/3
* CEs [47] --> Loop 26
* CEs [46] --> Loop 27
* CEs [44] --> Loop 28
* CEs [45] --> Loop 29
* CEs [35] --> Loop 30
* CEs [37] --> Loop 31
* CEs [36] --> Loop 32
* CEs [34] --> Loop 33
* CEs [38] --> Loop 34
* CEs [39,40,41,42,43] --> Loop 35
### Ranking functions of CR mod(V,V1,Out)
* RF of phase [26]: [V-1,V-V1+1]
* RF of phase [28]: [V]
#### Partial ranking functions of CR mod(V,V1,Out)
* Partial RF of phase [26]:
- RF of loop [26:1]:
V-1
V-V1+1
* Partial RF of phase [28]:
- RF of loop [28:1]:
V
### Specialization of cost equations start/3
* CE 4 is refined into CE [48,49,50,51,52,53,54,55]
* CE 2 is refined into CE [56]
* CE 3 is refined into CE [57]
* CE 5 is refined into CE [58,59,60,61,62]
* CE 6 is refined into CE [63,64]
* CE 7 is refined into CE [65,66,67]
* CE 8 is refined into CE [68,69,70,71,72,73,74]
### Cost equations --> "Loop" of start/3
* CEs [71] --> Loop 36
* CEs [59,65,70] --> Loop 37
* CEs [52] --> Loop 38
* CEs [48,49,50,51,53,54,55] --> Loop 39
* CEs [69] --> Loop 40
* CEs [57] --> Loop 41
* CEs [56,58,60,61,62,63,64,66,67,68,72,73,74] --> Loop 42
### Ranking functions of CR start(V,V1,V14)
#### Partial ranking functions of CR start(V,V1,V14)
Computing Bounds
=====================================
#### Cost of chains of pred(V,Out):
* Chain [17]: 0
with precondition: [Out=0,V>=0]
* Chain [16]: 1
with precondition: [V=Out+1,V>=1]
#### Cost of chains of minus(V,V1,Out):
* Chain [[19],[18],21]: 3*it(18)+1
Such that:aux(1) =< V1
it(18) =< aux(1)
with precondition: [Out=0,V>=1,V1>=2]
* Chain [[19],21]: 1*it(19)+1
Such that:it(19) =< V1
with precondition: [Out=0,V>=0,V1>=1]
* Chain [[19],20]: 1*it(19)+0
Such that:it(19) =< V1
with precondition: [Out=0,V>=0,V1>=1]
* Chain [[18],21]: 2*it(18)+1
Such that:it(18) =< V1
with precondition: [V=Out+V1,V1>=1,V>=V1]
* Chain [21]: 1
with precondition: [V1=0,V=Out,V>=0]
* Chain [20]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of le(V,V1,Out):
* Chain [[22],25]: 1*it(22)+1
Such that:it(22) =< V
with precondition: [Out=2,V>=1,V1>=V]
* Chain [[22],24]: 1*it(22)+1
Such that:it(22) =< V1
with precondition: [Out=1,V1>=1,V>=V1+1]
* Chain [[22],23]: 1*it(22)+0
Such that:it(22) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [25]: 1
with precondition: [V=0,Out=2,V1>=0]
* Chain [24]: 1
with precondition: [V1=0,Out=1,V>=1]
* Chain [23]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of mod(V,V1,Out):
* Chain [[28],35]: 6*it(28)+1*s(8)+2
Such that:s(8) =< 1
aux(4) =< V
it(28) =< aux(4)
with precondition: [V1=1,Out=0,V>=1]
* Chain [[28],31]: 4*it(28)+2
Such that:it(28) =< V
with precondition: [V1=1,Out=0,V>=2]
* Chain [[28],29,35]: 4*it(28)+1*s(8)+6
Such that:s(8) =< 1
it(28) =< V
with precondition: [V1=1,Out=0,V>=2]
* Chain [[26],35]: 9*it(26)+1*s(8)+2
Such that:s(8) =< V1
aux(8) =< V
it(26) =< aux(8)
with precondition: [Out=0,V1>=2,V>=V1]
* Chain [[26],34]: 4*it(26)+3*s(15)+2
Such that:it(26) =< V-V1+1
aux(9) =< V
it(26) =< aux(9)
s(15) =< aux(9)
with precondition: [Out=0,V1>=2,V>=V1+1]
* Chain [[26],33]: 4*it(26)+3*s(15)+3
Such that:it(26) =< V-V1+1
aux(10) =< V
it(26) =< aux(10)
s(15) =< aux(10)
with precondition: [Out=1,V1>=2,V>=V1+1]
* Chain [[26],30]: 4*it(26)+3*s(15)+1*s(17)+3
Such that:aux(6) =< V
it(26) =< V-V1+1
aux(7) =< V-Out
s(17) =< Out
it(26) =< aux(6)
s(16) =< aux(6)
it(26) =< aux(7)
s(16) =< aux(7)
s(15) =< s(16)
with precondition: [Out>=2,V1>=Out+1,V>=Out+V1]
* Chain [[26],27,35]: 4*it(26)+7*s(8)+3*s(15)+6
Such that:aux(6) =< V
aux(12) =< V1
aux(13) =< V-V1
it(26) =< aux(13)
s(8) =< aux(12)
it(26) =< aux(6)
s(16) =< aux(6)
s(16) =< aux(13)
s(15) =< s(16)
with precondition: [Out=0,V1>=2,V>=2*V1]
* Chain [35]: 2*s(6)+1*s(8)+2
Such that:s(8) =< V1
aux(3) =< V
s(6) =< aux(3)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [34]: 2
with precondition: [V=1,Out=0,V1>=2]
* Chain [33]: 3
with precondition: [V=1,Out=1,V1>=2]
* Chain [32]: 1
with precondition: [V1=0,Out=0,V>=1]
* Chain [31]: 2
with precondition: [V1=1,Out=0,V>=1]
* Chain [30]: 1*s(17)+3
Such that:s(17) =< V
with precondition: [V=Out,V>=2,V1>=V+1]
* Chain [29,35]: 1*s(8)+6
Such that:s(8) =< 1
with precondition: [V1=1,Out=0,V>=1]
* Chain [27,35]: 7*s(8)+6
Such that:aux(12) =< V1
s(8) =< aux(12)
with precondition: [Out=0,V1>=2,V>=V1]
#### Cost of chains of start(V,V1,V14):
* Chain [42]: 25*s(46)+23*s(48)+12*s(53)+4*s(57)+3*s(59)+6
Such that:s(52) =< V-V1
aux(19) =< V
aux(20) =< V-V1+1
aux(21) =< V1
s(48) =< aux(19)
s(53) =< aux(20)
s(46) =< aux(21)
s(57) =< s(52)
s(57) =< aux(19)
s(58) =< aux(19)
s(58) =< s(52)
s(59) =< s(58)
s(53) =< aux(19)
with precondition: [V>=0]
* Chain [41]: 1
with precondition: [V=1,V1>=1,V14>=1]
* Chain [40]: 3
with precondition: [V=1,V1>=2]
* Chain [39]: 39*s(72)+19*s(75)+45*s(85)+12*s(97)+4*s(101)+3*s(103)+22*s(104)+8
Such that:s(96) =< V1-2*V14
aux(26) =< 1
aux(27) =< V1
aux(28) =< V1-2*V14+1
aux(29) =< V1-V14
aux(30) =< V14
s(97) =< aux(28)
s(104) =< aux(29)
s(85) =< aux(30)
s(72) =< aux(27)
s(75) =< aux(26)
s(101) =< s(96)
s(101) =< aux(29)
s(102) =< aux(29)
s(102) =< s(96)
s(103) =< s(102)
s(97) =< aux(29)
with precondition: [V=2,V1>=1,V14>=1]
* Chain [38]: 2*s(118)+5
Such that:s(118) =< V14
with precondition: [V=2,V1=V14+1,V1>=3]
* Chain [37]: 1
with precondition: [V1=0,V>=0]
* Chain [36]: 3*s(121)+14*s(122)+6
Such that:s(119) =< 1
s(120) =< V
s(121) =< s(119)
s(122) =< s(120)
with precondition: [V1=1,V>=1]
Closed-form bounds of start(V,V1,V14):
-------------------------------------
* Chain [42] with precondition: [V>=0]
- Upper bound: 26*V+6+nat(V1)*25+nat(V-V1+1)*12+nat(V-V1)*4
- Complexity: n
* Chain [41] with precondition: [V=1,V1>=1,V14>=1]
- Upper bound: 1
- Complexity: constant
* Chain [40] with precondition: [V=1,V1>=2]
- Upper bound: 3
- Complexity: constant
* Chain [39] with precondition: [V=2,V1>=1,V14>=1]
- Upper bound: 39*V1+45*V14+27+nat(V1-2*V14+1)*12+nat(V1-V14)*25+nat(V1-2*V14)*4
- Complexity: n
* Chain [38] with precondition: [V=2,V1=V14+1,V1>=3]
- Upper bound: 2*V14+5
- Complexity: n
* Chain [37] with precondition: [V1=0,V>=0]
- Upper bound: 1
- Complexity: constant
* Chain [36] with precondition: [V1=1,V>=1]
- Upper bound: 14*V+9
- Complexity: n
### Maximum cost of start(V,V1,V14): max([14*V+3+max([3,nat(V1)*25+12*V+nat(V-V1+1)*12+nat(V-V1)*4]),nat(V1)*39+22+nat(V14)*43+nat(V1-2*V14+1)*12+nat(V1-V14)*25+nat(V1-2*V14)*4+ (nat(V14)*2+2)])+3
Asymptotic class: n
* Total analysis performed in 503 ms.