WORST_CASE(?,O(1))
* Step 1: UnsatRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. copypol(A,B,C,D) -> n0(A,B,C,D) [A >= 0] (1,1)
1. m0(A,B,C,D) -> m1(B,A,E,C) [B >= 0 && C >= 1 && A >= 0] (?,1)
2. m2(A,B,C,D) -> m3(A,B,C,D) [A >= 1] (?,1)
3. m3(A,B,C,D) -> m5(A,B,C,D) [A >= 1] (?,1)
4. m6(A,B,C,D) -> m7(A,B,C,D) [A >= 1] (?,1)
5. m9(A,B,C,D) -> c2(m8(A,B,C,D),m2(A,B,C,D)) [A >= 1] (?,1)
6. m7(A,B,C,D) -> m9(A,B,C,D) [A >= 1] (?,1)
7. n3(A,B,C,D) -> n2(A,B,C,D) [A >= 0 && A >= 1 + C] (?,1)
8. n4(A,B,C,D) -> n2(A,B,C,D) [0 >= 1] (?,1)
9. m1(A,B,C,D) -> n3(A,B,C,D) [A >= 1 + C] (?,1)
10. m1(A,B,C,D) -> n5(B,A,D,C) [C >= A] (?,1)
11. n60(A,B,C,D) -> n1(A,B,C,D) True (?,1)
12. n61(A,B,C,D) -> m6(A,B,C,D) True (?,1)
13. n62(A,B,C,D) -> m0(C,0,B,D) True (?,1)
14. n6(A,B,C,D) -> c3(n60(E,F,A,D),n61(E,F,A,D),n62(E,F,A,D)) [F >= 1 && E >= 1 && A >= 0] (?,1)
15. n0(A,B,C,D) -> n6(A,B,C,D) [A >= 0] (?,1)
16. n7(A,B,C,D) -> m0(A,E,C,D) [B >= 0 && A >= 0 && C >= 1 && 1 + B >= E && E >= 1 + B] (?,1)
17. n5(A,B,C,D) -> n8(B,C,A,D) [B >= 0 && A >= 0 && C >= 1 && D >= B] (?,1)
18. n8(A,B,C,D) -> n4(A,B,C,D) [A >= 11] (?,1)
19. n8(A,B,C,D) -> n7(C,A,B,D) [10 >= A] (?,1)
20. m5(A,B,C,D) -> c2(m4(A,B,C,D),n9(A,B,C,D)) [A >= 1] (?,1)
Signature:
{(copypol,4)
;(m0,4)
;(m1,4)
;(m2,4)
;(m3,4)
;(m4,4)
;(m5,4)
;(m6,4)
;(m7,4)
;(m8,4)
;(m9,4)
;(n0,4)
;(n1,4)
;(n2,4)
;(n3,4)
;(n4,4)
;(n5,4)
;(n6,4)
;(n60,4)
;(n61,4)
;(n62,4)
;(n7,4)
;(n8,4)
;(n9,4)}
Flow Graph:
[0->{15},1->{9,10},2->{3},3->{20},4->{6},5->{2},6->{5},7->{},8->{},9->{7},10->{17},11->{},12->{4},13->{1}
,14->{11,12,13},15->{14},16->{1},17->{18,19},18->{8},19->{16},20->{}]
+ Applied Processor:
UnsatRules
+ Details:
The following transitions have unsatisfiable constraints and are removed: [8]
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. copypol(A,B,C,D) -> n0(A,B,C,D) [A >= 0] (1,1)
1. m0(A,B,C,D) -> m1(B,A,E,C) [B >= 0 && C >= 1 && A >= 0] (?,1)
2. m2(A,B,C,D) -> m3(A,B,C,D) [A >= 1] (?,1)
3. m3(A,B,C,D) -> m5(A,B,C,D) [A >= 1] (?,1)
4. m6(A,B,C,D) -> m7(A,B,C,D) [A >= 1] (?,1)
5. m9(A,B,C,D) -> c2(m8(A,B,C,D),m2(A,B,C,D)) [A >= 1] (?,1)
6. m7(A,B,C,D) -> m9(A,B,C,D) [A >= 1] (?,1)
7. n3(A,B,C,D) -> n2(A,B,C,D) [A >= 0 && A >= 1 + C] (?,1)
9. m1(A,B,C,D) -> n3(A,B,C,D) [A >= 1 + C] (?,1)
10. m1(A,B,C,D) -> n5(B,A,D,C) [C >= A] (?,1)
11. n60(A,B,C,D) -> n1(A,B,C,D) True (?,1)
12. n61(A,B,C,D) -> m6(A,B,C,D) True (?,1)
13. n62(A,B,C,D) -> m0(C,0,B,D) True (?,1)
14. n6(A,B,C,D) -> c3(n60(E,F,A,D),n61(E,F,A,D),n62(E,F,A,D)) [F >= 1 && E >= 1 && A >= 0] (?,1)
15. n0(A,B,C,D) -> n6(A,B,C,D) [A >= 0] (?,1)
16. n7(A,B,C,D) -> m0(A,E,C,D) [B >= 0 && A >= 0 && C >= 1 && 1 + B >= E && E >= 1 + B] (?,1)
17. n5(A,B,C,D) -> n8(B,C,A,D) [B >= 0 && A >= 0 && C >= 1 && D >= B] (?,1)
18. n8(A,B,C,D) -> n4(A,B,C,D) [A >= 11] (?,1)
19. n8(A,B,C,D) -> n7(C,A,B,D) [10 >= A] (?,1)
20. m5(A,B,C,D) -> c2(m4(A,B,C,D),n9(A,B,C,D)) [A >= 1] (?,1)
Signature:
{(copypol,4)
;(m0,4)
;(m1,4)
;(m2,4)
;(m3,4)
;(m4,4)
;(m5,4)
;(m6,4)
;(m7,4)
;(m8,4)
;(m9,4)
;(n0,4)
;(n1,4)
;(n2,4)
;(n3,4)
;(n4,4)
;(n5,4)
;(n6,4)
;(n60,4)
;(n61,4)
;(n62,4)
;(n7,4)
;(n8,4)
;(n9,4)}
Flow Graph:
[0->{15},1->{9,10},2->{3},3->{20},4->{6},5->{2},6->{5},7->{},9->{7},10->{17},11->{},12->{4},13->{1}
,14->{11,12,13},15->{14},16->{1},17->{18,19},18->{},19->{16},20->{}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,A>, A, .= 0) (< 0,0,B>, B, .= 0) (< 0,0,C>, C, .= 0) (< 0,0,D>, D, .= 0)
(< 1,0,A>, B, .= 0) (< 1,0,B>, A, .= 0) (< 1,0,C>, ?, .?) (< 1,0,D>, C, .= 0)
(< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0) (< 2,0,C>, C, .= 0) (< 2,0,D>, D, .= 0)
(< 3,0,A>, A, .= 0) (< 3,0,B>, B, .= 0) (< 3,0,C>, C, .= 0) (< 3,0,D>, D, .= 0)
(< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 4,0,C>, C, .= 0) (< 4,0,D>, D, .= 0)
(< 5,0,A>, A, .= 0) (< 5,0,B>, B, .= 0) (< 5,0,C>, C, .= 0) (< 5,0,D>, D, .= 0)
(< 5,1,A>, A, .= 0) (< 5,1,B>, B, .= 0) (< 5,1,C>, C, .= 0) (< 5,1,D>, D, .= 0)
(< 6,0,A>, A, .= 0) (< 6,0,B>, B, .= 0) (< 6,0,C>, C, .= 0) (< 6,0,D>, D, .= 0)
(< 7,0,A>, A, .= 0) (< 7,0,B>, B, .= 0) (< 7,0,C>, C, .= 0) (< 7,0,D>, D, .= 0)
(< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, C, .= 0) (< 9,0,D>, D, .= 0)
(<10,0,A>, B, .= 0) (<10,0,B>, A, .= 0) (<10,0,C>, D, .= 0) (<10,0,D>, C, .= 0)
(<11,0,A>, A, .= 0) (<11,0,B>, B, .= 0) (<11,0,C>, C, .= 0) (<11,0,D>, D, .= 0)
(<12,0,A>, A, .= 0) (<12,0,B>, B, .= 0) (<12,0,C>, C, .= 0) (<12,0,D>, D, .= 0)
(<13,0,A>, C, .= 0) (<13,0,B>, 0, .= 0) (<13,0,C>, B, .= 0) (<13,0,D>, D, .= 0)
(<14,0,A>, ?, .?) (<14,0,B>, ?, .?) (<14,0,C>, A, .= 0) (<14,0,D>, D, .= 0)
(<14,1,A>, ?, .?) (<14,1,B>, ?, .?) (<14,1,C>, A, .= 0) (<14,1,D>, D, .= 0)
(<14,2,A>, ?, .?) (<14,2,B>, ?, .?) (<14,2,C>, A, .= 0) (<14,2,D>, D, .= 0)
(<15,0,A>, A, .= 0) (<15,0,B>, B, .= 0) (<15,0,C>, C, .= 0) (<15,0,D>, D, .= 0)
(<16,0,A>, A, .= 0) (<16,0,B>, 1 + B, .+ 1) (<16,0,C>, C, .= 0) (<16,0,D>, D, .= 0)
(<17,0,A>, B, .= 0) (<17,0,B>, C, .= 0) (<17,0,C>, A, .= 0) (<17,0,D>, D, .= 0)
(<18,0,A>, A, .= 0) (<18,0,B>, B, .= 0) (<18,0,C>, C, .= 0) (<18,0,D>, D, .= 0)
(<19,0,A>, C, .= 0) (<19,0,B>, A, .= 0) (<19,0,C>, B, .= 0) (<19,0,D>, D, .= 0)
(<20,0,A>, A, .= 0) (<20,0,B>, B, .= 0) (<20,0,C>, C, .= 0) (<20,0,D>, D, .= 0)
(<20,1,A>, A, .= 0) (<20,1,B>, B, .= 0) (<20,1,C>, C, .= 0) (<20,1,D>, D, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. copypol(A,B,C,D) -> n0(A,B,C,D) [A >= 0] (1,1)
1. m0(A,B,C,D) -> m1(B,A,E,C) [B >= 0 && C >= 1 && A >= 0] (?,1)
2. m2(A,B,C,D) -> m3(A,B,C,D) [A >= 1] (?,1)
3. m3(A,B,C,D) -> m5(A,B,C,D) [A >= 1] (?,1)
4. m6(A,B,C,D) -> m7(A,B,C,D) [A >= 1] (?,1)
5. m9(A,B,C,D) -> c2(m8(A,B,C,D),m2(A,B,C,D)) [A >= 1] (?,1)
6. m7(A,B,C,D) -> m9(A,B,C,D) [A >= 1] (?,1)
7. n3(A,B,C,D) -> n2(A,B,C,D) [A >= 0 && A >= 1 + C] (?,1)
9. m1(A,B,C,D) -> n3(A,B,C,D) [A >= 1 + C] (?,1)
10. m1(A,B,C,D) -> n5(B,A,D,C) [C >= A] (?,1)
11. n60(A,B,C,D) -> n1(A,B,C,D) True (?,1)
12. n61(A,B,C,D) -> m6(A,B,C,D) True (?,1)
13. n62(A,B,C,D) -> m0(C,0,B,D) True (?,1)
14. n6(A,B,C,D) -> c3(n60(E,F,A,D),n61(E,F,A,D),n62(E,F,A,D)) [F >= 1 && E >= 1 && A >= 0] (?,1)
15. n0(A,B,C,D) -> n6(A,B,C,D) [A >= 0] (?,1)
16. n7(A,B,C,D) -> m0(A,E,C,D) [B >= 0 && A >= 0 && C >= 1 && 1 + B >= E && E >= 1 + B] (?,1)
17. n5(A,B,C,D) -> n8(B,C,A,D) [B >= 0 && A >= 0 && C >= 1 && D >= B] (?,1)
18. n8(A,B,C,D) -> n4(A,B,C,D) [A >= 11] (?,1)
19. n8(A,B,C,D) -> n7(C,A,B,D) [10 >= A] (?,1)
20. m5(A,B,C,D) -> c2(m4(A,B,C,D),n9(A,B,C,D)) [A >= 1] (?,1)
Signature:
{(copypol,4)
;(m0,4)
;(m1,4)
;(m2,4)
;(m3,4)
;(m4,4)
;(m5,4)
;(m6,4)
;(m7,4)
;(m8,4)
;(m9,4)
;(n0,4)
;(n1,4)
;(n2,4)
;(n3,4)
;(n4,4)
;(n5,4)
;(n6,4)
;(n60,4)
;(n61,4)
;(n62,4)
;(n7,4)
;(n8,4)
;(n9,4)}
Flow Graph:
[0->{15},1->{9,10},2->{3},3->{20},4->{6},5->{2},6->{5},7->{},9->{7},10->{17},11->{},12->{4},13->{1}
,14->{11,12,13},15->{14},16->{1},17->{18,19},18->{},19->{16},20->{}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?)
(< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?)
(< 5,1,A>, ?) (< 5,1,B>, ?) (< 5,1,C>, ?) (< 5,1,D>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<13,0,A>, ?) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?)
(<14,1,A>, ?) (<14,1,B>, ?) (<14,1,C>, ?) (<14,1,D>, ?)
(<14,2,A>, ?) (<14,2,B>, ?) (<14,2,C>, ?) (<14,2,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?)
(<17,0,A>, ?) (<17,0,B>, ?) (<17,0,C>, ?) (<17,0,D>, ?)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?)
(<20,1,A>, ?) (<20,1,B>, ?) (<20,1,C>, ?) (<20,1,D>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, 1) (< 1,0,B>, A) (< 1,0,C>, ?) (< 1,0,D>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, A) (< 2,0,D>, D)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, A) (< 3,0,D>, D)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, A) (< 4,0,D>, D)
(< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, A) (< 5,0,D>, D)
(< 5,1,A>, ?) (< 5,1,B>, ?) (< 5,1,C>, A) (< 5,1,D>, D)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, A) (< 6,0,D>, D)
(< 7,0,A>, 1) (< 7,0,B>, A) (< 7,0,C>, ?) (< 7,0,D>, ?)
(< 9,0,A>, 1) (< 9,0,B>, A) (< 9,0,C>, ?) (< 9,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 1) (<10,0,C>, ?) (<10,0,D>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, A) (<11,0,D>, D)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, A) (<12,0,D>, D)
(<13,0,A>, A) (<13,0,B>, 0) (<13,0,C>, ?) (<13,0,D>, D)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, A) (<14,0,D>, D)
(<14,1,A>, ?) (<14,1,B>, ?) (<14,1,C>, A) (<14,1,D>, D)
(<14,2,A>, ?) (<14,2,B>, ?) (<14,2,C>, A) (<14,2,D>, D)
(<15,0,A>, A) (<15,0,B>, B) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, A) (<16,0,B>, 1) (<16,0,C>, 1) (<16,0,D>, ?)
(<17,0,A>, 1) (<17,0,B>, 1) (<17,0,C>, A) (<17,0,D>, ?)
(<18,0,A>, 1) (<18,0,B>, 1) (<18,0,C>, A) (<18,0,D>, ?)
(<19,0,A>, A) (<19,0,B>, 1) (<19,0,C>, 1) (<19,0,D>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, A) (<20,0,D>, D)
(<20,1,A>, ?) (<20,1,B>, ?) (<20,1,C>, A) (<20,1,D>, D)
* Step 4: LeafRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. copypol(A,B,C,D) -> n0(A,B,C,D) [A >= 0] (1,1)
1. m0(A,B,C,D) -> m1(B,A,E,C) [B >= 0 && C >= 1 && A >= 0] (?,1)
2. m2(A,B,C,D) -> m3(A,B,C,D) [A >= 1] (?,1)
3. m3(A,B,C,D) -> m5(A,B,C,D) [A >= 1] (?,1)
4. m6(A,B,C,D) -> m7(A,B,C,D) [A >= 1] (?,1)
5. m9(A,B,C,D) -> c2(m8(A,B,C,D),m2(A,B,C,D)) [A >= 1] (?,1)
6. m7(A,B,C,D) -> m9(A,B,C,D) [A >= 1] (?,1)
7. n3(A,B,C,D) -> n2(A,B,C,D) [A >= 0 && A >= 1 + C] (?,1)
9. m1(A,B,C,D) -> n3(A,B,C,D) [A >= 1 + C] (?,1)
10. m1(A,B,C,D) -> n5(B,A,D,C) [C >= A] (?,1)
11. n60(A,B,C,D) -> n1(A,B,C,D) True (?,1)
12. n61(A,B,C,D) -> m6(A,B,C,D) True (?,1)
13. n62(A,B,C,D) -> m0(C,0,B,D) True (?,1)
14. n6(A,B,C,D) -> c3(n60(E,F,A,D),n61(E,F,A,D),n62(E,F,A,D)) [F >= 1 && E >= 1 && A >= 0] (?,1)
15. n0(A,B,C,D) -> n6(A,B,C,D) [A >= 0] (?,1)
16. n7(A,B,C,D) -> m0(A,E,C,D) [B >= 0 && A >= 0 && C >= 1 && 1 + B >= E && E >= 1 + B] (?,1)
17. n5(A,B,C,D) -> n8(B,C,A,D) [B >= 0 && A >= 0 && C >= 1 && D >= B] (?,1)
18. n8(A,B,C,D) -> n4(A,B,C,D) [A >= 11] (?,1)
19. n8(A,B,C,D) -> n7(C,A,B,D) [10 >= A] (?,1)
20. m5(A,B,C,D) -> c2(m4(A,B,C,D),n9(A,B,C,D)) [A >= 1] (?,1)
Signature:
{(copypol,4)
;(m0,4)
;(m1,4)
;(m2,4)
;(m3,4)
;(m4,4)
;(m5,4)
;(m6,4)
;(m7,4)
;(m8,4)
;(m9,4)
;(n0,4)
;(n1,4)
;(n2,4)
;(n3,4)
;(n4,4)
;(n5,4)
;(n6,4)
;(n60,4)
;(n61,4)
;(n62,4)
;(n7,4)
;(n8,4)
;(n9,4)}
Flow Graph:
[0->{15},1->{9,10},2->{3},3->{20},4->{6},5->{2},6->{5},7->{},9->{7},10->{17},11->{},12->{4},13->{1}
,14->{11,12,13},15->{14},16->{1},17->{18,19},18->{},19->{16},20->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, 1) (< 1,0,B>, A) (< 1,0,C>, ?) (< 1,0,D>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, A) (< 2,0,D>, D)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, A) (< 3,0,D>, D)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, A) (< 4,0,D>, D)
(< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, A) (< 5,0,D>, D)
(< 5,1,A>, ?) (< 5,1,B>, ?) (< 5,1,C>, A) (< 5,1,D>, D)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, A) (< 6,0,D>, D)
(< 7,0,A>, 1) (< 7,0,B>, A) (< 7,0,C>, ?) (< 7,0,D>, ?)
(< 9,0,A>, 1) (< 9,0,B>, A) (< 9,0,C>, ?) (< 9,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 1) (<10,0,C>, ?) (<10,0,D>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, A) (<11,0,D>, D)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, A) (<12,0,D>, D)
(<13,0,A>, A) (<13,0,B>, 0) (<13,0,C>, ?) (<13,0,D>, D)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, A) (<14,0,D>, D)
(<14,1,A>, ?) (<14,1,B>, ?) (<14,1,C>, A) (<14,1,D>, D)
(<14,2,A>, ?) (<14,2,B>, ?) (<14,2,C>, A) (<14,2,D>, D)
(<15,0,A>, A) (<15,0,B>, B) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, A) (<16,0,B>, 1) (<16,0,C>, 1) (<16,0,D>, ?)
(<17,0,A>, 1) (<17,0,B>, 1) (<17,0,C>, A) (<17,0,D>, ?)
(<18,0,A>, 1) (<18,0,B>, 1) (<18,0,C>, A) (<18,0,D>, ?)
(<19,0,A>, A) (<19,0,B>, 1) (<19,0,C>, 1) (<19,0,D>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, A) (<20,0,D>, D)
(<20,1,A>, ?) (<20,1,B>, ?) (<20,1,C>, A) (<20,1,D>, D)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [12,4,6,5,2,3,9,7,11,18,20]
* Step 5: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. copypol(A,B,C,D) -> n0(A,B,C,D) [A >= 0] (1,1)
1. m0(A,B,C,D) -> m1(B,A,E,C) [B >= 0 && C >= 1 && A >= 0] (?,1)
10. m1(A,B,C,D) -> n5(B,A,D,C) [C >= A] (?,1)
13. n62(A,B,C,D) -> m0(C,0,B,D) True (?,1)
14. n6(A,B,C,D) -> c3(n60(E,F,A,D),n61(E,F,A,D),n62(E,F,A,D)) [F >= 1 && E >= 1 && A >= 0] (?,1)
15. n0(A,B,C,D) -> n6(A,B,C,D) [A >= 0] (?,1)
16. n7(A,B,C,D) -> m0(A,E,C,D) [B >= 0 && A >= 0 && C >= 1 && 1 + B >= E && E >= 1 + B] (?,1)
17. n5(A,B,C,D) -> n8(B,C,A,D) [B >= 0 && A >= 0 && C >= 1 && D >= B] (?,1)
19. n8(A,B,C,D) -> n7(C,A,B,D) [10 >= A] (?,1)
Signature:
{(copypol,4)
;(m0,4)
;(m1,4)
;(m2,4)
;(m3,4)
;(m4,4)
;(m5,4)
;(m6,4)
;(m7,4)
;(m8,4)
;(m9,4)
;(n0,4)
;(n1,4)
;(n2,4)
;(n3,4)
;(n4,4)
;(n5,4)
;(n6,4)
;(n60,4)
;(n61,4)
;(n62,4)
;(n7,4)
;(n8,4)
;(n9,4)}
Flow Graph:
[0->{15},1->{10},10->{17},13->{1},14->{13},15->{14},16->{1},17->{19},19->{16}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, 1) (< 1,0,B>, A) (< 1,0,C>, ?) (< 1,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 1) (<10,0,C>, ?) (<10,0,D>, ?)
(<13,0,A>, A) (<13,0,B>, 0) (<13,0,C>, ?) (<13,0,D>, D)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, A) (<14,0,D>, D)
(<14,1,A>, ?) (<14,1,B>, ?) (<14,1,C>, A) (<14,1,D>, D)
(<14,2,A>, ?) (<14,2,B>, ?) (<14,2,C>, A) (<14,2,D>, D)
(<15,0,A>, A) (<15,0,B>, B) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, A) (<16,0,B>, 1) (<16,0,C>, 1) (<16,0,D>, ?)
(<17,0,A>, 1) (<17,0,B>, 1) (<17,0,C>, A) (<17,0,D>, ?)
(<19,0,A>, A) (<19,0,B>, 1) (<19,0,C>, 1) (<19,0,D>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(copypol) = 1
p(m0) = 0
p(m1) = 0
p(n0) = 1
p(n5) = 0
p(n6) = 0
p(n60) = 0
p(n61) = 0
p(n62) = 0
p(n7) = 0
p(n8) = 0
The following rules are strictly oriented:
[A >= 0] ==>
n0(A,B,C,D) = 1
> 0
= n6(A,B,C,D)
The following rules are weakly oriented:
[A >= 0] ==>
copypol(A,B,C,D) = 1
>= 1
= n0(A,B,C,D)
[B >= 0 && C >= 1 && A >= 0] ==>
m0(A,B,C,D) = 0
>= 0
= m1(B,A,E,C)
[C >= A] ==>
m1(A,B,C,D) = 0
>= 0
= n5(B,A,D,C)
True ==>
n62(A,B,C,D) = 0
>= 0
= m0(C,0,B,D)
[F >= 1 && E >= 1 && A >= 0] ==>
n6(A,B,C,D) = 0
>= 0
= c3(n60(E,F,A,D),n61(E,F,A,D),n62(E,F,A,D))
[B >= 0 && A >= 0 && C >= 1 && 1 + B >= E && E >= 1 + B] ==>
n7(A,B,C,D) = 0
>= 0
= m0(A,E,C,D)
[B >= 0 && A >= 0 && C >= 1 && D >= B] ==>
n5(A,B,C,D) = 0
>= 0
= n8(B,C,A,D)
[10 >= A] ==>
n8(A,B,C,D) = 0
>= 0
= n7(C,A,B,D)
* Step 6: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. copypol(A,B,C,D) -> n0(A,B,C,D) [A >= 0] (1,1)
1. m0(A,B,C,D) -> m1(B,A,E,C) [B >= 0 && C >= 1 && A >= 0] (?,1)
10. m1(A,B,C,D) -> n5(B,A,D,C) [C >= A] (?,1)
13. n62(A,B,C,D) -> m0(C,0,B,D) True (?,1)
14. n6(A,B,C,D) -> c3(n60(E,F,A,D),n61(E,F,A,D),n62(E,F,A,D)) [F >= 1 && E >= 1 && A >= 0] (?,1)
15. n0(A,B,C,D) -> n6(A,B,C,D) [A >= 0] (1,1)
16. n7(A,B,C,D) -> m0(A,E,C,D) [B >= 0 && A >= 0 && C >= 1 && 1 + B >= E && E >= 1 + B] (?,1)
17. n5(A,B,C,D) -> n8(B,C,A,D) [B >= 0 && A >= 0 && C >= 1 && D >= B] (?,1)
19. n8(A,B,C,D) -> n7(C,A,B,D) [10 >= A] (?,1)
Signature:
{(copypol,4)
;(m0,4)
;(m1,4)
;(m2,4)
;(m3,4)
;(m4,4)
;(m5,4)
;(m6,4)
;(m7,4)
;(m8,4)
;(m9,4)
;(n0,4)
;(n1,4)
;(n2,4)
;(n3,4)
;(n4,4)
;(n5,4)
;(n6,4)
;(n60,4)
;(n61,4)
;(n62,4)
;(n7,4)
;(n8,4)
;(n9,4)}
Flow Graph:
[0->{15},1->{10},10->{17},13->{1},14->{13},15->{14},16->{1},17->{19},19->{16}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, 1) (< 1,0,B>, A) (< 1,0,C>, ?) (< 1,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 1) (<10,0,C>, ?) (<10,0,D>, ?)
(<13,0,A>, A) (<13,0,B>, 0) (<13,0,C>, ?) (<13,0,D>, D)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, A) (<14,0,D>, D)
(<14,1,A>, ?) (<14,1,B>, ?) (<14,1,C>, A) (<14,1,D>, D)
(<14,2,A>, ?) (<14,2,B>, ?) (<14,2,C>, A) (<14,2,D>, D)
(<15,0,A>, A) (<15,0,B>, B) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, A) (<16,0,B>, 1) (<16,0,C>, 1) (<16,0,D>, ?)
(<17,0,A>, 1) (<17,0,B>, 1) (<17,0,C>, A) (<17,0,D>, ?)
(<19,0,A>, A) (<19,0,B>, 1) (<19,0,C>, 1) (<19,0,D>, ?)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 7: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. copypol(A,B,C,D) -> n0(A,B,C,D) [A >= 0] (1,1)
1. m0(A,B,C,D) -> m1(B,A,E,C) [B >= 0 && C >= 1 && A >= 0] (?,1)
10. m1(A,B,C,D) -> n5(B,A,D,C) [C >= A] (?,1)
13. n62(A,B,C,D) -> m0(C,0,B,D) True (1,1)
14. n6(A,B,C,D) -> c3(n60(E,F,A,D),n61(E,F,A,D),n62(E,F,A,D)) [F >= 1 && E >= 1 && A >= 0] (1,1)
15. n0(A,B,C,D) -> n6(A,B,C,D) [A >= 0] (1,1)
16. n7(A,B,C,D) -> m0(A,E,C,D) [B >= 0 && A >= 0 && C >= 1 && 1 + B >= E && E >= 1 + B] (?,1)
17. n5(A,B,C,D) -> n8(B,C,A,D) [B >= 0 && A >= 0 && C >= 1 && D >= B] (?,1)
19. n8(A,B,C,D) -> n7(C,A,B,D) [10 >= A] (?,1)
Signature:
{(copypol,4)
;(m0,4)
;(m1,4)
;(m2,4)
;(m3,4)
;(m4,4)
;(m5,4)
;(m6,4)
;(m7,4)
;(m8,4)
;(m9,4)
;(n0,4)
;(n1,4)
;(n2,4)
;(n3,4)
;(n4,4)
;(n5,4)
;(n6,4)
;(n60,4)
;(n61,4)
;(n62,4)
;(n7,4)
;(n8,4)
;(n9,4)}
Flow Graph:
[0->{15},1->{10},10->{17},13->{1},14->{13},15->{14},16->{1},17->{19},19->{16}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, 1) (< 1,0,B>, A) (< 1,0,C>, ?) (< 1,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 1) (<10,0,C>, ?) (<10,0,D>, ?)
(<13,0,A>, A) (<13,0,B>, 0) (<13,0,C>, ?) (<13,0,D>, D)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, A) (<14,0,D>, D)
(<14,1,A>, ?) (<14,1,B>, ?) (<14,1,C>, A) (<14,1,D>, D)
(<14,2,A>, ?) (<14,2,B>, ?) (<14,2,C>, A) (<14,2,D>, D)
(<15,0,A>, A) (<15,0,B>, B) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, A) (<16,0,B>, 1) (<16,0,C>, 1) (<16,0,D>, ?)
(<17,0,A>, 1) (<17,0,B>, 1) (<17,0,C>, A) (<17,0,D>, ?)
(<19,0,A>, A) (<19,0,B>, 1) (<19,0,C>, 1) (<19,0,D>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [1,16,19,17,10], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(m0) = 11 + -1*x2
p(m1) = 11 + -1*x1
p(n5) = 11 + -1*x2
p(n7) = 10 + -1*x2
p(n8) = 11 + -1*x1
The following rules are strictly oriented:
[10 >= A] ==>
n8(A,B,C,D) = 11 + -1*A
> 10 + -1*A
= n7(C,A,B,D)
The following rules are weakly oriented:
[B >= 0 && C >= 1 && A >= 0] ==>
m0(A,B,C,D) = 11 + -1*B
>= 11 + -1*B
= m1(B,A,E,C)
[C >= A] ==>
m1(A,B,C,D) = 11 + -1*A
>= 11 + -1*A
= n5(B,A,D,C)
[B >= 0 && A >= 0 && C >= 1 && 1 + B >= E && E >= 1 + B] ==>
n7(A,B,C,D) = 10 + -1*B
>= 11 + -1*E
= m0(A,E,C,D)
[B >= 0 && A >= 0 && C >= 1 && D >= B] ==>
n5(A,B,C,D) = 11 + -1*B
>= 11 + -1*B
= n8(B,C,A,D)
We use the following global sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, 1) (< 1,0,B>, A) (< 1,0,C>, ?) (< 1,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 1) (<10,0,C>, ?) (<10,0,D>, ?)
(<13,0,A>, A) (<13,0,B>, 0) (<13,0,C>, ?) (<13,0,D>, D)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, A) (<14,0,D>, D)
(<14,1,A>, ?) (<14,1,B>, ?) (<14,1,C>, A) (<14,1,D>, D)
(<14,2,A>, ?) (<14,2,B>, ?) (<14,2,C>, A) (<14,2,D>, D)
(<15,0,A>, A) (<15,0,B>, B) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, A) (<16,0,B>, 1) (<16,0,C>, 1) (<16,0,D>, ?)
(<17,0,A>, 1) (<17,0,B>, 1) (<17,0,C>, A) (<17,0,D>, ?)
(<19,0,A>, A) (<19,0,B>, 1) (<19,0,C>, 1) (<19,0,D>, ?)
* Step 8: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. copypol(A,B,C,D) -> n0(A,B,C,D) [A >= 0] (1,1)
1. m0(A,B,C,D) -> m1(B,A,E,C) [B >= 0 && C >= 1 && A >= 0] (?,1)
10. m1(A,B,C,D) -> n5(B,A,D,C) [C >= A] (?,1)
13. n62(A,B,C,D) -> m0(C,0,B,D) True (1,1)
14. n6(A,B,C,D) -> c3(n60(E,F,A,D),n61(E,F,A,D),n62(E,F,A,D)) [F >= 1 && E >= 1 && A >= 0] (1,1)
15. n0(A,B,C,D) -> n6(A,B,C,D) [A >= 0] (1,1)
16. n7(A,B,C,D) -> m0(A,E,C,D) [B >= 0 && A >= 0 && C >= 1 && 1 + B >= E && E >= 1 + B] (?,1)
17. n5(A,B,C,D) -> n8(B,C,A,D) [B >= 0 && A >= 0 && C >= 1 && D >= B] (?,1)
19. n8(A,B,C,D) -> n7(C,A,B,D) [10 >= A] (11,1)
Signature:
{(copypol,4)
;(m0,4)
;(m1,4)
;(m2,4)
;(m3,4)
;(m4,4)
;(m5,4)
;(m6,4)
;(m7,4)
;(m8,4)
;(m9,4)
;(n0,4)
;(n1,4)
;(n2,4)
;(n3,4)
;(n4,4)
;(n5,4)
;(n6,4)
;(n60,4)
;(n61,4)
;(n62,4)
;(n7,4)
;(n8,4)
;(n9,4)}
Flow Graph:
[0->{15},1->{10},10->{17},13->{1},14->{13},15->{14},16->{1},17->{19},19->{16}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, 1) (< 1,0,B>, A) (< 1,0,C>, ?) (< 1,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 1) (<10,0,C>, ?) (<10,0,D>, ?)
(<13,0,A>, A) (<13,0,B>, 0) (<13,0,C>, ?) (<13,0,D>, D)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, A) (<14,0,D>, D)
(<14,1,A>, ?) (<14,1,B>, ?) (<14,1,C>, A) (<14,1,D>, D)
(<14,2,A>, ?) (<14,2,B>, ?) (<14,2,C>, A) (<14,2,D>, D)
(<15,0,A>, A) (<15,0,B>, B) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, A) (<16,0,B>, 1) (<16,0,C>, 1) (<16,0,D>, ?)
(<17,0,A>, 1) (<17,0,B>, 1) (<17,0,C>, A) (<17,0,D>, ?)
(<19,0,A>, A) (<19,0,B>, 1) (<19,0,C>, 1) (<19,0,D>, ?)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 9: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. copypol(A,B,C,D) -> n0(A,B,C,D) [A >= 0] (1,1)
1. m0(A,B,C,D) -> m1(B,A,E,C) [B >= 0 && C >= 1 && A >= 0] (?,1)
10. m1(A,B,C,D) -> n5(B,A,D,C) [C >= A] (?,1)
13. n62(A,B,C,D) -> m0(C,0,B,D) True (1,1)
14. n6(A,B,C,D) -> c3(n60(E,F,A,D),n61(E,F,A,D),n62(E,F,A,D)) [F >= 1 && E >= 1 && A >= 0] (1,1)
15. n0(A,B,C,D) -> n6(A,B,C,D) [A >= 0] (1,1)
16. n7(A,B,C,D) -> m0(A,E,C,D) [B >= 0 && A >= 0 && C >= 1 && 1 + B >= E && E >= 1 + B] (11,1)
17. n5(A,B,C,D) -> n8(B,C,A,D) [B >= 0 && A >= 0 && C >= 1 && D >= B] (?,1)
19. n8(A,B,C,D) -> n7(C,A,B,D) [10 >= A] (11,1)
Signature:
{(copypol,4)
;(m0,4)
;(m1,4)
;(m2,4)
;(m3,4)
;(m4,4)
;(m5,4)
;(m6,4)
;(m7,4)
;(m8,4)
;(m9,4)
;(n0,4)
;(n1,4)
;(n2,4)
;(n3,4)
;(n4,4)
;(n5,4)
;(n6,4)
;(n60,4)
;(n61,4)
;(n62,4)
;(n7,4)
;(n8,4)
;(n9,4)}
Flow Graph:
[0->{15},1->{10},10->{17},13->{1},14->{13},15->{14},16->{1},17->{19},19->{16}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, 1) (< 1,0,B>, A) (< 1,0,C>, ?) (< 1,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 1) (<10,0,C>, ?) (<10,0,D>, ?)
(<13,0,A>, A) (<13,0,B>, 0) (<13,0,C>, ?) (<13,0,D>, D)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, A) (<14,0,D>, D)
(<14,1,A>, ?) (<14,1,B>, ?) (<14,1,C>, A) (<14,1,D>, D)
(<14,2,A>, ?) (<14,2,B>, ?) (<14,2,C>, A) (<14,2,D>, D)
(<15,0,A>, A) (<15,0,B>, B) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, A) (<16,0,B>, 1) (<16,0,C>, 1) (<16,0,D>, ?)
(<17,0,A>, 1) (<17,0,B>, 1) (<17,0,C>, A) (<17,0,D>, ?)
(<19,0,A>, A) (<19,0,B>, 1) (<19,0,C>, 1) (<19,0,D>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [1,19,17,10], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(m0) = 1
p(m1) = 1
p(n5) = 1
p(n7) = 0
p(n8) = 0
The following rules are strictly oriented:
[B >= 0 && A >= 0 && C >= 1 && D >= B] ==>
n5(A,B,C,D) = 1
> 0
= n8(B,C,A,D)
The following rules are weakly oriented:
[B >= 0 && C >= 1 && A >= 0] ==>
m0(A,B,C,D) = 1
>= 1
= m1(B,A,E,C)
[C >= A] ==>
m1(A,B,C,D) = 1
>= 1
= n5(B,A,D,C)
[10 >= A] ==>
n8(A,B,C,D) = 0
>= 0
= n7(C,A,B,D)
We use the following global sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, 1) (< 1,0,B>, A) (< 1,0,C>, ?) (< 1,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 1) (<10,0,C>, ?) (<10,0,D>, ?)
(<13,0,A>, A) (<13,0,B>, 0) (<13,0,C>, ?) (<13,0,D>, D)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, A) (<14,0,D>, D)
(<14,1,A>, ?) (<14,1,B>, ?) (<14,1,C>, A) (<14,1,D>, D)
(<14,2,A>, ?) (<14,2,B>, ?) (<14,2,C>, A) (<14,2,D>, D)
(<15,0,A>, A) (<15,0,B>, B) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, A) (<16,0,B>, 1) (<16,0,C>, 1) (<16,0,D>, ?)
(<17,0,A>, 1) (<17,0,B>, 1) (<17,0,C>, A) (<17,0,D>, ?)
(<19,0,A>, A) (<19,0,B>, 1) (<19,0,C>, 1) (<19,0,D>, ?)
* Step 10: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. copypol(A,B,C,D) -> n0(A,B,C,D) [A >= 0] (1,1)
1. m0(A,B,C,D) -> m1(B,A,E,C) [B >= 0 && C >= 1 && A >= 0] (?,1)
10. m1(A,B,C,D) -> n5(B,A,D,C) [C >= A] (?,1)
13. n62(A,B,C,D) -> m0(C,0,B,D) True (1,1)
14. n6(A,B,C,D) -> c3(n60(E,F,A,D),n61(E,F,A,D),n62(E,F,A,D)) [F >= 1 && E >= 1 && A >= 0] (1,1)
15. n0(A,B,C,D) -> n6(A,B,C,D) [A >= 0] (1,1)
16. n7(A,B,C,D) -> m0(A,E,C,D) [B >= 0 && A >= 0 && C >= 1 && 1 + B >= E && E >= 1 + B] (11,1)
17. n5(A,B,C,D) -> n8(B,C,A,D) [B >= 0 && A >= 0 && C >= 1 && D >= B] (12,1)
19. n8(A,B,C,D) -> n7(C,A,B,D) [10 >= A] (11,1)
Signature:
{(copypol,4)
;(m0,4)
;(m1,4)
;(m2,4)
;(m3,4)
;(m4,4)
;(m5,4)
;(m6,4)
;(m7,4)
;(m8,4)
;(m9,4)
;(n0,4)
;(n1,4)
;(n2,4)
;(n3,4)
;(n4,4)
;(n5,4)
;(n6,4)
;(n60,4)
;(n61,4)
;(n62,4)
;(n7,4)
;(n8,4)
;(n9,4)}
Flow Graph:
[0->{15},1->{10},10->{17},13->{1},14->{13},15->{14},16->{1},17->{19},19->{16}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, 1) (< 1,0,B>, A) (< 1,0,C>, ?) (< 1,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 1) (<10,0,C>, ?) (<10,0,D>, ?)
(<13,0,A>, A) (<13,0,B>, 0) (<13,0,C>, ?) (<13,0,D>, D)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, A) (<14,0,D>, D)
(<14,1,A>, ?) (<14,1,B>, ?) (<14,1,C>, A) (<14,1,D>, D)
(<14,2,A>, ?) (<14,2,B>, ?) (<14,2,C>, A) (<14,2,D>, D)
(<15,0,A>, A) (<15,0,B>, B) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, A) (<16,0,B>, 1) (<16,0,C>, 1) (<16,0,D>, ?)
(<17,0,A>, 1) (<17,0,B>, 1) (<17,0,C>, A) (<17,0,D>, ?)
(<19,0,A>, A) (<19,0,B>, 1) (<19,0,C>, 1) (<19,0,D>, ?)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 11: LocalSizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. copypol(A,B,C,D) -> n0(A,B,C,D) [A >= 0] (1,1)
1. m0(A,B,C,D) -> m1(B,A,E,C) [B >= 0 && C >= 1 && A >= 0] (12,1)
10. m1(A,B,C,D) -> n5(B,A,D,C) [C >= A] (12,1)
13. n62(A,B,C,D) -> m0(C,0,B,D) True (1,1)
14. n6(A,B,C,D) -> c3(n60(E,F,A,D),n61(E,F,A,D),n62(E,F,A,D)) [F >= 1 && E >= 1 && A >= 0] (1,1)
15. n0(A,B,C,D) -> n6(A,B,C,D) [A >= 0] (1,1)
16. n7(A,B,C,D) -> m0(A,E,C,D) [B >= 0 && A >= 0 && C >= 1 && 1 + B >= E && E >= 1 + B] (11,1)
17. n5(A,B,C,D) -> n8(B,C,A,D) [B >= 0 && A >= 0 && C >= 1 && D >= B] (12,1)
19. n8(A,B,C,D) -> n7(C,A,B,D) [10 >= A] (11,1)
Signature:
{(copypol,4)
;(m0,4)
;(m1,4)
;(m2,4)
;(m3,4)
;(m4,4)
;(m5,4)
;(m6,4)
;(m7,4)
;(m8,4)
;(m9,4)
;(n0,4)
;(n1,4)
;(n2,4)
;(n3,4)
;(n4,4)
;(n5,4)
;(n6,4)
;(n60,4)
;(n61,4)
;(n62,4)
;(n7,4)
;(n8,4)
;(n9,4)}
Flow Graph:
[0->{15},1->{10},10->{17},13->{1},14->{13},15->{14},16->{1},17->{19},19->{16}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D)
(< 1,0,A>, 1) (< 1,0,B>, A) (< 1,0,C>, ?) (< 1,0,D>, ?)
(<10,0,A>, A) (<10,0,B>, 1) (<10,0,C>, ?) (<10,0,D>, ?)
(<13,0,A>, A) (<13,0,B>, 0) (<13,0,C>, ?) (<13,0,D>, D)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, A) (<14,0,D>, D)
(<14,1,A>, ?) (<14,1,B>, ?) (<14,1,C>, A) (<14,1,D>, D)
(<14,2,A>, ?) (<14,2,B>, ?) (<14,2,C>, A) (<14,2,D>, D)
(<15,0,A>, A) (<15,0,B>, B) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, A) (<16,0,B>, 1) (<16,0,C>, 1) (<16,0,D>, ?)
(<17,0,A>, 1) (<17,0,B>, 1) (<17,0,C>, A) (<17,0,D>, ?)
(<19,0,A>, A) (<19,0,B>, 1) (<19,0,C>, 1) (<19,0,D>, ?)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
The problem is already solved.
WORST_CASE(?,O(1))