WORST_CASE(?,O(n^1))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. cons(A,B,C) -> m0(A,B,C) [A >= 0] (?,1)
1. m1(A,B,C) -> m2(A,B,C) [A >= 0] (?,1)
2. m4(A,B,C) -> m3(A,B,C) [A >= 0] (?,1)
3. m2(A,B,C) -> m4(A,B,C) [A >= 0] (?,1)
4. m5(A,B,C) -> m6(A,B,C) [A >= 1] (?,1)
5. m6(A,B,C) -> m8(A,B,C) [A >= 1] (?,1)
6. m9(A,B,C) -> n0(A,B,C) [A >= 1] (?,1)
7. n2(A,B,C) -> c2(n1(A,B,C),m5(A,B,C)) [A >= 1] (?,1)
8. n0(A,B,C) -> n2(A,B,C) [A >= 1] (?,1)
9. n4(A,B,C) -> n3(A,B,C) [B >= 0 && A >= 1 && A >= C && C >= A] (?,1)
10. n50(A,B,C) -> n4(A,C,A) True (?,1)
11. n51(A,B,C) -> cons(B,B,C) True (?,1)
12. n5(A,B,C) -> c2(n50(A,C,D),n51(A,C,D)) [D >= 1 && C >= 1 && A >= 1] (?,1)
13. n60(A,B,C) -> n4(A,C,A) True (?,1)
14. n61(A,B,C) -> m1(B,B,C) True (?,1)
15. n6(A,B,C) -> c2(n60(A,C,D),n61(A,C,D)) [C >= 0 && A >= 1 && C >= D && D >= C] (?,1)
16. n70(A,B,C) -> n8(A,B,C) True (?,1)
17. n71(A,B,C) -> m9(B,B,C) True (?,1)
18. n7(A,B,C) -> c2(n70(D,E,F),n71(D,E,F)) [E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] (?,1)
19. n8(A,B,C) -> n5(A,B,C) True (?,1)
20. n8(A,B,C) -> n6(A,B,C) True (?,1)
21. m0(A,B,C) -> n7(A,B,C) [A >= 0] (?,1)
22. m8(A,B,C) -> c2(m7(A,B,C),n9(A,B,C)) [A >= 1] (?,1)
23. start(A,B,C) -> cons(A,B,C) True (1,1)
Signature:
{(cons,3)
;(m0,3)
;(m1,3)
;(m2,3)
;(m3,3)
;(m4,3)
;(m5,3)
;(m6,3)
;(m7,3)
;(m8,3)
;(m9,3)
;(n0,3)
;(n1,3)
;(n2,3)
;(n3,3)
;(n4,3)
;(n5,3)
;(n50,3)
;(n51,3)
;(n6,3)
;(n60,3)
;(n61,3)
;(n7,3)
;(n70,3)
;(n71,3)
;(n8,3)
;(n9,3)
;(start,3)}
Flow Graph:
[0->{21},1->{3},2->{},3->{2},4->{5},5->{22},6->{8},7->{4},8->{7},9->{},10->{9},11->{0},12->{10,11},13->{9}
,14->{1},15->{13,14},16->{19,20},17->{6},18->{16,17},19->{12},20->{15},21->{18},22->{},23->{0}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,A>, A, .= 0) (< 0,0,B>, B, .= 0) (< 0,0,C>, C, .= 0)
(< 1,0,A>, A, .= 0) (< 1,0,B>, B, .= 0) (< 1,0,C>, C, .= 0)
(< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0) (< 2,0,C>, C, .= 0)
(< 3,0,A>, A, .= 0) (< 3,0,B>, B, .= 0) (< 3,0,C>, C, .= 0)
(< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 4,0,C>, C, .= 0)
(< 5,0,A>, A, .= 0) (< 5,0,B>, B, .= 0) (< 5,0,C>, C, .= 0)
(< 6,0,A>, A, .= 0) (< 6,0,B>, B, .= 0) (< 6,0,C>, C, .= 0)
(< 7,0,A>, A, .= 0) (< 7,0,B>, B, .= 0) (< 7,0,C>, C, .= 0)
(< 7,1,A>, A, .= 0) (< 7,1,B>, B, .= 0) (< 7,1,C>, C, .= 0)
(< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0) (< 8,0,C>, C, .= 0)
(< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, C, .= 0)
(<10,0,A>, A, .= 0) (<10,0,B>, C, .= 0) (<10,0,C>, A, .= 0)
(<11,0,A>, B, .= 0) (<11,0,B>, B, .= 0) (<11,0,C>, C, .= 0)
(<12,0,A>, A, .= 0) (<12,0,B>, C, .= 0) (<12,0,C>, ?, .?)
(<12,1,A>, A, .= 0) (<12,1,B>, C, .= 0) (<12,1,C>, ?, .?)
(<13,0,A>, A, .= 0) (<13,0,B>, C, .= 0) (<13,0,C>, A, .= 0)
(<14,0,A>, B, .= 0) (<14,0,B>, B, .= 0) (<14,0,C>, C, .= 0)
(<15,0,A>, A, .= 0) (<15,0,B>, C, .= 0) (<15,0,C>, C, .= 0)
(<15,1,A>, A, .= 0) (<15,1,B>, C, .= 0) (<15,1,C>, C, .= 0)
(<16,0,A>, A, .= 0) (<16,0,B>, B, .= 0) (<16,0,C>, C, .= 0)
(<17,0,A>, B, .= 0) (<17,0,B>, B, .= 0) (<17,0,C>, C, .= 0)
(<18,0,A>, ?, .?) (<18,0,B>, ?, .?) (<18,0,C>, 1 + A, .+ 1)
(<18,1,A>, ?, .?) (<18,1,B>, ?, .?) (<18,1,C>, 1 + A, .+ 1)
(<19,0,A>, A, .= 0) (<19,0,B>, B, .= 0) (<19,0,C>, C, .= 0)
(<20,0,A>, A, .= 0) (<20,0,B>, B, .= 0) (<20,0,C>, C, .= 0)
(<21,0,A>, A, .= 0) (<21,0,B>, B, .= 0) (<21,0,C>, C, .= 0)
(<22,0,A>, A, .= 0) (<22,0,B>, B, .= 0) (<22,0,C>, C, .= 0)
(<22,1,A>, A, .= 0) (<22,1,B>, B, .= 0) (<22,1,C>, C, .= 0)
(<23,0,A>, A, .= 0) (<23,0,B>, B, .= 0) (<23,0,C>, C, .= 0)
* Step 2: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. cons(A,B,C) -> m0(A,B,C) [A >= 0] (?,1)
1. m1(A,B,C) -> m2(A,B,C) [A >= 0] (?,1)
2. m4(A,B,C) -> m3(A,B,C) [A >= 0] (?,1)
3. m2(A,B,C) -> m4(A,B,C) [A >= 0] (?,1)
4. m5(A,B,C) -> m6(A,B,C) [A >= 1] (?,1)
5. m6(A,B,C) -> m8(A,B,C) [A >= 1] (?,1)
6. m9(A,B,C) -> n0(A,B,C) [A >= 1] (?,1)
7. n2(A,B,C) -> c2(n1(A,B,C),m5(A,B,C)) [A >= 1] (?,1)
8. n0(A,B,C) -> n2(A,B,C) [A >= 1] (?,1)
9. n4(A,B,C) -> n3(A,B,C) [B >= 0 && A >= 1 && A >= C && C >= A] (?,1)
10. n50(A,B,C) -> n4(A,C,A) True (?,1)
11. n51(A,B,C) -> cons(B,B,C) True (?,1)
12. n5(A,B,C) -> c2(n50(A,C,D),n51(A,C,D)) [D >= 1 && C >= 1 && A >= 1] (?,1)
13. n60(A,B,C) -> n4(A,C,A) True (?,1)
14. n61(A,B,C) -> m1(B,B,C) True (?,1)
15. n6(A,B,C) -> c2(n60(A,C,D),n61(A,C,D)) [C >= 0 && A >= 1 && C >= D && D >= C] (?,1)
16. n70(A,B,C) -> n8(A,B,C) True (?,1)
17. n71(A,B,C) -> m9(B,B,C) True (?,1)
18. n7(A,B,C) -> c2(n70(D,E,F),n71(D,E,F)) [E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] (?,1)
19. n8(A,B,C) -> n5(A,B,C) True (?,1)
20. n8(A,B,C) -> n6(A,B,C) True (?,1)
21. m0(A,B,C) -> n7(A,B,C) [A >= 0] (?,1)
22. m8(A,B,C) -> c2(m7(A,B,C),n9(A,B,C)) [A >= 1] (?,1)
23. start(A,B,C) -> cons(A,B,C) True (1,1)
Signature:
{(cons,3)
;(m0,3)
;(m1,3)
;(m2,3)
;(m3,3)
;(m4,3)
;(m5,3)
;(m6,3)
;(m7,3)
;(m8,3)
;(m9,3)
;(n0,3)
;(n1,3)
;(n2,3)
;(n3,3)
;(n4,3)
;(n5,3)
;(n50,3)
;(n51,3)
;(n6,3)
;(n60,3)
;(n61,3)
;(n7,3)
;(n70,3)
;(n71,3)
;(n8,3)
;(n9,3)
;(start,3)}
Flow Graph:
[0->{21},1->{3},2->{},3->{2},4->{5},5->{22},6->{8},7->{4},8->{7},9->{},10->{9},11->{0},12->{10,11},13->{9}
,14->{1},15->{13,14},16->{19,20},17->{6},18->{16,17},19->{12},20->{15},21->{18},22->{},23->{0}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?)
(< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 7,1,A>, ?) (< 7,1,B>, ?) (< 7,1,C>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?)
(<12,1,A>, ?) (<12,1,B>, ?) (<12,1,C>, ?)
(<13,0,A>, ?) (<13,0,B>, ?) (<13,0,C>, ?)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?)
(<15,1,A>, ?) (<15,1,B>, ?) (<15,1,C>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?)
(<17,0,A>, ?) (<17,0,B>, ?) (<17,0,C>, ?)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?)
(<18,1,A>, ?) (<18,1,B>, ?) (<18,1,C>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, ?) (<22,0,B>, ?) (<22,0,C>, ?)
(<22,1,A>, ?) (<22,1,B>, ?) (<22,1,C>, ?)
(<23,0,A>, ?) (<23,0,B>, ?) (<23,0,C>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?)
(< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 7,1,A>, ?) (< 7,1,B>, ?) (< 7,1,C>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?)
(<12,1,A>, ?) (<12,1,B>, ?) (<12,1,C>, ?)
(<13,0,A>, ?) (<13,0,B>, ?) (<13,0,C>, ?)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?)
(<15,1,A>, ?) (<15,1,B>, ?) (<15,1,C>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?)
(<17,0,A>, ?) (<17,0,B>, ?) (<17,0,C>, ?)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?)
(<18,1,A>, ?) (<18,1,B>, ?) (<18,1,C>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, ?) (<22,0,B>, ?) (<22,0,C>, ?)
(<22,1,A>, ?) (<22,1,B>, ?) (<22,1,C>, ?)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, C)
* Step 3: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. cons(A,B,C) -> m0(A,B,C) [A >= 0] (?,1)
1. m1(A,B,C) -> m2(A,B,C) [A >= 0] (?,1)
2. m4(A,B,C) -> m3(A,B,C) [A >= 0] (?,1)
3. m2(A,B,C) -> m4(A,B,C) [A >= 0] (?,1)
4. m5(A,B,C) -> m6(A,B,C) [A >= 1] (?,1)
5. m6(A,B,C) -> m8(A,B,C) [A >= 1] (?,1)
6. m9(A,B,C) -> n0(A,B,C) [A >= 1] (?,1)
7. n2(A,B,C) -> c2(n1(A,B,C),m5(A,B,C)) [A >= 1] (?,1)
8. n0(A,B,C) -> n2(A,B,C) [A >= 1] (?,1)
9. n4(A,B,C) -> n3(A,B,C) [B >= 0 && A >= 1 && A >= C && C >= A] (?,1)
10. n50(A,B,C) -> n4(A,C,A) True (?,1)
11. n51(A,B,C) -> cons(B,B,C) True (?,1)
12. n5(A,B,C) -> c2(n50(A,C,D),n51(A,C,D)) [D >= 1 && C >= 1 && A >= 1] (?,1)
13. n60(A,B,C) -> n4(A,C,A) True (?,1)
14. n61(A,B,C) -> m1(B,B,C) True (?,1)
15. n6(A,B,C) -> c2(n60(A,C,D),n61(A,C,D)) [C >= 0 && A >= 1 && C >= D && D >= C] (?,1)
16. n70(A,B,C) -> n8(A,B,C) True (?,1)
17. n71(A,B,C) -> m9(B,B,C) True (?,1)
18. n7(A,B,C) -> c2(n70(D,E,F),n71(D,E,F)) [E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] (?,1)
19. n8(A,B,C) -> n5(A,B,C) True (?,1)
20. n8(A,B,C) -> n6(A,B,C) True (?,1)
21. m0(A,B,C) -> n7(A,B,C) [A >= 0] (?,1)
22. m8(A,B,C) -> c2(m7(A,B,C),n9(A,B,C)) [A >= 1] (?,1)
23. start(A,B,C) -> cons(A,B,C) True (1,1)
Signature:
{(cons,3)
;(m0,3)
;(m1,3)
;(m2,3)
;(m3,3)
;(m4,3)
;(m5,3)
;(m6,3)
;(m7,3)
;(m8,3)
;(m9,3)
;(n0,3)
;(n1,3)
;(n2,3)
;(n3,3)
;(n4,3)
;(n5,3)
;(n50,3)
;(n51,3)
;(n6,3)
;(n60,3)
;(n61,3)
;(n7,3)
;(n70,3)
;(n71,3)
;(n8,3)
;(n9,3)
;(start,3)}
Flow Graph:
[0->{21},1->{3},2->{},3->{2},4->{5},5->{22},6->{8},7->{4},8->{7},9->{},10->{9},11->{0},12->{10,11},13->{9}
,14->{1},15->{13,14},16->{19,20},17->{6},18->{16,17},19->{12},20->{15},21->{18},22->{},23->{0}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?)
(< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 7,1,A>, ?) (< 7,1,B>, ?) (< 7,1,C>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?)
(<12,1,A>, ?) (<12,1,B>, ?) (<12,1,C>, ?)
(<13,0,A>, ?) (<13,0,B>, ?) (<13,0,C>, ?)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?)
(<15,1,A>, ?) (<15,1,B>, ?) (<15,1,C>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?)
(<17,0,A>, ?) (<17,0,B>, ?) (<17,0,C>, ?)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?)
(<18,1,A>, ?) (<18,1,B>, ?) (<18,1,C>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,C>, ?)
(<22,0,A>, ?) (<22,0,B>, ?) (<22,0,C>, ?)
(<22,1,A>, ?) (<22,1,B>, ?) (<22,1,C>, ?)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, C)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [17
,6
,20
,8
,15
,7
,14
,1
,4
,3
,5
,10
,13
,2
,9
,22]
* Step 4: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. cons(A,B,C) -> m0(A,B,C) [A >= 0] (?,1)
11. n51(A,B,C) -> cons(B,B,C) True (?,1)
12. n5(A,B,C) -> c2(n50(A,C,D),n51(A,C,D)) [D >= 1 && C >= 1 && A >= 1] (?,1)
16. n70(A,B,C) -> n8(A,B,C) True (?,1)
18. n7(A,B,C) -> c2(n70(D,E,F),n71(D,E,F)) [E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] (?,1)
19. n8(A,B,C) -> n5(A,B,C) True (?,1)
21. m0(A,B,C) -> n7(A,B,C) [A >= 0] (?,1)
23. start(A,B,C) -> cons(A,B,C) True (1,1)
Signature:
{(cons,3)
;(m0,3)
;(m1,3)
;(m2,3)
;(m3,3)
;(m4,3)
;(m5,3)
;(m6,3)
;(m7,3)
;(m8,3)
;(m9,3)
;(n0,3)
;(n1,3)
;(n2,3)
;(n3,3)
;(n4,3)
;(n5,3)
;(n50,3)
;(n51,3)
;(n6,3)
;(n60,3)
;(n61,3)
;(n7,3)
;(n70,3)
;(n71,3)
;(n8,3)
;(n9,3)
;(start,3)}
Flow Graph:
[0->{21},11->{0},12->{11},16->{19},18->{16},19->{12},21->{18},23->{0}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?)
(<12,1,A>, ?) (<12,1,B>, ?) (<12,1,C>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?)
(<18,1,A>, ?) (<18,1,B>, ?) (<18,1,C>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, C)
+ Applied Processor:
ChainProcessor False [0,11,12,16,18,19,21,23]
+ Details:
We chained rule 0 to obtain the rules [24] .
* Step 5: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
11. n51(A,B,C) -> cons(B,B,C) True (?,1)
12. n5(A,B,C) -> c2(n50(A,C,D),n51(A,C,D)) [D >= 1 && C >= 1 && A >= 1] (?,1)
16. n70(A,B,C) -> n8(A,B,C) True (?,1)
18. n7(A,B,C) -> c2(n70(D,E,F),n71(D,E,F)) [E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] (?,1)
19. n8(A,B,C) -> n5(A,B,C) True (?,1)
21. m0(A,B,C) -> n7(A,B,C) [A >= 0] (?,1)
23. start(A,B,C) -> cons(A,B,C) True (1,1)
24. cons(A,B,C) -> n7(A,B,C) [A >= 0 && A >= 0] (?,2)
Signature:
{(cons,3)
;(m0,3)
;(m1,3)
;(m2,3)
;(m3,3)
;(m4,3)
;(m5,3)
;(m6,3)
;(m7,3)
;(m8,3)
;(m9,3)
;(n0,3)
;(n1,3)
;(n2,3)
;(n3,3)
;(n4,3)
;(n5,3)
;(n50,3)
;(n51,3)
;(n6,3)
;(n60,3)
;(n61,3)
;(n7,3)
;(n70,3)
;(n71,3)
;(n8,3)
;(n9,3)
;(start,3)}
Flow Graph:
[11->{24},12->{11},16->{19},18->{16},19->{12},21->{18},23->{24},24->{18}]
Sizebounds:
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?)
(<12,1,A>, ?) (<12,1,B>, ?) (<12,1,C>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?)
(<18,1,A>, ?) (<18,1,B>, ?) (<18,1,C>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, C)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,C>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [21]
* Step 6: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
11. n51(A,B,C) -> cons(B,B,C) True (?,1)
12. n5(A,B,C) -> c2(n50(A,C,D),n51(A,C,D)) [D >= 1 && C >= 1 && A >= 1] (?,1)
16. n70(A,B,C) -> n8(A,B,C) True (?,1)
18. n7(A,B,C) -> c2(n70(D,E,F),n71(D,E,F)) [E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] (?,1)
19. n8(A,B,C) -> n5(A,B,C) True (?,1)
23. start(A,B,C) -> cons(A,B,C) True (1,1)
24. cons(A,B,C) -> n7(A,B,C) [A >= 0 && A >= 0] (?,2)
Signature:
{(cons,3)
;(m0,3)
;(m1,3)
;(m2,3)
;(m3,3)
;(m4,3)
;(m5,3)
;(m6,3)
;(m7,3)
;(m8,3)
;(m9,3)
;(n0,3)
;(n1,3)
;(n2,3)
;(n3,3)
;(n4,3)
;(n5,3)
;(n50,3)
;(n51,3)
;(n6,3)
;(n60,3)
;(n61,3)
;(n7,3)
;(n70,3)
;(n71,3)
;(n8,3)
;(n9,3)
;(start,3)}
Flow Graph:
[11->{24},12->{11},16->{19},18->{16},19->{12},23->{24},24->{18}]
Sizebounds:
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?)
(<12,1,A>, ?) (<12,1,B>, ?) (<12,1,C>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?)
(<18,1,A>, ?) (<18,1,B>, ?) (<18,1,C>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, C)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,C>, ?)
+ Applied Processor:
ChainProcessor False [11,12,16,18,19,23,24]
+ Details:
We chained rule 11 to obtain the rules [25] .
* Step 7: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
12. n5(A,B,C) -> c2(n50(A,C,D),n51(A,C,D)) [D >= 1 && C >= 1 && A >= 1] (?,1)
16. n70(A,B,C) -> n8(A,B,C) True (?,1)
18. n7(A,B,C) -> c2(n70(D,E,F),n71(D,E,F)) [E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] (?,1)
19. n8(A,B,C) -> n5(A,B,C) True (?,1)
23. start(A,B,C) -> cons(A,B,C) True (1,1)
24. cons(A,B,C) -> n7(A,B,C) [A >= 0 && A >= 0] (?,2)
25. n51(A,B,C) -> n7(B,B,C) [B >= 0 && B >= 0] (?,3)
Signature:
{(cons,3)
;(m0,3)
;(m1,3)
;(m2,3)
;(m3,3)
;(m4,3)
;(m5,3)
;(m6,3)
;(m7,3)
;(m8,3)
;(m9,3)
;(n0,3)
;(n1,3)
;(n2,3)
;(n3,3)
;(n4,3)
;(n5,3)
;(n50,3)
;(n51,3)
;(n6,3)
;(n60,3)
;(n61,3)
;(n7,3)
;(n70,3)
;(n71,3)
;(n8,3)
;(n9,3)
;(start,3)}
Flow Graph:
[12->{25},16->{19},18->{16},19->{12},23->{24},24->{18},25->{18}]
Sizebounds:
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?)
(<12,1,A>, ?) (<12,1,B>, ?) (<12,1,C>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?)
(<18,1,A>, ?) (<18,1,B>, ?) (<18,1,C>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, C)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,C>, ?)
(<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?)
+ Applied Processor:
ChainProcessor False [12,16,18,19,23,24,25]
+ Details:
We chained rule 12 to obtain the rules [26] .
* Step 8: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
16. n70(A,B,C) -> n8(A,B,C) True (?,1)
18. n7(A,B,C) -> c2(n70(D,E,F),n71(D,E,F)) [E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] (?,1)
19. n8(A,B,C) -> n5(A,B,C) True (?,1)
23. start(A,B,C) -> cons(A,B,C) True (1,1)
24. cons(A,B,C) -> n7(A,B,C) [A >= 0 && A >= 0] (?,2)
25. n51(A,B,C) -> n7(B,B,C) [B >= 0 && B >= 0] (?,3)
26. n5(A,B,C) -> c2(n50(A,C,D),n7(C,C,D)) [D >= 1 && C >= 1 && A >= 1 && C >= 0 && C >= 0] (?,4)
Signature:
{(cons,3)
;(m0,3)
;(m1,3)
;(m2,3)
;(m3,3)
;(m4,3)
;(m5,3)
;(m6,3)
;(m7,3)
;(m8,3)
;(m9,3)
;(n0,3)
;(n1,3)
;(n2,3)
;(n3,3)
;(n4,3)
;(n5,3)
;(n50,3)
;(n51,3)
;(n6,3)
;(n60,3)
;(n61,3)
;(n7,3)
;(n70,3)
;(n71,3)
;(n8,3)
;(n9,3)
;(start,3)}
Flow Graph:
[16->{19},18->{16},19->{26},23->{24},24->{18},25->{18},26->{18}]
Sizebounds:
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?)
(<18,1,A>, ?) (<18,1,B>, ?) (<18,1,C>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, C)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,C>, ?)
(<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [25]
* Step 9: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
16. n70(A,B,C) -> n8(A,B,C) True (?,1)
18. n7(A,B,C) -> c2(n70(D,E,F),n71(D,E,F)) [E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] (?,1)
19. n8(A,B,C) -> n5(A,B,C) True (?,1)
23. start(A,B,C) -> cons(A,B,C) True (1,1)
24. cons(A,B,C) -> n7(A,B,C) [A >= 0 && A >= 0] (?,2)
26. n5(A,B,C) -> c2(n50(A,C,D),n7(C,C,D)) [D >= 1 && C >= 1 && A >= 1 && C >= 0 && C >= 0] (?,4)
Signature:
{(cons,3)
;(m0,3)
;(m1,3)
;(m2,3)
;(m3,3)
;(m4,3)
;(m5,3)
;(m6,3)
;(m7,3)
;(m8,3)
;(m9,3)
;(n0,3)
;(n1,3)
;(n2,3)
;(n3,3)
;(n4,3)
;(n5,3)
;(n50,3)
;(n51,3)
;(n6,3)
;(n60,3)
;(n61,3)
;(n7,3)
;(n70,3)
;(n71,3)
;(n8,3)
;(n9,3)
;(start,3)}
Flow Graph:
[16->{19},18->{16},19->{26},23->{24},24->{18},26->{18}]
Sizebounds:
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?)
(<18,1,A>, ?) (<18,1,B>, ?) (<18,1,C>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, C)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,C>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?)
+ Applied Processor:
ChainProcessor False [16,18,19,23,24,26]
+ Details:
We chained rule 16 to obtain the rules [27] .
* Step 10: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
18. n7(A,B,C) -> c2(n70(D,E,F),n71(D,E,F)) [E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] (?,1)
19. n8(A,B,C) -> n5(A,B,C) True (?,1)
23. start(A,B,C) -> cons(A,B,C) True (1,1)
24. cons(A,B,C) -> n7(A,B,C) [A >= 0 && A >= 0] (?,2)
26. n5(A,B,C) -> c2(n50(A,C,D),n7(C,C,D)) [D >= 1 && C >= 1 && A >= 1 && C >= 0 && C >= 0] (?,4)
27. n70(A,B,C) -> n5(A,B,C) True (?,2)
Signature:
{(cons,3)
;(m0,3)
;(m1,3)
;(m2,3)
;(m3,3)
;(m4,3)
;(m5,3)
;(m6,3)
;(m7,3)
;(m8,3)
;(m9,3)
;(n0,3)
;(n1,3)
;(n2,3)
;(n3,3)
;(n4,3)
;(n5,3)
;(n50,3)
;(n51,3)
;(n6,3)
;(n60,3)
;(n61,3)
;(n7,3)
;(n70,3)
;(n71,3)
;(n8,3)
;(n9,3)
;(start,3)}
Flow Graph:
[18->{27},19->{26},23->{24},24->{18},26->{18},27->{26}]
Sizebounds:
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?)
(<18,1,A>, ?) (<18,1,B>, ?) (<18,1,C>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, C)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,C>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [19]
* Step 11: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
18. n7(A,B,C) -> c2(n70(D,E,F),n71(D,E,F)) [E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] (?,1)
23. start(A,B,C) -> cons(A,B,C) True (1,1)
24. cons(A,B,C) -> n7(A,B,C) [A >= 0 && A >= 0] (?,2)
26. n5(A,B,C) -> c2(n50(A,C,D),n7(C,C,D)) [D >= 1 && C >= 1 && A >= 1 && C >= 0 && C >= 0] (?,4)
27. n70(A,B,C) -> n5(A,B,C) True (?,2)
Signature:
{(cons,3)
;(m0,3)
;(m1,3)
;(m2,3)
;(m3,3)
;(m4,3)
;(m5,3)
;(m6,3)
;(m7,3)
;(m8,3)
;(m9,3)
;(n0,3)
;(n1,3)
;(n2,3)
;(n3,3)
;(n4,3)
;(n5,3)
;(n50,3)
;(n51,3)
;(n6,3)
;(n60,3)
;(n61,3)
;(n7,3)
;(n70,3)
;(n71,3)
;(n8,3)
;(n9,3)
;(start,3)}
Flow Graph:
[18->{27},23->{24},24->{18},26->{18},27->{26}]
Sizebounds:
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?)
(<18,1,A>, ?) (<18,1,B>, ?) (<18,1,C>, ?)
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, C)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,C>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, ?)
+ Applied Processor:
ChainProcessor False [18,23,24,26,27]
+ Details:
We chained rule 18 to obtain the rules [28] .
* Step 12: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
23. start(A,B,C) -> cons(A,B,C) True (1,1)
24. cons(A,B,C) -> n7(A,B,C) [A >= 0 && A >= 0] (?,2)
26. n5(A,B,C) -> c2(n50(A,C,D),n7(C,C,D)) [D >= 1 && C >= 1 && A >= 1 && C >= 0 && C >= 0] (?,4)
27. n70(A,B,C) -> n5(A,B,C) True (?,2)
28. n7(A,B,C) -> c2(n5(D,E,F),n71(D,E,F)) [E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] (?,3)
Signature:
{(cons,3)
;(m0,3)
;(m1,3)
;(m2,3)
;(m3,3)
;(m4,3)
;(m5,3)
;(m6,3)
;(m7,3)
;(m8,3)
;(m9,3)
;(n0,3)
;(n1,3)
;(n2,3)
;(n3,3)
;(n4,3)
;(n5,3)
;(n50,3)
;(n51,3)
;(n6,3)
;(n60,3)
;(n61,3)
;(n7,3)
;(n70,3)
;(n71,3)
;(n8,3)
;(n9,3)
;(start,3)}
Flow Graph:
[23->{24},24->{28},26->{28},27->{26},28->{26}]
Sizebounds:
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, C)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,C>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [27]
* Step 13: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
23. start(A,B,C) -> cons(A,B,C) True (1,1)
24. cons(A,B,C) -> n7(A,B,C) [A >= 0 && A >= 0] (?,2)
26. n5(A,B,C) -> c2(n50(A,C,D),n7(C,C,D)) [D >= 1 && C >= 1 && A >= 1 && C >= 0 && C >= 0] (?,4)
28. n7(A,B,C) -> c2(n5(D,E,F),n71(D,E,F)) [E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] (?,3)
Signature:
{(cons,3)
;(m0,3)
;(m1,3)
;(m2,3)
;(m3,3)
;(m4,3)
;(m5,3)
;(m6,3)
;(m7,3)
;(m8,3)
;(m9,3)
;(n0,3)
;(n1,3)
;(n2,3)
;(n3,3)
;(n4,3)
;(n5,3)
;(n50,3)
;(n51,3)
;(n6,3)
;(n60,3)
;(n61,3)
;(n7,3)
;(n70,3)
;(n71,3)
;(n8,3)
;(n9,3)
;(start,3)}
Flow Graph:
[23->{24},24->{28},26->{28},28->{26}]
Sizebounds:
(<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, C)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,C>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?)
+ Applied Processor:
ChainProcessor False [23,24,26,28]
+ Details:
We chained rule 23 to obtain the rules [29] .
* Step 14: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
24. cons(A,B,C) -> n7(A,B,C) [A >= 0 && A >= 0] (?,2)
26. n5(A,B,C) -> c2(n50(A,C,D),n7(C,C,D)) [D >= 1 && C >= 1 && A >= 1 && C >= 0 && C >= 0] (?,4)
28. n7(A,B,C) -> c2(n5(D,E,F),n71(D,E,F)) [E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] (?,3)
29. start(A,B,C) -> n7(A,B,C) [A >= 0 && A >= 0] (1,3)
Signature:
{(cons,3)
;(m0,3)
;(m1,3)
;(m2,3)
;(m3,3)
;(m4,3)
;(m5,3)
;(m6,3)
;(m7,3)
;(m8,3)
;(m9,3)
;(n0,3)
;(n1,3)
;(n2,3)
;(n3,3)
;(n4,3)
;(n5,3)
;(n50,3)
;(n51,3)
;(n6,3)
;(n60,3)
;(n61,3)
;(n7,3)
;(n70,3)
;(n71,3)
;(n8,3)
;(n9,3)
;(start,3)}
Flow Graph:
[24->{28},26->{28},28->{26},29->{28}]
Sizebounds:
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,C>, ?)
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?)
(<29,0,A>, ?) (<29,0,B>, ?) (<29,0,C>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [24]
* Step 15: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
26. n5(A,B,C) -> c2(n50(A,C,D),n7(C,C,D)) [D >= 1 && C >= 1 && A >= 1 && C >= 0 && C >= 0] (?,4)
28. n7(A,B,C) -> c2(n5(D,E,F),n71(D,E,F)) [E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] (?,3)
29. start(A,B,C) -> n7(A,B,C) [A >= 0 && A >= 0] (1,3)
Signature:
{(cons,3)
;(m0,3)
;(m1,3)
;(m2,3)
;(m3,3)
;(m4,3)
;(m5,3)
;(m6,3)
;(m7,3)
;(m8,3)
;(m9,3)
;(n0,3)
;(n1,3)
;(n2,3)
;(n3,3)
;(n4,3)
;(n5,3)
;(n50,3)
;(n51,3)
;(n6,3)
;(n60,3)
;(n61,3)
;(n7,3)
;(n70,3)
;(n71,3)
;(n8,3)
;(n9,3)
;(start,3)}
Flow Graph:
[26->{28},28->{26},29->{28}]
Sizebounds:
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?)
(<29,0,A>, ?) (<29,0,B>, ?) (<29,0,C>, ?)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<26,0,A>, A, .= 0) (<26,0,B>, C, .= 0) (<26,0,C>, ?, .?)
(<26,1,A>, C, .= 0) (<26,1,B>, C, .= 0) (<26,1,C>, ?, .?)
(<28,0,A>, ?, .?) (<28,0,B>, ?, .?) (<28,0,C>, 1 + A, .+ 1)
(<28,1,A>, ?, .?) (<28,1,B>, ?, .?) (<28,1,C>, 1 + A, .+ 1)
(<29,0,A>, A, .= 0) (<29,0,B>, B, .= 0) (<29,0,C>, C, .= 0)
* Step 16: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
26. n5(A,B,C) -> c2(n50(A,C,D),n7(C,C,D)) [D >= 1 && C >= 1 && A >= 1 && C >= 0 && C >= 0] (?,4)
28. n7(A,B,C) -> c2(n5(D,E,F),n71(D,E,F)) [E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] (?,3)
29. start(A,B,C) -> n7(A,B,C) [A >= 0 && A >= 0] (1,3)
Signature:
{(cons,3)
;(m0,3)
;(m1,3)
;(m2,3)
;(m3,3)
;(m4,3)
;(m5,3)
;(m6,3)
;(m7,3)
;(m8,3)
;(m9,3)
;(n0,3)
;(n1,3)
;(n2,3)
;(n3,3)
;(n4,3)
;(n5,3)
;(n50,3)
;(n51,3)
;(n6,3)
;(n60,3)
;(n61,3)
;(n7,3)
;(n70,3)
;(n71,3)
;(n8,3)
;(n9,3)
;(start,3)}
Flow Graph:
[26->{28},28->{26},29->{28}]
Sizebounds:
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?)
(<26,1,A>, ?) (<26,1,B>, ?) (<26,1,C>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?)
(<28,1,A>, ?) (<28,1,B>, ?) (<28,1,C>, ?)
(<29,0,A>, ?) (<29,0,B>, ?) (<29,0,C>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?)
(<26,1,A>, ?) (<26,1,B>, ?) (<26,1,C>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?)
(<28,1,A>, ?) (<28,1,B>, ?) (<28,1,C>, ?)
(<29,0,A>, A) (<29,0,B>, B) (<29,0,C>, C)
* Step 17: LocationConstraintsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
26. n5(A,B,C) -> c2(n50(A,C,D),n7(C,C,D)) [D >= 1 && C >= 1 && A >= 1 && C >= 0 && C >= 0] (?,4)
28. n7(A,B,C) -> c2(n5(D,E,F),n71(D,E,F)) [E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] (?,3)
29. start(A,B,C) -> n7(A,B,C) [A >= 0 && A >= 0] (1,3)
Signature:
{(cons,3)
;(m0,3)
;(m1,3)
;(m2,3)
;(m3,3)
;(m4,3)
;(m5,3)
;(m6,3)
;(m7,3)
;(m8,3)
;(m9,3)
;(n0,3)
;(n1,3)
;(n2,3)
;(n3,3)
;(n4,3)
;(n5,3)
;(n50,3)
;(n51,3)
;(n6,3)
;(n60,3)
;(n61,3)
;(n7,3)
;(n70,3)
;(n71,3)
;(n8,3)
;(n9,3)
;(start,3)}
Flow Graph:
[26->{28},28->{26},29->{28}]
Sizebounds:
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?)
(<26,1,A>, ?) (<26,1,B>, ?) (<26,1,C>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?)
(<28,1,A>, ?) (<28,1,B>, ?) (<28,1,C>, ?)
(<29,0,A>, A) (<29,0,B>, B) (<29,0,C>, C)
+ Applied Processor:
LocationConstraintsProc
+ Details:
We computed the location constraints 26 : True 28 : True 29 : True .
* Step 18: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
26. n5(A,B,C) -> c2(n50(A,C,D),n7(C,C,D)) [D >= 1 && C >= 1 && A >= 1 && C >= 0 && C >= 0] (?,4)
28. n7(A,B,C) -> c2(n5(D,E,F),n71(D,E,F)) [E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] (?,3)
29. start(A,B,C) -> n7(A,B,C) [A >= 0 && A >= 0] (1,3)
Signature:
{(cons,3)
;(m0,3)
;(m1,3)
;(m2,3)
;(m3,3)
;(m4,3)
;(m5,3)
;(m6,3)
;(m7,3)
;(m8,3)
;(m9,3)
;(n0,3)
;(n1,3)
;(n2,3)
;(n3,3)
;(n4,3)
;(n5,3)
;(n50,3)
;(n51,3)
;(n6,3)
;(n60,3)
;(n61,3)
;(n7,3)
;(n70,3)
;(n71,3)
;(n8,3)
;(n9,3)
;(start,3)}
Flow Graph:
[26->{28},28->{26},29->{28}]
Sizebounds:
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?)
(<26,1,A>, ?) (<26,1,B>, ?) (<26,1,C>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?)
(<28,1,A>, ?) (<28,1,B>, ?) (<28,1,C>, ?)
(<29,0,A>, A) (<29,0,B>, B) (<29,0,C>, C)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(n5) = x3
p(n50) = 0
p(n7) = x1
p(n71) = 0
p(start) = x1
The following rules are strictly oriented:
[E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] ==>
n7(A,B,C) = A
> F
= c2(n5(D,E,F),n71(D,E,F))
The following rules are weakly oriented:
[D >= 1 && C >= 1 && A >= 1 && C >= 0 && C >= 0] ==>
n5(A,B,C) = C
>= C
= c2(n50(A,C,D),n7(C,C,D))
[A >= 0 && A >= 0] ==>
start(A,B,C) = A
>= A
= n7(A,B,C)
* Step 19: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
26. n5(A,B,C) -> c2(n50(A,C,D),n7(C,C,D)) [D >= 1 && C >= 1 && A >= 1 && C >= 0 && C >= 0] (?,4)
28. n7(A,B,C) -> c2(n5(D,E,F),n71(D,E,F)) [E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] (A,3)
29. start(A,B,C) -> n7(A,B,C) [A >= 0 && A >= 0] (1,3)
Signature:
{(cons,3)
;(m0,3)
;(m1,3)
;(m2,3)
;(m3,3)
;(m4,3)
;(m5,3)
;(m6,3)
;(m7,3)
;(m8,3)
;(m9,3)
;(n0,3)
;(n1,3)
;(n2,3)
;(n3,3)
;(n4,3)
;(n5,3)
;(n50,3)
;(n51,3)
;(n6,3)
;(n60,3)
;(n61,3)
;(n7,3)
;(n70,3)
;(n71,3)
;(n8,3)
;(n9,3)
;(start,3)}
Flow Graph:
[26->{28},28->{26},29->{28}]
Sizebounds:
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?)
(<26,1,A>, ?) (<26,1,B>, ?) (<26,1,C>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?)
(<28,1,A>, ?) (<28,1,B>, ?) (<28,1,C>, ?)
(<29,0,A>, A) (<29,0,B>, B) (<29,0,C>, C)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(n5) = 1 + x3
p(n50) = 0
p(n7) = x1
p(n71) = 0
p(start) = x1
The following rules are strictly oriented:
[D >= 1 && C >= 1 && A >= 1 && C >= 0 && C >= 0] ==>
n5(A,B,C) = 1 + C
> C
= c2(n50(A,C,D),n7(C,C,D))
The following rules are weakly oriented:
[E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] ==>
n7(A,B,C) = A
>= 1 + F
= c2(n5(D,E,F),n71(D,E,F))
[A >= 0 && A >= 0] ==>
start(A,B,C) = A
>= A
= n7(A,B,C)
* Step 20: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
26. n5(A,B,C) -> c2(n50(A,C,D),n7(C,C,D)) [D >= 1 && C >= 1 && A >= 1 && C >= 0 && C >= 0] (A,4)
28. n7(A,B,C) -> c2(n5(D,E,F),n71(D,E,F)) [E >= 1 && D >= 1 && F >= 0 && A >= 1 + F] (A,3)
29. start(A,B,C) -> n7(A,B,C) [A >= 0 && A >= 0] (1,3)
Signature:
{(cons,3)
;(m0,3)
;(m1,3)
;(m2,3)
;(m3,3)
;(m4,3)
;(m5,3)
;(m6,3)
;(m7,3)
;(m8,3)
;(m9,3)
;(n0,3)
;(n1,3)
;(n2,3)
;(n3,3)
;(n4,3)
;(n5,3)
;(n50,3)
;(n51,3)
;(n6,3)
;(n60,3)
;(n61,3)
;(n7,3)
;(n70,3)
;(n71,3)
;(n8,3)
;(n9,3)
;(start,3)}
Flow Graph:
[26->{28},28->{26},29->{28}]
Sizebounds:
(<26,0,A>, ?) (<26,0,B>, ?) (<26,0,C>, ?)
(<26,1,A>, ?) (<26,1,B>, ?) (<26,1,C>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?)
(<28,1,A>, ?) (<28,1,B>, ?) (<28,1,C>, ?)
(<29,0,A>, A) (<29,0,B>, B) (<29,0,C>, C)
+ Applied Processor:
UnsatPaths
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))