WORST_CASE(?,O(n^1))
* Step 1: RestrictVarsProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. add(A,B,C,D) -> n4(A,B,C,D) [A >= 0] (1,1)
1. m0(A,B,C,D) -> m1(A,B,C,D) True (?,1)
2. m2(A,B,C,D) -> m3(A,B,C,D) True (?,1)
3. m5(A,B,C,D) -> m4(E,B,C,D) [1 + A >= E && E >= 1 + A] (?,1)
4. m3(A,B,C,D) -> m5(A,B,C,D) True (?,1)
5. m6(A,B,C,D) -> m7(A,B,C,D) True (?,1)
6. m9(A,B,C,D) -> m8(E,B,C,D) [2 + A >= E && E >= 2 + A] (?,1)
7. m7(A,B,C,D) -> m9(A,B,C,D) True (?,1)
8. n0(A,B,C,D) -> n1(A,B,C,D) True (?,1)
9. n3(A,B,C,D) -> n2(E,B,C,D) [3 + A >= E && E >= 3 + A] (?,1)
10. n1(A,B,C,D) -> n3(A,B,C,D) True (?,1)
11. n7(A,B,C,D) -> m0(A,B,C,D) [3 + A >= B] (?,1)
12. n80(A,B,C,D) -> n7(A,B,C,D) True (?,1)
13. n81(A,B,C,D) -> m2(C,B,C,D) True (?,1)
14. n8(A,B,C,D) -> c2(n80(A,E,B,D),n81(A,E,B,D)) [A >= B && 1 + B >= E && E >= 1 + B] (?,1)
15. n90(A,B,C,D) -> n7(A,B,C,D) True (?,1)
16. n91(A,B,C,D) -> m6(C,B,C,D) True (?,1)
17. n9(A,B,C,D) -> c2(n90(A,E,B,D),n91(A,E,B,D)) [A >= B && 2 + B >= E && E >= 2 + B] (?,1)
18. o00(A,B,C,D) -> n7(A,B,C,D) True (?,1)
19. o01(A,B,C,D) -> n0(C,B,C,D) True (?,1)
20. o0(A,B,C,D) -> c2(o00(A,E,B,D),o01(A,E,B,D)) [A >= B && 3 + B >= E && E >= 3 + B] (?,1)
21. o1(A,B,C,D) -> c2(n5(A,0,C,D),m0(A,0,C,D)) [A >= 0] (?,1)
22. n4(A,B,C,D) -> o1(A,B,C,D) [A >= 0] (?,1)
23. o2(A,B,C,D) -> o3(A,B,C,D) [A >= B] (?,1)
24. o3(A,B,C,D) -> n8(A,B,C,D) True (?,1)
25. o3(A,B,C,D) -> n9(A,B,C,D) True (?,1)
26. o3(A,B,C,D) -> o0(A,B,C,D) True (?,1)
27. m1(A,B,C,D) -> o2(A,B,C,D) True (?,1)
28. m1(A,B,C,D) -> n6(A,B,C,B) True (?,1)
Signature:
{(add,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)
;(n7,4)
;(n8,4)
;(n80,4)
;(n81,4)
;(n9,4)
;(n90,4)
;(n91,4)
;(o0,4)
;(o00,4)
;(o01,4)
;(o1,4)
;(o2,4)
;(o3,4)}
Flow Graph:
[0->{22},1->{27,28},2->{4},3->{},4->{3},5->{7},6->{},7->{6},8->{10},9->{},10->{9},11->{1},12->{11},13->{2}
,14->{12,13},15->{11},16->{5},17->{15,16},18->{11},19->{8},20->{18,19},21->{1},22->{21},23->{24,25,26}
,24->{14},25->{17},26->{20},27->{23},28->{}]
+ Applied Processor:
RestrictVarsProcessor
+ Details:
We removed the arguments [D] .
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. add(A,B,C) -> n4(A,B,C) [A >= 0] (1,1)
1. m0(A,B,C) -> m1(A,B,C) True (?,1)
2. m2(A,B,C) -> m3(A,B,C) True (?,1)
3. m5(A,B,C) -> m4(E,B,C) [1 + A >= E && E >= 1 + A] (?,1)
4. m3(A,B,C) -> m5(A,B,C) True (?,1)
5. m6(A,B,C) -> m7(A,B,C) True (?,1)
6. m9(A,B,C) -> m8(E,B,C) [2 + A >= E && E >= 2 + A] (?,1)
7. m7(A,B,C) -> m9(A,B,C) True (?,1)
8. n0(A,B,C) -> n1(A,B,C) True (?,1)
9. n3(A,B,C) -> n2(E,B,C) [3 + A >= E && E >= 3 + A] (?,1)
10. n1(A,B,C) -> n3(A,B,C) True (?,1)
11. n7(A,B,C) -> m0(A,B,C) [3 + A >= B] (?,1)
12. n80(A,B,C) -> n7(A,B,C) True (?,1)
13. n81(A,B,C) -> m2(C,B,C) True (?,1)
14. n8(A,B,C) -> c2(n80(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B] (?,1)
15. n90(A,B,C) -> n7(A,B,C) True (?,1)
16. n91(A,B,C) -> m6(C,B,C) True (?,1)
17. n9(A,B,C) -> c2(n90(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B] (?,1)
18. o00(A,B,C) -> n7(A,B,C) True (?,1)
19. o01(A,B,C) -> n0(C,B,C) True (?,1)
20. o0(A,B,C) -> c2(o00(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B] (?,1)
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (?,1)
22. n4(A,B,C) -> o1(A,B,C) [A >= 0] (?,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
27. m1(A,B,C) -> o2(A,B,C) True (?,1)
28. m1(A,B,C) -> n6(A,B,C) True (?,1)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[0->{22},1->{27,28},2->{4},3->{},4->{3},5->{7},6->{},7->{6},8->{10},9->{},10->{9},11->{1},12->{11},13->{2}
,14->{12,13},15->{11},16->{5},17->{15,16},18->{11},19->{8},20->{18,19},21->{1},22->{21},23->{24,25,26}
,24->{14},25->{17},26->{20},27->{23},28->{}]
+ 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>, 1 + A, .+ 1) (< 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>, 2 + A, .+ 2) (< 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)
(< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0) (< 8,0,C>, C, .= 0)
(< 9,0,A>, 3 + A, .+ 3) (< 9,0,B>, B, .= 0) (< 9,0,C>, C, .= 0)
(<10,0,A>, A, .= 0) (<10,0,B>, B, .= 0) (<10,0,C>, C, .= 0)
(<11,0,A>, A, .= 0) (<11,0,B>, B, .= 0) (<11,0,C>, C, .= 0)
(<12,0,A>, A, .= 0) (<12,0,B>, B, .= 0) (<12,0,C>, C, .= 0)
(<13,0,A>, C, .= 0) (<13,0,B>, B, .= 0) (<13,0,C>, C, .= 0)
(<14,0,A>, A, .= 0) (<14,0,B>, 1 + A + B, .* 1) (<14,0,C>, B, .= 0)
(<14,1,A>, A, .= 0) (<14,1,B>, 1 + A + B, .* 1) (<14,1,C>, B, .= 0)
(<15,0,A>, A, .= 0) (<15,0,B>, B, .= 0) (<15,0,C>, C, .= 0)
(<16,0,A>, C, .= 0) (<16,0,B>, B, .= 0) (<16,0,C>, C, .= 0)
(<17,0,A>, A, .= 0) (<17,0,B>, 2 + A + B, .* 2) (<17,0,C>, B, .= 0)
(<17,1,A>, A, .= 0) (<17,1,B>, 2 + A + B, .* 2) (<17,1,C>, B, .= 0)
(<18,0,A>, A, .= 0) (<18,0,B>, B, .= 0) (<18,0,C>, C, .= 0)
(<19,0,A>, C, .= 0) (<19,0,B>, B, .= 0) (<19,0,C>, C, .= 0)
(<20,0,A>, A, .= 0) (<20,0,B>, 3 + A + B, .* 3) (<20,0,C>, B, .= 0)
(<20,1,A>, A, .= 0) (<20,1,B>, 3 + A + B, .* 3) (<20,1,C>, B, .= 0)
(<21,0,A>, A, .= 0) (<21,0,B>, 0, .= 0) (<21,0,C>, C, .= 0)
(<21,1,A>, A, .= 0) (<21,1,B>, 0, .= 0) (<21,1,C>, C, .= 0)
(<22,0,A>, A, .= 0) (<22,0,B>, B, .= 0) (<22,0,C>, C, .= 0)
(<23,0,A>, A, .= 0) (<23,0,B>, B, .= 0) (<23,0,C>, C, .= 0)
(<24,0,A>, A, .= 0) (<24,0,B>, B, .= 0) (<24,0,C>, C, .= 0)
(<25,0,A>, A, .= 0) (<25,0,B>, B, .= 0) (<25,0,C>, C, .= 0)
(<26,0,A>, A, .= 0) (<26,0,B>, B, .= 0) (<26,0,C>, C, .= 0)
(<27,0,A>, A, .= 0) (<27,0,B>, B, .= 0) (<27,0,C>, C, .= 0)
(<28,0,A>, A, .= 0) (<28,0,B>, B, .= 0) (<28,0,C>, C, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. add(A,B,C) -> n4(A,B,C) [A >= 0] (1,1)
1. m0(A,B,C) -> m1(A,B,C) True (?,1)
2. m2(A,B,C) -> m3(A,B,C) True (?,1)
3. m5(A,B,C) -> m4(E,B,C) [1 + A >= E && E >= 1 + A] (?,1)
4. m3(A,B,C) -> m5(A,B,C) True (?,1)
5. m6(A,B,C) -> m7(A,B,C) True (?,1)
6. m9(A,B,C) -> m8(E,B,C) [2 + A >= E && E >= 2 + A] (?,1)
7. m7(A,B,C) -> m9(A,B,C) True (?,1)
8. n0(A,B,C) -> n1(A,B,C) True (?,1)
9. n3(A,B,C) -> n2(E,B,C) [3 + A >= E && E >= 3 + A] (?,1)
10. n1(A,B,C) -> n3(A,B,C) True (?,1)
11. n7(A,B,C) -> m0(A,B,C) [3 + A >= B] (?,1)
12. n80(A,B,C) -> n7(A,B,C) True (?,1)
13. n81(A,B,C) -> m2(C,B,C) True (?,1)
14. n8(A,B,C) -> c2(n80(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B] (?,1)
15. n90(A,B,C) -> n7(A,B,C) True (?,1)
16. n91(A,B,C) -> m6(C,B,C) True (?,1)
17. n9(A,B,C) -> c2(n90(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B] (?,1)
18. o00(A,B,C) -> n7(A,B,C) True (?,1)
19. o01(A,B,C) -> n0(C,B,C) True (?,1)
20. o0(A,B,C) -> c2(o00(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B] (?,1)
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (?,1)
22. n4(A,B,C) -> o1(A,B,C) [A >= 0] (?,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
27. m1(A,B,C) -> o2(A,B,C) True (?,1)
28. m1(A,B,C) -> n6(A,B,C) True (?,1)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[0->{22},1->{27,28},2->{4},3->{},4->{3},5->{7},6->{},7->{6},8->{10},9->{},10->{9},11->{1},12->{11},13->{2}
,14->{12,13},15->{11},16->{5},17->{15,16},18->{11},19->{8},20->{18,19},21->{1},22->{21},23->{24,25,26}
,24->{14},25->{17},26->{20},27->{23},28->{}]
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>, ?)
(< 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>, ?)
(<13,0,A>, ?) (<13,0,B>, ?) (<13,0,C>, ?)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?)
(<14,1,A>, ?) (<14,1,B>, ?) (<14,1,C>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?)
(<17,0,A>, ?) (<17,0,B>, ?) (<17,0,C>, ?)
(<17,1,A>, ?) (<17,1,B>, ?) (<17,1,C>, ?)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?)
(<20,1,A>, ?) (<20,1,B>, ?) (<20,1,C>, ?)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,C>, ?)
(<21,1,A>, ?) (<21,1,B>, ?) (<21,1,C>, ?)
(<22,0,A>, ?) (<22,0,B>, ?) (<22,0,C>, ?)
(<23,0,A>, ?) (<23,0,B>, ?) (<23,0,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>, ?)
(<27,0,A>, ?) (<27,0,B>, ?) (<27,0,C>, ?)
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C)
(< 1,0,A>, A) (< 1,0,B>, 3 + A) (< 1,0,C>, A + C)
(< 2,0,A>, A) (< 2,0,B>, A) (< 2,0,C>, A)
(< 3,0,A>, 1 + A) (< 3,0,B>, A) (< 3,0,C>, A)
(< 4,0,A>, A) (< 4,0,B>, A) (< 4,0,C>, A)
(< 5,0,A>, A) (< 5,0,B>, A) (< 5,0,C>, A)
(< 6,0,A>, 2 + A) (< 6,0,B>, A) (< 6,0,C>, A)
(< 7,0,A>, A) (< 7,0,B>, A) (< 7,0,C>, A)
(< 8,0,A>, A) (< 8,0,B>, A) (< 8,0,C>, A)
(< 9,0,A>, 3 + A) (< 9,0,B>, A) (< 9,0,C>, A)
(<10,0,A>, A) (<10,0,B>, A) (<10,0,C>, A)
(<11,0,A>, A) (<11,0,B>, 3 + A) (<11,0,C>, A)
(<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, A)
(<13,0,A>, A) (<13,0,B>, A) (<13,0,C>, A)
(<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, A)
(<14,1,A>, A) (<14,1,B>, A) (<14,1,C>, A)
(<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, A)
(<16,0,A>, A) (<16,0,B>, A) (<16,0,C>, A)
(<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, A)
(<17,1,A>, A) (<17,1,B>, A) (<17,1,C>, A)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, A)
(<19,0,A>, A) (<19,0,B>, A) (<19,0,C>, A)
(<20,0,A>, A) (<20,0,B>, A) (<20,0,C>, A)
(<20,1,A>, A) (<20,1,B>, A) (<20,1,C>, A)
(<21,0,A>, A) (<21,0,B>, 0) (<21,0,C>, C)
(<21,1,A>, A) (<21,1,B>, 0) (<21,1,C>, C)
(<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, C)
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<27,0,A>, A) (<27,0,B>, 3 + A) (<27,0,C>, A + C)
(<28,0,A>, A) (<28,0,B>, 3 + A) (<28,0,C>, A + C)
* Step 4: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. add(A,B,C) -> n4(A,B,C) [A >= 0] (1,1)
1. m0(A,B,C) -> m1(A,B,C) True (?,1)
2. m2(A,B,C) -> m3(A,B,C) True (?,1)
3. m5(A,B,C) -> m4(E,B,C) [1 + A >= E && E >= 1 + A] (?,1)
4. m3(A,B,C) -> m5(A,B,C) True (?,1)
5. m6(A,B,C) -> m7(A,B,C) True (?,1)
6. m9(A,B,C) -> m8(E,B,C) [2 + A >= E && E >= 2 + A] (?,1)
7. m7(A,B,C) -> m9(A,B,C) True (?,1)
8. n0(A,B,C) -> n1(A,B,C) True (?,1)
9. n3(A,B,C) -> n2(E,B,C) [3 + A >= E && E >= 3 + A] (?,1)
10. n1(A,B,C) -> n3(A,B,C) True (?,1)
11. n7(A,B,C) -> m0(A,B,C) [3 + A >= B] (?,1)
12. n80(A,B,C) -> n7(A,B,C) True (?,1)
13. n81(A,B,C) -> m2(C,B,C) True (?,1)
14. n8(A,B,C) -> c2(n80(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B] (?,1)
15. n90(A,B,C) -> n7(A,B,C) True (?,1)
16. n91(A,B,C) -> m6(C,B,C) True (?,1)
17. n9(A,B,C) -> c2(n90(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B] (?,1)
18. o00(A,B,C) -> n7(A,B,C) True (?,1)
19. o01(A,B,C) -> n0(C,B,C) True (?,1)
20. o0(A,B,C) -> c2(o00(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B] (?,1)
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (?,1)
22. n4(A,B,C) -> o1(A,B,C) [A >= 0] (?,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
27. m1(A,B,C) -> o2(A,B,C) True (?,1)
28. m1(A,B,C) -> n6(A,B,C) True (?,1)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[0->{22},1->{27,28},2->{4},3->{},4->{3},5->{7},6->{},7->{6},8->{10},9->{},10->{9},11->{1},12->{11},13->{2}
,14->{12,13},15->{11},16->{5},17->{15,16},18->{11},19->{8},20->{18,19},21->{1},22->{21},23->{24,25,26}
,24->{14},25->{17},26->{20},27->{23},28->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C)
(< 1,0,A>, A) (< 1,0,B>, 3 + A) (< 1,0,C>, A + C)
(< 2,0,A>, A) (< 2,0,B>, A) (< 2,0,C>, A)
(< 3,0,A>, 1 + A) (< 3,0,B>, A) (< 3,0,C>, A)
(< 4,0,A>, A) (< 4,0,B>, A) (< 4,0,C>, A)
(< 5,0,A>, A) (< 5,0,B>, A) (< 5,0,C>, A)
(< 6,0,A>, 2 + A) (< 6,0,B>, A) (< 6,0,C>, A)
(< 7,0,A>, A) (< 7,0,B>, A) (< 7,0,C>, A)
(< 8,0,A>, A) (< 8,0,B>, A) (< 8,0,C>, A)
(< 9,0,A>, 3 + A) (< 9,0,B>, A) (< 9,0,C>, A)
(<10,0,A>, A) (<10,0,B>, A) (<10,0,C>, A)
(<11,0,A>, A) (<11,0,B>, 3 + A) (<11,0,C>, A)
(<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, A)
(<13,0,A>, A) (<13,0,B>, A) (<13,0,C>, A)
(<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, A)
(<14,1,A>, A) (<14,1,B>, A) (<14,1,C>, A)
(<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, A)
(<16,0,A>, A) (<16,0,B>, A) (<16,0,C>, A)
(<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, A)
(<17,1,A>, A) (<17,1,B>, A) (<17,1,C>, A)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, A)
(<19,0,A>, A) (<19,0,B>, A) (<19,0,C>, A)
(<20,0,A>, A) (<20,0,B>, A) (<20,0,C>, A)
(<20,1,A>, A) (<20,1,B>, A) (<20,1,C>, A)
(<21,0,A>, A) (<21,0,B>, 0) (<21,0,C>, C)
(<21,1,A>, A) (<21,1,B>, 0) (<21,1,C>, C)
(<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, C)
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<27,0,A>, A) (<27,0,B>, 3 + A) (<27,0,C>, A + C)
(<28,0,A>, A) (<28,0,B>, 3 + A) (<28,0,C>, A + C)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [13,16,19,2,5,8,4,7,10,3,6,9,28]
* Step 5: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. add(A,B,C) -> n4(A,B,C) [A >= 0] (1,1)
1. m0(A,B,C) -> m1(A,B,C) True (?,1)
11. n7(A,B,C) -> m0(A,B,C) [3 + A >= B] (?,1)
12. n80(A,B,C) -> n7(A,B,C) True (?,1)
14. n8(A,B,C) -> c2(n80(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B] (?,1)
15. n90(A,B,C) -> n7(A,B,C) True (?,1)
17. n9(A,B,C) -> c2(n90(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B] (?,1)
18. o00(A,B,C) -> n7(A,B,C) True (?,1)
20. o0(A,B,C) -> c2(o00(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B] (?,1)
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (?,1)
22. n4(A,B,C) -> o1(A,B,C) [A >= 0] (?,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
27. m1(A,B,C) -> o2(A,B,C) True (?,1)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[0->{22},1->{27},11->{1},12->{11},14->{12},15->{11},17->{15},18->{11},20->{18},21->{1},22->{21},23->{24,25
,26},24->{14},25->{17},26->{20},27->{23}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C)
(< 1,0,A>, A) (< 1,0,B>, 3 + A) (< 1,0,C>, A + C)
(<11,0,A>, A) (<11,0,B>, 3 + A) (<11,0,C>, A)
(<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, A)
(<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, A)
(<14,1,A>, A) (<14,1,B>, A) (<14,1,C>, A)
(<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, A)
(<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, A)
(<17,1,A>, A) (<17,1,B>, A) (<17,1,C>, A)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, A)
(<20,0,A>, A) (<20,0,B>, A) (<20,0,C>, A)
(<20,1,A>, A) (<20,1,B>, A) (<20,1,C>, A)
(<21,0,A>, A) (<21,0,B>, 0) (<21,0,C>, C)
(<21,1,A>, A) (<21,1,B>, 0) (<21,1,C>, C)
(<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, C)
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<27,0,A>, A) (<27,0,B>, 3 + A) (<27,0,C>, A + C)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(add) = 2
p(m0) = 1
p(m1) = 1
p(n4) = 2
p(n5) = 0
p(n7) = 1
p(n8) = 1
p(n80) = 1
p(n81) = 0
p(n9) = 1
p(n90) = 1
p(n91) = 0
p(o0) = 1
p(o00) = 1
p(o01) = 0
p(o1) = 1
p(o2) = 1
p(o3) = 1
The following rules are strictly oriented:
[A >= 0] ==>
n4(A,B,C) = 2
> 1
= o1(A,B,C)
The following rules are weakly oriented:
[A >= 0] ==>
add(A,B,C) = 2
>= 2
= n4(A,B,C)
True ==>
m0(A,B,C) = 1
>= 1
= m1(A,B,C)
[3 + A >= B] ==>
n7(A,B,C) = 1
>= 1
= m0(A,B,C)
True ==>
n80(A,B,C) = 1
>= 1
= n7(A,B,C)
[A >= B && 1 + B >= E && E >= 1 + B] ==>
n8(A,B,C) = 1
>= 1
= c2(n80(A,E,B),n81(A,E,B))
True ==>
n90(A,B,C) = 1
>= 1
= n7(A,B,C)
[A >= B && 2 + B >= E && E >= 2 + B] ==>
n9(A,B,C) = 1
>= 1
= c2(n90(A,E,B),n91(A,E,B))
True ==>
o00(A,B,C) = 1
>= 1
= n7(A,B,C)
[A >= B && 3 + B >= E && E >= 3 + B] ==>
o0(A,B,C) = 1
>= 1
= c2(o00(A,E,B),o01(A,E,B))
[A >= 0] ==>
o1(A,B,C) = 1
>= 1
= c2(n5(A,0,C),m0(A,0,C))
[A >= B] ==>
o2(A,B,C) = 1
>= 1
= o3(A,B,C)
True ==>
o3(A,B,C) = 1
>= 1
= n8(A,B,C)
True ==>
o3(A,B,C) = 1
>= 1
= n9(A,B,C)
True ==>
o3(A,B,C) = 1
>= 1
= o0(A,B,C)
True ==>
m1(A,B,C) = 1
>= 1
= o2(A,B,C)
* Step 6: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. add(A,B,C) -> n4(A,B,C) [A >= 0] (1,1)
1. m0(A,B,C) -> m1(A,B,C) True (?,1)
11. n7(A,B,C) -> m0(A,B,C) [3 + A >= B] (?,1)
12. n80(A,B,C) -> n7(A,B,C) True (?,1)
14. n8(A,B,C) -> c2(n80(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B] (?,1)
15. n90(A,B,C) -> n7(A,B,C) True (?,1)
17. n9(A,B,C) -> c2(n90(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B] (?,1)
18. o00(A,B,C) -> n7(A,B,C) True (?,1)
20. o0(A,B,C) -> c2(o00(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B] (?,1)
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (?,1)
22. n4(A,B,C) -> o1(A,B,C) [A >= 0] (2,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
27. m1(A,B,C) -> o2(A,B,C) True (?,1)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[0->{22},1->{27},11->{1},12->{11},14->{12},15->{11},17->{15},18->{11},20->{18},21->{1},22->{21},23->{24,25
,26},24->{14},25->{17},26->{20},27->{23}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C)
(< 1,0,A>, A) (< 1,0,B>, 3 + A) (< 1,0,C>, A + C)
(<11,0,A>, A) (<11,0,B>, 3 + A) (<11,0,C>, A)
(<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, A)
(<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, A)
(<14,1,A>, A) (<14,1,B>, A) (<14,1,C>, A)
(<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, A)
(<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, A)
(<17,1,A>, A) (<17,1,B>, A) (<17,1,C>, A)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, A)
(<20,0,A>, A) (<20,0,B>, A) (<20,0,C>, A)
(<20,1,A>, A) (<20,1,B>, A) (<20,1,C>, A)
(<21,0,A>, A) (<21,0,B>, 0) (<21,0,C>, C)
(<21,1,A>, A) (<21,1,B>, 0) (<21,1,C>, C)
(<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, C)
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<27,0,A>, A) (<27,0,B>, 3 + A) (<27,0,C>, A + C)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 7: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. add(A,B,C) -> n4(A,B,C) [A >= 0] (1,1)
1. m0(A,B,C) -> m1(A,B,C) True (?,1)
11. n7(A,B,C) -> m0(A,B,C) [3 + A >= B] (?,1)
12. n80(A,B,C) -> n7(A,B,C) True (?,1)
14. n8(A,B,C) -> c2(n80(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B] (?,1)
15. n90(A,B,C) -> n7(A,B,C) True (?,1)
17. n9(A,B,C) -> c2(n90(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B] (?,1)
18. o00(A,B,C) -> n7(A,B,C) True (?,1)
20. o0(A,B,C) -> c2(o00(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B] (?,1)
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (2,1)
22. n4(A,B,C) -> o1(A,B,C) [A >= 0] (2,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
27. m1(A,B,C) -> o2(A,B,C) True (?,1)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[0->{22},1->{27},11->{1},12->{11},14->{12},15->{11},17->{15},18->{11},20->{18},21->{1},22->{21},23->{24,25
,26},24->{14},25->{17},26->{20},27->{23}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C)
(< 1,0,A>, A) (< 1,0,B>, 3 + A) (< 1,0,C>, A + C)
(<11,0,A>, A) (<11,0,B>, 3 + A) (<11,0,C>, A)
(<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, A)
(<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, A)
(<14,1,A>, A) (<14,1,B>, A) (<14,1,C>, A)
(<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, A)
(<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, A)
(<17,1,A>, A) (<17,1,B>, A) (<17,1,C>, A)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, A)
(<20,0,A>, A) (<20,0,B>, A) (<20,0,C>, A)
(<20,1,A>, A) (<20,1,B>, A) (<20,1,C>, A)
(<21,0,A>, A) (<21,0,B>, 0) (<21,0,C>, C)
(<21,1,A>, A) (<21,1,B>, 0) (<21,1,C>, C)
(<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, C)
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<27,0,A>, A) (<27,0,B>, 3 + A) (<27,0,C>, A + C)
+ Applied Processor:
ChainProcessor False [0,1,11,12,14,15,17,18,20,21,22,23,24,25,26,27]
+ Details:
We chained rule 0 to obtain the rules [28] .
* Step 8: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
1. m0(A,B,C) -> m1(A,B,C) True (?,1)
11. n7(A,B,C) -> m0(A,B,C) [3 + A >= B] (?,1)
12. n80(A,B,C) -> n7(A,B,C) True (?,1)
14. n8(A,B,C) -> c2(n80(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B] (?,1)
15. n90(A,B,C) -> n7(A,B,C) True (?,1)
17. n9(A,B,C) -> c2(n90(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B] (?,1)
18. o00(A,B,C) -> n7(A,B,C) True (?,1)
20. o0(A,B,C) -> c2(o00(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B] (?,1)
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (2,1)
22. n4(A,B,C) -> o1(A,B,C) [A >= 0] (2,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
27. m1(A,B,C) -> o2(A,B,C) True (?,1)
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[1->{27},11->{1},12->{11},14->{12},15->{11},17->{15},18->{11},20->{18},21->{1},22->{21},23->{24,25,26}
,24->{14},25->{17},26->{20},27->{23},28->{21}]
Sizebounds:
(< 1,0,A>, A) (< 1,0,B>, 3 + A) (< 1,0,C>, A + C)
(<11,0,A>, A) (<11,0,B>, 3 + A) (<11,0,C>, A)
(<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, A)
(<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, A)
(<14,1,A>, A) (<14,1,B>, A) (<14,1,C>, A)
(<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, A)
(<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, A)
(<17,1,A>, A) (<17,1,B>, A) (<17,1,C>, A)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, A)
(<20,0,A>, A) (<20,0,B>, A) (<20,0,C>, A)
(<20,1,A>, A) (<20,1,B>, A) (<20,1,C>, A)
(<21,0,A>, A) (<21,0,B>, 0) (<21,0,C>, C)
(<21,1,A>, A) (<21,1,B>, 0) (<21,1,C>, C)
(<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, C)
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<27,0,A>, A) (<27,0,B>, 3 + A) (<27,0,C>, A + C)
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [22]
* Step 9: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
1. m0(A,B,C) -> m1(A,B,C) True (?,1)
11. n7(A,B,C) -> m0(A,B,C) [3 + A >= B] (?,1)
12. n80(A,B,C) -> n7(A,B,C) True (?,1)
14. n8(A,B,C) -> c2(n80(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B] (?,1)
15. n90(A,B,C) -> n7(A,B,C) True (?,1)
17. n9(A,B,C) -> c2(n90(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B] (?,1)
18. o00(A,B,C) -> n7(A,B,C) True (?,1)
20. o0(A,B,C) -> c2(o00(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B] (?,1)
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (2,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
27. m1(A,B,C) -> o2(A,B,C) True (?,1)
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[1->{27},11->{1},12->{11},14->{12},15->{11},17->{15},18->{11},20->{18},21->{1},23->{24,25,26},24->{14}
,25->{17},26->{20},27->{23},28->{21}]
Sizebounds:
(< 1,0,A>, A) (< 1,0,B>, 3 + A) (< 1,0,C>, A + C)
(<11,0,A>, A) (<11,0,B>, 3 + A) (<11,0,C>, A)
(<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, A)
(<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, A)
(<14,1,A>, A) (<14,1,B>, A) (<14,1,C>, A)
(<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, A)
(<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, A)
(<17,1,A>, A) (<17,1,B>, A) (<17,1,C>, A)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, A)
(<20,0,A>, A) (<20,0,B>, A) (<20,0,C>, A)
(<20,1,A>, A) (<20,1,B>, A) (<20,1,C>, A)
(<21,0,A>, A) (<21,0,B>, 0) (<21,0,C>, C)
(<21,1,A>, A) (<21,1,B>, 0) (<21,1,C>, C)
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<27,0,A>, A) (<27,0,B>, 3 + A) (<27,0,C>, A + C)
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
+ Applied Processor:
ChainProcessor False [1,11,12,14,15,17,18,20,21,23,24,25,26,27,28]
+ Details:
We chained rule 1 to obtain the rules [29] .
* Step 10: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
11. n7(A,B,C) -> m0(A,B,C) [3 + A >= B] (?,1)
12. n80(A,B,C) -> n7(A,B,C) True (?,1)
14. n8(A,B,C) -> c2(n80(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B] (?,1)
15. n90(A,B,C) -> n7(A,B,C) True (?,1)
17. n9(A,B,C) -> c2(n90(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B] (?,1)
18. o00(A,B,C) -> n7(A,B,C) True (?,1)
20. o0(A,B,C) -> c2(o00(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B] (?,1)
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (2,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
27. m1(A,B,C) -> o2(A,B,C) True (?,1)
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
29. m0(A,B,C) -> o2(A,B,C) True (?,2)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[11->{29},12->{11},14->{12},15->{11},17->{15},18->{11},20->{18},21->{29},23->{24,25,26},24->{14},25->{17}
,26->{20},27->{23},28->{21},29->{23}]
Sizebounds:
(<11,0,A>, A) (<11,0,B>, 3 + A) (<11,0,C>, A)
(<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, A)
(<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, A)
(<14,1,A>, A) (<14,1,B>, A) (<14,1,C>, A)
(<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, A)
(<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, A)
(<17,1,A>, A) (<17,1,B>, A) (<17,1,C>, A)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, A)
(<20,0,A>, A) (<20,0,B>, A) (<20,0,C>, A)
(<20,1,A>, A) (<20,1,B>, A) (<20,1,C>, A)
(<21,0,A>, A) (<21,0,B>, 0) (<21,0,C>, C)
(<21,1,A>, A) (<21,1,B>, 0) (<21,1,C>, C)
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<27,0,A>, A) (<27,0,B>, 3 + A) (<27,0,C>, A + C)
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<29,0,A>, A) (<29,0,B>, 3 + A) (<29,0,C>, A + C)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [27]
* Step 11: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
11. n7(A,B,C) -> m0(A,B,C) [3 + A >= B] (?,1)
12. n80(A,B,C) -> n7(A,B,C) True (?,1)
14. n8(A,B,C) -> c2(n80(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B] (?,1)
15. n90(A,B,C) -> n7(A,B,C) True (?,1)
17. n9(A,B,C) -> c2(n90(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B] (?,1)
18. o00(A,B,C) -> n7(A,B,C) True (?,1)
20. o0(A,B,C) -> c2(o00(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B] (?,1)
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (2,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
29. m0(A,B,C) -> o2(A,B,C) True (?,2)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[11->{29},12->{11},14->{12},15->{11},17->{15},18->{11},20->{18},21->{29},23->{24,25,26},24->{14},25->{17}
,26->{20},28->{21},29->{23}]
Sizebounds:
(<11,0,A>, A) (<11,0,B>, 3 + A) (<11,0,C>, A)
(<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, A)
(<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, A)
(<14,1,A>, A) (<14,1,B>, A) (<14,1,C>, A)
(<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, A)
(<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, A)
(<17,1,A>, A) (<17,1,B>, A) (<17,1,C>, A)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, A)
(<20,0,A>, A) (<20,0,B>, A) (<20,0,C>, A)
(<20,1,A>, A) (<20,1,B>, A) (<20,1,C>, A)
(<21,0,A>, A) (<21,0,B>, 0) (<21,0,C>, C)
(<21,1,A>, A) (<21,1,B>, 0) (<21,1,C>, C)
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<29,0,A>, A) (<29,0,B>, 3 + A) (<29,0,C>, A + C)
+ Applied Processor:
ChainProcessor False [11,12,14,15,17,18,20,21,23,24,25,26,28,29]
+ Details:
We chained rule 11 to obtain the rules [30] .
* Step 12: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
12. n80(A,B,C) -> n7(A,B,C) True (?,1)
14. n8(A,B,C) -> c2(n80(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B] (?,1)
15. n90(A,B,C) -> n7(A,B,C) True (?,1)
17. n9(A,B,C) -> c2(n90(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B] (?,1)
18. o00(A,B,C) -> n7(A,B,C) True (?,1)
20. o0(A,B,C) -> c2(o00(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B] (?,1)
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (2,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
29. m0(A,B,C) -> o2(A,B,C) True (?,2)
30. n7(A,B,C) -> o2(A,B,C) [3 + A >= B] (?,3)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[12->{30},14->{12},15->{30},17->{15},18->{30},20->{18},21->{29},23->{24,25,26},24->{14},25->{17},26->{20}
,28->{21},29->{23},30->{23}]
Sizebounds:
(<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, A)
(<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, A)
(<14,1,A>, A) (<14,1,B>, A) (<14,1,C>, A)
(<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, A)
(<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, A)
(<17,1,A>, A) (<17,1,B>, A) (<17,1,C>, A)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, A)
(<20,0,A>, A) (<20,0,B>, A) (<20,0,C>, A)
(<20,1,A>, A) (<20,1,B>, A) (<20,1,C>, A)
(<21,0,A>, A) (<21,0,B>, 0) (<21,0,C>, C)
(<21,1,A>, A) (<21,1,B>, 0) (<21,1,C>, C)
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<29,0,A>, A) (<29,0,B>, 3 + A) (<29,0,C>, A + C)
(<30,0,A>, A) (<30,0,B>, 3 + A) (<30,0,C>, A + C)
+ Applied Processor:
ChainProcessor False [12,14,15,17,18,20,21,23,24,25,26,28,29,30]
+ Details:
We chained rule 12 to obtain the rules [31] .
* Step 13: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
14. n8(A,B,C) -> c2(n80(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B] (?,1)
15. n90(A,B,C) -> n7(A,B,C) True (?,1)
17. n9(A,B,C) -> c2(n90(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B] (?,1)
18. o00(A,B,C) -> n7(A,B,C) True (?,1)
20. o0(A,B,C) -> c2(o00(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B] (?,1)
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (2,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
29. m0(A,B,C) -> o2(A,B,C) True (?,2)
30. n7(A,B,C) -> o2(A,B,C) [3 + A >= B] (?,3)
31. n80(A,B,C) -> o2(A,B,C) [3 + A >= B] (?,4)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[14->{31},15->{30},17->{15},18->{30},20->{18},21->{29},23->{24,25,26},24->{14},25->{17},26->{20},28->{21}
,29->{23},30->{23},31->{23}]
Sizebounds:
(<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, A)
(<14,1,A>, A) (<14,1,B>, A) (<14,1,C>, A)
(<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, A)
(<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, A)
(<17,1,A>, A) (<17,1,B>, A) (<17,1,C>, A)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, A)
(<20,0,A>, A) (<20,0,B>, A) (<20,0,C>, A)
(<20,1,A>, A) (<20,1,B>, A) (<20,1,C>, A)
(<21,0,A>, A) (<21,0,B>, 0) (<21,0,C>, C)
(<21,1,A>, A) (<21,1,B>, 0) (<21,1,C>, C)
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<29,0,A>, A) (<29,0,B>, 3 + A) (<29,0,C>, A + C)
(<30,0,A>, A) (<30,0,B>, 3 + A) (<30,0,C>, A + C)
(<31,0,A>, A) (<31,0,B>, 3 + A) (<31,0,C>, A + C)
+ Applied Processor:
ChainProcessor False [14,15,17,18,20,21,23,24,25,26,28,29,30,31]
+ Details:
We chained rule 14 to obtain the rules [32] .
* Step 14: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
15. n90(A,B,C) -> n7(A,B,C) True (?,1)
17. n9(A,B,C) -> c2(n90(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B] (?,1)
18. o00(A,B,C) -> n7(A,B,C) True (?,1)
20. o0(A,B,C) -> c2(o00(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B] (?,1)
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (2,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
29. m0(A,B,C) -> o2(A,B,C) True (?,2)
30. n7(A,B,C) -> o2(A,B,C) [3 + A >= B] (?,3)
31. n80(A,B,C) -> o2(A,B,C) [3 + A >= B] (?,4)
32. n8(A,B,C) -> c2(o2(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E] (?,5)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[15->{30},17->{15},18->{30},20->{18},21->{29},23->{24,25,26},24->{32},25->{17},26->{20},28->{21},29->{23}
,30->{23},31->{23},32->{23}]
Sizebounds:
(<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, A)
(<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, A)
(<17,1,A>, A) (<17,1,B>, A) (<17,1,C>, A)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, A)
(<20,0,A>, A) (<20,0,B>, A) (<20,0,C>, A)
(<20,1,A>, A) (<20,1,B>, A) (<20,1,C>, A)
(<21,0,A>, A) (<21,0,B>, 0) (<21,0,C>, C)
(<21,1,A>, A) (<21,1,B>, 0) (<21,1,C>, C)
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<29,0,A>, A) (<29,0,B>, 3 + A) (<29,0,C>, A + C)
(<30,0,A>, A) (<30,0,B>, 3 + A) (<30,0,C>, A + C)
(<31,0,A>, A) (<31,0,B>, 3 + A) (<31,0,C>, A + C)
(<32,0,A>, A) (<32,0,B>, 3 + A) (<32,0,C>, A + C)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [31]
* Step 15: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
15. n90(A,B,C) -> n7(A,B,C) True (?,1)
17. n9(A,B,C) -> c2(n90(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B] (?,1)
18. o00(A,B,C) -> n7(A,B,C) True (?,1)
20. o0(A,B,C) -> c2(o00(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B] (?,1)
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (2,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
29. m0(A,B,C) -> o2(A,B,C) True (?,2)
30. n7(A,B,C) -> o2(A,B,C) [3 + A >= B] (?,3)
32. n8(A,B,C) -> c2(o2(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E] (?,5)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[15->{30},17->{15},18->{30},20->{18},21->{29},23->{24,25,26},24->{32},25->{17},26->{20},28->{21},29->{23}
,30->{23},32->{23}]
Sizebounds:
(<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, A)
(<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, A)
(<17,1,A>, A) (<17,1,B>, A) (<17,1,C>, A)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, A)
(<20,0,A>, A) (<20,0,B>, A) (<20,0,C>, A)
(<20,1,A>, A) (<20,1,B>, A) (<20,1,C>, A)
(<21,0,A>, A) (<21,0,B>, 0) (<21,0,C>, C)
(<21,1,A>, A) (<21,1,B>, 0) (<21,1,C>, C)
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<29,0,A>, A) (<29,0,B>, 3 + A) (<29,0,C>, A + C)
(<30,0,A>, A) (<30,0,B>, 3 + A) (<30,0,C>, A + C)
(<32,0,A>, A) (<32,0,B>, 3 + A) (<32,0,C>, A + C)
+ Applied Processor:
ChainProcessor False [15,17,18,20,21,23,24,25,26,28,29,30,32]
+ Details:
We chained rule 15 to obtain the rules [33] .
* Step 16: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
17. n9(A,B,C) -> c2(n90(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B] (?,1)
18. o00(A,B,C) -> n7(A,B,C) True (?,1)
20. o0(A,B,C) -> c2(o00(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B] (?,1)
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (2,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
29. m0(A,B,C) -> o2(A,B,C) True (?,2)
30. n7(A,B,C) -> o2(A,B,C) [3 + A >= B] (?,3)
32. n8(A,B,C) -> c2(o2(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E] (?,5)
33. n90(A,B,C) -> o2(A,B,C) [3 + A >= B] (?,4)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[17->{33},18->{30},20->{18},21->{29},23->{24,25,26},24->{32},25->{17},26->{20},28->{21},29->{23},30->{23}
,32->{23},33->{23}]
Sizebounds:
(<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, A)
(<17,1,A>, A) (<17,1,B>, A) (<17,1,C>, A)
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, A)
(<20,0,A>, A) (<20,0,B>, A) (<20,0,C>, A)
(<20,1,A>, A) (<20,1,B>, A) (<20,1,C>, A)
(<21,0,A>, A) (<21,0,B>, 0) (<21,0,C>, C)
(<21,1,A>, A) (<21,1,B>, 0) (<21,1,C>, C)
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<29,0,A>, A) (<29,0,B>, 3 + A) (<29,0,C>, A + C)
(<30,0,A>, A) (<30,0,B>, 3 + A) (<30,0,C>, A + C)
(<32,0,A>, A) (<32,0,B>, 3 + A) (<32,0,C>, A + C)
(<33,0,A>, A) (<33,0,B>, 3 + A) (<33,0,C>, A + C)
+ Applied Processor:
ChainProcessor False [17,18,20,21,23,24,25,26,28,29,30,32,33]
+ Details:
We chained rule 17 to obtain the rules [34] .
* Step 17: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
18. o00(A,B,C) -> n7(A,B,C) True (?,1)
20. o0(A,B,C) -> c2(o00(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B] (?,1)
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (2,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
29. m0(A,B,C) -> o2(A,B,C) True (?,2)
30. n7(A,B,C) -> o2(A,B,C) [3 + A >= B] (?,3)
32. n8(A,B,C) -> c2(o2(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E] (?,5)
33. n90(A,B,C) -> o2(A,B,C) [3 + A >= B] (?,4)
34. n9(A,B,C) -> c2(o2(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E] (?,5)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[18->{30},20->{18},21->{29},23->{24,25,26},24->{32},25->{34},26->{20},28->{21},29->{23},30->{23},32->{23}
,33->{23},34->{23}]
Sizebounds:
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, A)
(<20,0,A>, A) (<20,0,B>, A) (<20,0,C>, A)
(<20,1,A>, A) (<20,1,B>, A) (<20,1,C>, A)
(<21,0,A>, A) (<21,0,B>, 0) (<21,0,C>, C)
(<21,1,A>, A) (<21,1,B>, 0) (<21,1,C>, C)
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<29,0,A>, A) (<29,0,B>, 3 + A) (<29,0,C>, A + C)
(<30,0,A>, A) (<30,0,B>, 3 + A) (<30,0,C>, A + C)
(<32,0,A>, A) (<32,0,B>, 3 + A) (<32,0,C>, A + C)
(<33,0,A>, A) (<33,0,B>, 3 + A) (<33,0,C>, A + C)
(<34,0,A>, A) (<34,0,B>, 3 + A) (<34,0,C>, A + C)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [33]
* Step 18: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
18. o00(A,B,C) -> n7(A,B,C) True (?,1)
20. o0(A,B,C) -> c2(o00(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B] (?,1)
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (2,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
29. m0(A,B,C) -> o2(A,B,C) True (?,2)
30. n7(A,B,C) -> o2(A,B,C) [3 + A >= B] (?,3)
32. n8(A,B,C) -> c2(o2(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E] (?,5)
34. n9(A,B,C) -> c2(o2(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E] (?,5)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[18->{30},20->{18},21->{29},23->{24,25,26},24->{32},25->{34},26->{20},28->{21},29->{23},30->{23},32->{23}
,34->{23}]
Sizebounds:
(<18,0,A>, A) (<18,0,B>, A) (<18,0,C>, A)
(<20,0,A>, A) (<20,0,B>, A) (<20,0,C>, A)
(<20,1,A>, A) (<20,1,B>, A) (<20,1,C>, A)
(<21,0,A>, A) (<21,0,B>, 0) (<21,0,C>, C)
(<21,1,A>, A) (<21,1,B>, 0) (<21,1,C>, C)
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<29,0,A>, A) (<29,0,B>, 3 + A) (<29,0,C>, A + C)
(<30,0,A>, A) (<30,0,B>, 3 + A) (<30,0,C>, A + C)
(<32,0,A>, A) (<32,0,B>, 3 + A) (<32,0,C>, A + C)
(<34,0,A>, A) (<34,0,B>, 3 + A) (<34,0,C>, A + C)
+ Applied Processor:
ChainProcessor False [18,20,21,23,24,25,26,28,29,30,32,34]
+ Details:
We chained rule 18 to obtain the rules [35] .
* Step 19: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
20. o0(A,B,C) -> c2(o00(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B] (?,1)
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (2,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
29. m0(A,B,C) -> o2(A,B,C) True (?,2)
30. n7(A,B,C) -> o2(A,B,C) [3 + A >= B] (?,3)
32. n8(A,B,C) -> c2(o2(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E] (?,5)
34. n9(A,B,C) -> c2(o2(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E] (?,5)
35. o00(A,B,C) -> o2(A,B,C) [3 + A >= B] (?,4)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[20->{35},21->{29},23->{24,25,26},24->{32},25->{34},26->{20},28->{21},29->{23},30->{23},32->{23},34->{23}
,35->{23}]
Sizebounds:
(<20,0,A>, A) (<20,0,B>, A) (<20,0,C>, A)
(<20,1,A>, A) (<20,1,B>, A) (<20,1,C>, A)
(<21,0,A>, A) (<21,0,B>, 0) (<21,0,C>, C)
(<21,1,A>, A) (<21,1,B>, 0) (<21,1,C>, C)
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<29,0,A>, A) (<29,0,B>, 3 + A) (<29,0,C>, A + C)
(<30,0,A>, A) (<30,0,B>, 3 + A) (<30,0,C>, A + C)
(<32,0,A>, A) (<32,0,B>, 3 + A) (<32,0,C>, A + C)
(<34,0,A>, A) (<34,0,B>, 3 + A) (<34,0,C>, A + C)
(<35,0,A>, A) (<35,0,B>, 3 + A) (<35,0,C>, A + C)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [30]
* Step 20: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
20. o0(A,B,C) -> c2(o00(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B] (?,1)
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (2,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
29. m0(A,B,C) -> o2(A,B,C) True (?,2)
32. n8(A,B,C) -> c2(o2(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E] (?,5)
34. n9(A,B,C) -> c2(o2(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E] (?,5)
35. o00(A,B,C) -> o2(A,B,C) [3 + A >= B] (?,4)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[20->{35},21->{29},23->{24,25,26},24->{32},25->{34},26->{20},28->{21},29->{23},32->{23},34->{23},35->{23}]
Sizebounds:
(<20,0,A>, A) (<20,0,B>, A) (<20,0,C>, A)
(<20,1,A>, A) (<20,1,B>, A) (<20,1,C>, A)
(<21,0,A>, A) (<21,0,B>, 0) (<21,0,C>, C)
(<21,1,A>, A) (<21,1,B>, 0) (<21,1,C>, C)
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<29,0,A>, A) (<29,0,B>, 3 + A) (<29,0,C>, A + C)
(<32,0,A>, A) (<32,0,B>, 3 + A) (<32,0,C>, A + C)
(<34,0,A>, A) (<34,0,B>, 3 + A) (<34,0,C>, A + C)
(<35,0,A>, A) (<35,0,B>, 3 + A) (<35,0,C>, A + C)
+ Applied Processor:
ChainProcessor False [20,21,23,24,25,26,28,29,32,34,35]
+ Details:
We chained rule 20 to obtain the rules [36] .
* Step 21: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (2,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
29. m0(A,B,C) -> o2(A,B,C) True (?,2)
32. n8(A,B,C) -> c2(o2(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E] (?,5)
34. n9(A,B,C) -> c2(o2(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E] (?,5)
35. o00(A,B,C) -> o2(A,B,C) [3 + A >= B] (?,4)
36. o0(A,B,C) -> c2(o2(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E] (?,5)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[21->{29},23->{24,25,26},24->{32},25->{34},26->{36},28->{21},29->{23},32->{23},34->{23},35->{23},36->{23}]
Sizebounds:
(<21,0,A>, A) (<21,0,B>, 0) (<21,0,C>, C)
(<21,1,A>, A) (<21,1,B>, 0) (<21,1,C>, C)
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<29,0,A>, A) (<29,0,B>, 3 + A) (<29,0,C>, A + C)
(<32,0,A>, A) (<32,0,B>, 3 + A) (<32,0,C>, A + C)
(<34,0,A>, A) (<34,0,B>, 3 + A) (<34,0,C>, A + C)
(<35,0,A>, A) (<35,0,B>, 3 + A) (<35,0,C>, A + C)
(<36,0,A>, A) (<36,0,B>, 3 + A) (<36,0,C>, A + C)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [35]
* Step 22: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
21. o1(A,B,C) -> c2(n5(A,0,C),m0(A,0,C)) [A >= 0] (2,1)
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
29. m0(A,B,C) -> o2(A,B,C) True (?,2)
32. n8(A,B,C) -> c2(o2(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E] (?,5)
34. n9(A,B,C) -> c2(o2(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E] (?,5)
36. o0(A,B,C) -> c2(o2(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E] (?,5)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[21->{29},23->{24,25,26},24->{32},25->{34},26->{36},28->{21},29->{23},32->{23},34->{23},36->{23}]
Sizebounds:
(<21,0,A>, A) (<21,0,B>, 0) (<21,0,C>, C)
(<21,1,A>, A) (<21,1,B>, 0) (<21,1,C>, C)
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<29,0,A>, A) (<29,0,B>, 3 + A) (<29,0,C>, A + C)
(<32,0,A>, A) (<32,0,B>, 3 + A) (<32,0,C>, A + C)
(<34,0,A>, A) (<34,0,B>, 3 + A) (<34,0,C>, A + C)
(<36,0,A>, A) (<36,0,B>, 3 + A) (<36,0,C>, A + C)
+ Applied Processor:
ChainProcessor False [21,23,24,25,26,28,29,32,34,36]
+ Details:
We chained rule 21 to obtain the rules [37] .
* Step 23: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
29. m0(A,B,C) -> o2(A,B,C) True (?,2)
32. n8(A,B,C) -> c2(o2(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E] (?,5)
34. n9(A,B,C) -> c2(o2(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E] (?,5)
36. o0(A,B,C) -> c2(o2(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E] (?,5)
37. o1(A,B,C) -> c2(n5(A,0,C),o2(A,0,C)) [A >= 0] (2,3)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[23->{24,25,26},24->{32},25->{34},26->{36},28->{37},29->{23},32->{23},34->{23},36->{23},37->{23}]
Sizebounds:
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<29,0,A>, A) (<29,0,B>, 3 + A) (<29,0,C>, A + C)
(<32,0,A>, A) (<32,0,B>, 3 + A) (<32,0,C>, A + C)
(<34,0,A>, A) (<34,0,B>, 3 + A) (<34,0,C>, A + C)
(<36,0,A>, A) (<36,0,B>, 3 + A) (<36,0,C>, A + C)
(<37,0,A>, A) (<37,0,B>, 3 + A) (<37,0,C>, A + C)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [29]
* Step 24: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
23. o2(A,B,C) -> o3(A,B,C) [A >= B] (?,1)
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
32. n8(A,B,C) -> c2(o2(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E] (?,5)
34. n9(A,B,C) -> c2(o2(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E] (?,5)
36. o0(A,B,C) -> c2(o2(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E] (?,5)
37. o1(A,B,C) -> c2(n5(A,0,C),o2(A,0,C)) [A >= 0] (2,3)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[23->{24,25,26},24->{32},25->{34},26->{36},28->{37},32->{23},34->{23},36->{23},37->{23}]
Sizebounds:
(<23,0,A>, A) (<23,0,B>, A) (<23,0,C>, A + C)
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<32,0,A>, A) (<32,0,B>, 3 + A) (<32,0,C>, A + C)
(<34,0,A>, A) (<34,0,B>, 3 + A) (<34,0,C>, A + C)
(<36,0,A>, A) (<36,0,B>, 3 + A) (<36,0,C>, A + C)
(<37,0,A>, A) (<37,0,B>, 3 + A) (<37,0,C>, A + C)
+ Applied Processor:
ChainProcessor False [23,24,25,26,28,32,34,36,37]
+ Details:
We chained rule 23 to obtain the rules [38,39,40] .
* Step 25: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
24. o3(A,B,C) -> n8(A,B,C) True (?,1)
25. o3(A,B,C) -> n9(A,B,C) True (?,1)
26. o3(A,B,C) -> o0(A,B,C) True (?,1)
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
32. n8(A,B,C) -> c2(o2(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E] (?,5)
34. n9(A,B,C) -> c2(o2(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E] (?,5)
36. o0(A,B,C) -> c2(o2(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E] (?,5)
37. o1(A,B,C) -> c2(n5(A,0,C),o2(A,0,C)) [A >= 0] (2,3)
38. o2(A,B,C) -> n8(A,B,C) [A >= B] (?,2)
39. o2(A,B,C) -> n9(A,B,C) [A >= B] (?,2)
40. o2(A,B,C) -> o0(A,B,C) [A >= B] (?,2)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[24->{32},25->{34},26->{36},28->{37},32->{38,39,40},34->{38,39,40},36->{38,39,40},37->{38,39,40},38->{32}
,39->{34},40->{36}]
Sizebounds:
(<24,0,A>, A) (<24,0,B>, A) (<24,0,C>, A + C)
(<25,0,A>, A) (<25,0,B>, A) (<25,0,C>, A + C)
(<26,0,A>, A) (<26,0,B>, A) (<26,0,C>, A + C)
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<32,0,A>, A) (<32,0,B>, 3 + A) (<32,0,C>, A + C)
(<34,0,A>, A) (<34,0,B>, 3 + A) (<34,0,C>, A + C)
(<36,0,A>, A) (<36,0,B>, 3 + A) (<36,0,C>, A + C)
(<37,0,A>, A) (<37,0,B>, 3 + A) (<37,0,C>, A + C)
(<38,0,A>, A) (<38,0,B>, A) (<38,0,C>, A + C)
(<39,0,A>, A) (<39,0,B>, A) (<39,0,C>, A + C)
(<40,0,A>, A) (<40,0,B>, A) (<40,0,C>, A + C)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [24,25,26]
* Step 26: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
32. n8(A,B,C) -> c2(o2(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E] (?,5)
34. n9(A,B,C) -> c2(o2(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E] (?,5)
36. o0(A,B,C) -> c2(o2(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E] (?,5)
37. o1(A,B,C) -> c2(n5(A,0,C),o2(A,0,C)) [A >= 0] (2,3)
38. o2(A,B,C) -> n8(A,B,C) [A >= B] (?,2)
39. o2(A,B,C) -> n9(A,B,C) [A >= B] (?,2)
40. o2(A,B,C) -> o0(A,B,C) [A >= B] (?,2)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[28->{37},32->{38,39,40},34->{38,39,40},36->{38,39,40},37->{38,39,40},38->{32},39->{34},40->{36}]
Sizebounds:
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<32,0,A>, A) (<32,0,B>, 3 + A) (<32,0,C>, A + C)
(<34,0,A>, A) (<34,0,B>, 3 + A) (<34,0,C>, A + C)
(<36,0,A>, A) (<36,0,B>, 3 + A) (<36,0,C>, A + C)
(<37,0,A>, A) (<37,0,B>, 3 + A) (<37,0,C>, A + C)
(<38,0,A>, A) (<38,0,B>, A) (<38,0,C>, A + C)
(<39,0,A>, A) (<39,0,B>, A) (<39,0,C>, A + C)
(<40,0,A>, A) (<40,0,B>, A) (<40,0,C>, A + C)
+ Applied Processor:
ChainProcessor False [28,32,34,36,37,38,39,40]
+ Details:
We chained rule 32 to obtain the rules [41,42,43] .
* Step 27: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
34. n9(A,B,C) -> c2(o2(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E] (?,5)
36. o0(A,B,C) -> c2(o2(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E] (?,5)
37. o1(A,B,C) -> c2(n5(A,0,C),o2(A,0,C)) [A >= 0] (2,3)
38. o2(A,B,C) -> n8(A,B,C) [A >= B] (?,2)
39. o2(A,B,C) -> n9(A,B,C) [A >= B] (?,2)
40. o2(A,B,C) -> o0(A,B,C) [A >= B] (?,2)
41. n8(A,B,C) -> c2(n8(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
42. n8(A,B,C) -> c2(n9(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
43. n8(A,B,C) -> c2(o0(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[28->{37},34->{38,39,40},36->{38,39,40},37->{38,39,40},38->{41,42,43},39->{34},40->{36},41->{41,42,43}
,42->{34},43->{36}]
Sizebounds:
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<34,0,A>, A) (<34,0,B>, 3 + A) (<34,0,C>, A + C)
(<36,0,A>, A) (<36,0,B>, 3 + A) (<36,0,C>, A + C)
(<37,0,A>, A) (<37,0,B>, 3 + A) (<37,0,C>, A + C)
(<38,0,A>, A) (<38,0,B>, A) (<38,0,C>, A + C)
(<39,0,A>, A) (<39,0,B>, A) (<39,0,C>, A + C)
(<40,0,A>, A) (<40,0,B>, A) (<40,0,C>, A + C)
(<41,0,A>, A) (<41,0,B>, A) (<41,0,C>, A + C)
(<42,0,A>, A) (<42,0,B>, A) (<42,0,C>, A + C)
(<43,0,A>, A) (<43,0,B>, A) (<43,0,C>, A + C)
+ Applied Processor:
ChainProcessor False [28,34,36,37,38,39,40,41,42,43]
+ Details:
We chained rule 34 to obtain the rules [44,45,46] .
* Step 28: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
36. o0(A,B,C) -> c2(o2(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E] (?,5)
37. o1(A,B,C) -> c2(n5(A,0,C),o2(A,0,C)) [A >= 0] (2,3)
38. o2(A,B,C) -> n8(A,B,C) [A >= B] (?,2)
39. o2(A,B,C) -> n9(A,B,C) [A >= B] (?,2)
40. o2(A,B,C) -> o0(A,B,C) [A >= B] (?,2)
41. n8(A,B,C) -> c2(n8(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
42. n8(A,B,C) -> c2(n9(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
43. n8(A,B,C) -> c2(o0(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
44. n9(A,B,C) -> c2(n8(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
45. n9(A,B,C) -> c2(n9(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
46. n9(A,B,C) -> c2(o0(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[28->{37},36->{38,39,40},37->{38,39,40},38->{41,42,43},39->{44,45,46},40->{36},41->{41,42,43},42->{44,45
,46},43->{36},44->{41,42,43},45->{44,45,46},46->{36}]
Sizebounds:
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<36,0,A>, A) (<36,0,B>, 3 + A) (<36,0,C>, A + C)
(<37,0,A>, A) (<37,0,B>, 3 + A) (<37,0,C>, A + C)
(<38,0,A>, A) (<38,0,B>, A) (<38,0,C>, A + C)
(<39,0,A>, A) (<39,0,B>, A) (<39,0,C>, A + C)
(<40,0,A>, A) (<40,0,B>, A) (<40,0,C>, A + C)
(<41,0,A>, A) (<41,0,B>, A) (<41,0,C>, A + C)
(<42,0,A>, A) (<42,0,B>, A) (<42,0,C>, A + C)
(<43,0,A>, A) (<43,0,B>, A) (<43,0,C>, A + C)
(<44,0,A>, A) (<44,0,B>, A) (<44,0,C>, A + C)
(<45,0,A>, A) (<45,0,B>, A) (<45,0,C>, A + C)
(<46,0,A>, A) (<46,0,B>, A) (<46,0,C>, A + C)
+ Applied Processor:
ChainProcessor False [28,36,37,38,39,40,41,42,43,44,45,46]
+ Details:
We chained rule 36 to obtain the rules [47,48,49] .
* Step 29: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
37. o1(A,B,C) -> c2(n5(A,0,C),o2(A,0,C)) [A >= 0] (2,3)
38. o2(A,B,C) -> n8(A,B,C) [A >= B] (?,2)
39. o2(A,B,C) -> n9(A,B,C) [A >= B] (?,2)
40. o2(A,B,C) -> o0(A,B,C) [A >= B] (?,2)
41. n8(A,B,C) -> c2(n8(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
42. n8(A,B,C) -> c2(n9(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
43. n8(A,B,C) -> c2(o0(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
44. n9(A,B,C) -> c2(n8(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
45. n9(A,B,C) -> c2(n9(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
46. n9(A,B,C) -> c2(o0(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
47. o0(A,B,C) -> c2(n8(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
48. o0(A,B,C) -> c2(n9(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
49. o0(A,B,C) -> c2(o0(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[28->{37},37->{38,39,40},38->{41,42,43},39->{44,45,46},40->{47,48,49},41->{41,42,43},42->{44,45,46}
,43->{47,48,49},44->{41,42,43},45->{44,45,46},46->{47,48,49},47->{41,42,43},48->{44,45,46},49->{47,48,49}]
Sizebounds:
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<37,0,A>, A) (<37,0,B>, 3 + A) (<37,0,C>, A + C)
(<38,0,A>, A) (<38,0,B>, A) (<38,0,C>, A + C)
(<39,0,A>, A) (<39,0,B>, A) (<39,0,C>, A + C)
(<40,0,A>, A) (<40,0,B>, A) (<40,0,C>, A + C)
(<41,0,A>, A) (<41,0,B>, A) (<41,0,C>, A + C)
(<42,0,A>, A) (<42,0,B>, A) (<42,0,C>, A + C)
(<43,0,A>, A) (<43,0,B>, A) (<43,0,C>, A + C)
(<44,0,A>, A) (<44,0,B>, A) (<44,0,C>, A + C)
(<45,0,A>, A) (<45,0,B>, A) (<45,0,C>, A + C)
(<46,0,A>, A) (<46,0,B>, A) (<46,0,C>, A + C)
(<47,0,A>, A) (<47,0,B>, A) (<47,0,C>, A + C)
(<48,0,A>, A) (<48,0,B>, A) (<48,0,C>, A + C)
(<49,0,A>, A) (<49,0,B>, A) (<49,0,C>, A + C)
+ Applied Processor:
ChainProcessor False [28,37,38,39,40,41,42,43,44,45,46,47,48,49]
+ Details:
We chained rule 37 to obtain the rules [50,51,52] .
* Step 30: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
38. o2(A,B,C) -> n8(A,B,C) [A >= B] (?,2)
39. o2(A,B,C) -> n9(A,B,C) [A >= B] (?,2)
40. o2(A,B,C) -> o0(A,B,C) [A >= B] (?,2)
41. n8(A,B,C) -> c2(n8(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
42. n8(A,B,C) -> c2(n9(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
43. n8(A,B,C) -> c2(o0(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
44. n9(A,B,C) -> c2(n8(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
45. n9(A,B,C) -> c2(n9(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
46. n9(A,B,C) -> c2(o0(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
47. o0(A,B,C) -> c2(n8(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
48. o0(A,B,C) -> c2(n9(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
49. o0(A,B,C) -> c2(o0(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
50. o1(A,B,C) -> c2(n5(A,0,C),n8(A,0,C)) [A >= 0 && A >= 0] (2,5)
51. o1(A,B,C) -> c2(n5(A,0,C),n9(A,0,C)) [A >= 0 && A >= 0] (2,5)
52. o1(A,B,C) -> c2(n5(A,0,C),o0(A,0,C)) [A >= 0 && A >= 0] (2,5)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[28->{50,51,52},38->{41,42,43},39->{44,45,46},40->{47,48,49},41->{41,42,43},42->{44,45,46},43->{47,48,49}
,44->{41,42,43},45->{44,45,46},46->{47,48,49},47->{41,42,43},48->{44,45,46},49->{47,48,49},50->{41,42,43}
,51->{44,45,46},52->{47,48,49}]
Sizebounds:
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<38,0,A>, A) (<38,0,B>, A) (<38,0,C>, A + C)
(<39,0,A>, A) (<39,0,B>, A) (<39,0,C>, A + C)
(<40,0,A>, A) (<40,0,B>, A) (<40,0,C>, A + C)
(<41,0,A>, A) (<41,0,B>, A) (<41,0,C>, A + C)
(<42,0,A>, A) (<42,0,B>, A) (<42,0,C>, A + C)
(<43,0,A>, A) (<43,0,B>, A) (<43,0,C>, A + C)
(<44,0,A>, A) (<44,0,B>, A) (<44,0,C>, A + C)
(<45,0,A>, A) (<45,0,B>, A) (<45,0,C>, A + C)
(<46,0,A>, A) (<46,0,B>, A) (<46,0,C>, A + C)
(<47,0,A>, A) (<47,0,B>, A) (<47,0,C>, A + C)
(<48,0,A>, A) (<48,0,B>, A) (<48,0,C>, A + C)
(<49,0,A>, A) (<49,0,B>, A) (<49,0,C>, A + C)
(<50,0,A>, A) (<50,0,B>, A) (<50,0,C>, A + C)
(<51,0,A>, A) (<51,0,B>, A) (<51,0,C>, A + C)
(<52,0,A>, A) (<52,0,B>, A) (<52,0,C>, A + C)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [38,39,40]
* Step 31: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
41. n8(A,B,C) -> c2(n8(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
42. n8(A,B,C) -> c2(n9(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
43. n8(A,B,C) -> c2(o0(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
44. n9(A,B,C) -> c2(n8(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
45. n9(A,B,C) -> c2(n9(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
46. n9(A,B,C) -> c2(o0(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
47. o0(A,B,C) -> c2(n8(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
48. o0(A,B,C) -> c2(n9(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
49. o0(A,B,C) -> c2(o0(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
50. o1(A,B,C) -> c2(n5(A,0,C),n8(A,0,C)) [A >= 0 && A >= 0] (2,5)
51. o1(A,B,C) -> c2(n5(A,0,C),n9(A,0,C)) [A >= 0 && A >= 0] (2,5)
52. o1(A,B,C) -> c2(n5(A,0,C),o0(A,0,C)) [A >= 0 && A >= 0] (2,5)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[28->{50,51,52},41->{41,42,43},42->{44,45,46},43->{47,48,49},44->{41,42,43},45->{44,45,46},46->{47,48,49}
,47->{41,42,43},48->{44,45,46},49->{47,48,49},50->{41,42,43},51->{44,45,46},52->{47,48,49}]
Sizebounds:
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<41,0,A>, A) (<41,0,B>, A) (<41,0,C>, A + C)
(<42,0,A>, A) (<42,0,B>, A) (<42,0,C>, A + C)
(<43,0,A>, A) (<43,0,B>, A) (<43,0,C>, A + C)
(<44,0,A>, A) (<44,0,B>, A) (<44,0,C>, A + C)
(<45,0,A>, A) (<45,0,B>, A) (<45,0,C>, A + C)
(<46,0,A>, A) (<46,0,B>, A) (<46,0,C>, A + C)
(<47,0,A>, A) (<47,0,B>, A) (<47,0,C>, A + C)
(<48,0,A>, A) (<48,0,B>, A) (<48,0,C>, A + C)
(<49,0,A>, A) (<49,0,B>, A) (<49,0,C>, A + C)
(<50,0,A>, A) (<50,0,B>, A) (<50,0,C>, A + C)
(<51,0,A>, A) (<51,0,B>, A) (<51,0,C>, A + C)
(<52,0,A>, A) (<52,0,B>, A) (<52,0,C>, A + C)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<28,0,A>, A, .= 0) (<28,0,B>, B, .= 0) (<28,0,C>, C, .= 0)
(<41,0,A>, A, .= 0) (<41,0,B>, 1 + A + B, .* 1) (<41,0,C>, B, .= 0)
(<41,1,A>, A, .= 0) (<41,1,B>, 1 + A + B, .* 1) (<41,1,C>, B, .= 0)
(<42,0,A>, A, .= 0) (<42,0,B>, 1 + A + B, .* 1) (<42,0,C>, B, .= 0)
(<42,1,A>, A, .= 0) (<42,1,B>, 1 + A + B, .* 1) (<42,1,C>, B, .= 0)
(<43,0,A>, A, .= 0) (<43,0,B>, 1 + A + B, .* 1) (<43,0,C>, B, .= 0)
(<43,1,A>, A, .= 0) (<43,1,B>, 1 + A + B, .* 1) (<43,1,C>, B, .= 0)
(<44,0,A>, A, .= 0) (<44,0,B>, 2 + A + B, .* 2) (<44,0,C>, B, .= 0)
(<44,1,A>, A, .= 0) (<44,1,B>, 2 + A + B, .* 2) (<44,1,C>, B, .= 0)
(<45,0,A>, A, .= 0) (<45,0,B>, 2 + A + B, .* 2) (<45,0,C>, B, .= 0)
(<45,1,A>, A, .= 0) (<45,1,B>, 2 + A + B, .* 2) (<45,1,C>, B, .= 0)
(<46,0,A>, A, .= 0) (<46,0,B>, 2 + A + B, .* 2) (<46,0,C>, B, .= 0)
(<46,1,A>, A, .= 0) (<46,1,B>, 2 + A + B, .* 2) (<46,1,C>, B, .= 0)
(<47,0,A>, A, .= 0) (<47,0,B>, 3 + A + B, .* 3) (<47,0,C>, B, .= 0)
(<47,1,A>, A, .= 0) (<47,1,B>, 3 + A + B, .* 3) (<47,1,C>, B, .= 0)
(<48,0,A>, A, .= 0) (<48,0,B>, 3 + A + B, .* 3) (<48,0,C>, B, .= 0)
(<48,1,A>, A, .= 0) (<48,1,B>, 3 + A + B, .* 3) (<48,1,C>, B, .= 0)
(<49,0,A>, A, .= 0) (<49,0,B>, 3 + A + B, .* 3) (<49,0,C>, B, .= 0)
(<49,1,A>, A, .= 0) (<49,1,B>, 3 + A + B, .* 3) (<49,1,C>, B, .= 0)
(<50,0,A>, A, .= 0) (<50,0,B>, 0, .= 0) (<50,0,C>, C, .= 0)
(<50,1,A>, A, .= 0) (<50,1,B>, 0, .= 0) (<50,1,C>, C, .= 0)
(<51,0,A>, A, .= 0) (<51,0,B>, 0, .= 0) (<51,0,C>, C, .= 0)
(<51,1,A>, A, .= 0) (<51,1,B>, 0, .= 0) (<51,1,C>, C, .= 0)
(<52,0,A>, A, .= 0) (<52,0,B>, 0, .= 0) (<52,0,C>, C, .= 0)
(<52,1,A>, A, .= 0) (<52,1,B>, 0, .= 0) (<52,1,C>, C, .= 0)
* Step 32: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
41. n8(A,B,C) -> c2(n8(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
42. n8(A,B,C) -> c2(n9(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
43. n8(A,B,C) -> c2(o0(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
44. n9(A,B,C) -> c2(n8(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
45. n9(A,B,C) -> c2(n9(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
46. n9(A,B,C) -> c2(o0(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
47. o0(A,B,C) -> c2(n8(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
48. o0(A,B,C) -> c2(n9(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
49. o0(A,B,C) -> c2(o0(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
50. o1(A,B,C) -> c2(n5(A,0,C),n8(A,0,C)) [A >= 0 && A >= 0] (2,5)
51. o1(A,B,C) -> c2(n5(A,0,C),n9(A,0,C)) [A >= 0 && A >= 0] (2,5)
52. o1(A,B,C) -> c2(n5(A,0,C),o0(A,0,C)) [A >= 0 && A >= 0] (2,5)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[28->{50,51,52},41->{41,42,43},42->{44,45,46},43->{47,48,49},44->{41,42,43},45->{44,45,46},46->{47,48,49}
,47->{41,42,43},48->{44,45,46},49->{47,48,49},50->{41,42,43},51->{44,45,46},52->{47,48,49}]
Sizebounds:
(<28,0,A>, ?) (<28,0,B>, ?) (<28,0,C>, ?)
(<41,0,A>, ?) (<41,0,B>, ?) (<41,0,C>, ?)
(<41,1,A>, ?) (<41,1,B>, ?) (<41,1,C>, ?)
(<42,0,A>, ?) (<42,0,B>, ?) (<42,0,C>, ?)
(<42,1,A>, ?) (<42,1,B>, ?) (<42,1,C>, ?)
(<43,0,A>, ?) (<43,0,B>, ?) (<43,0,C>, ?)
(<43,1,A>, ?) (<43,1,B>, ?) (<43,1,C>, ?)
(<44,0,A>, ?) (<44,0,B>, ?) (<44,0,C>, ?)
(<44,1,A>, ?) (<44,1,B>, ?) (<44,1,C>, ?)
(<45,0,A>, ?) (<45,0,B>, ?) (<45,0,C>, ?)
(<45,1,A>, ?) (<45,1,B>, ?) (<45,1,C>, ?)
(<46,0,A>, ?) (<46,0,B>, ?) (<46,0,C>, ?)
(<46,1,A>, ?) (<46,1,B>, ?) (<46,1,C>, ?)
(<47,0,A>, ?) (<47,0,B>, ?) (<47,0,C>, ?)
(<47,1,A>, ?) (<47,1,B>, ?) (<47,1,C>, ?)
(<48,0,A>, ?) (<48,0,B>, ?) (<48,0,C>, ?)
(<48,1,A>, ?) (<48,1,B>, ?) (<48,1,C>, ?)
(<49,0,A>, ?) (<49,0,B>, ?) (<49,0,C>, ?)
(<49,1,A>, ?) (<49,1,B>, ?) (<49,1,C>, ?)
(<50,0,A>, ?) (<50,0,B>, ?) (<50,0,C>, ?)
(<50,1,A>, ?) (<50,1,B>, ?) (<50,1,C>, ?)
(<51,0,A>, ?) (<51,0,B>, ?) (<51,0,C>, ?)
(<51,1,A>, ?) (<51,1,B>, ?) (<51,1,C>, ?)
(<52,0,A>, ?) (<52,0,B>, ?) (<52,0,C>, ?)
(<52,1,A>, ?) (<52,1,B>, ?) (<52,1,C>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<41,0,A>, A) (<41,0,B>, ?) (<41,0,C>, ?)
(<41,1,A>, A) (<41,1,B>, ?) (<41,1,C>, ?)
(<42,0,A>, A) (<42,0,B>, ?) (<42,0,C>, ?)
(<42,1,A>, A) (<42,1,B>, ?) (<42,1,C>, ?)
(<43,0,A>, A) (<43,0,B>, ?) (<43,0,C>, ?)
(<43,1,A>, A) (<43,1,B>, ?) (<43,1,C>, ?)
(<44,0,A>, A) (<44,0,B>, ?) (<44,0,C>, ?)
(<44,1,A>, A) (<44,1,B>, ?) (<44,1,C>, ?)
(<45,0,A>, A) (<45,0,B>, ?) (<45,0,C>, ?)
(<45,1,A>, A) (<45,1,B>, ?) (<45,1,C>, ?)
(<46,0,A>, A) (<46,0,B>, ?) (<46,0,C>, ?)
(<46,1,A>, A) (<46,1,B>, ?) (<46,1,C>, ?)
(<47,0,A>, A) (<47,0,B>, ?) (<47,0,C>, ?)
(<47,1,A>, A) (<47,1,B>, ?) (<47,1,C>, ?)
(<48,0,A>, A) (<48,0,B>, ?) (<48,0,C>, ?)
(<48,1,A>, A) (<48,1,B>, ?) (<48,1,C>, ?)
(<49,0,A>, A) (<49,0,B>, ?) (<49,0,C>, ?)
(<49,1,A>, A) (<49,1,B>, ?) (<49,1,C>, ?)
(<50,0,A>, A) (<50,0,B>, 0) (<50,0,C>, C)
(<50,1,A>, A) (<50,1,B>, 0) (<50,1,C>, C)
(<51,0,A>, A) (<51,0,B>, 0) (<51,0,C>, C)
(<51,1,A>, A) (<51,1,B>, 0) (<51,1,C>, C)
(<52,0,A>, A) (<52,0,B>, 0) (<52,0,C>, C)
(<52,1,A>, A) (<52,1,B>, 0) (<52,1,C>, C)
* Step 33: LocationConstraintsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
41. n8(A,B,C) -> c2(n8(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
42. n8(A,B,C) -> c2(n9(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
43. n8(A,B,C) -> c2(o0(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
44. n9(A,B,C) -> c2(n8(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
45. n9(A,B,C) -> c2(n9(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
46. n9(A,B,C) -> c2(o0(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
47. o0(A,B,C) -> c2(n8(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
48. o0(A,B,C) -> c2(n9(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
49. o0(A,B,C) -> c2(o0(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
50. o1(A,B,C) -> c2(n5(A,0,C),n8(A,0,C)) [A >= 0 && A >= 0] (2,5)
51. o1(A,B,C) -> c2(n5(A,0,C),n9(A,0,C)) [A >= 0 && A >= 0] (2,5)
52. o1(A,B,C) -> c2(n5(A,0,C),o0(A,0,C)) [A >= 0 && A >= 0] (2,5)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[28->{50,51,52},41->{41,42,43},42->{44,45,46},43->{47,48,49},44->{41,42,43},45->{44,45,46},46->{47,48,49}
,47->{41,42,43},48->{44,45,46},49->{47,48,49},50->{41,42,43},51->{44,45,46},52->{47,48,49}]
Sizebounds:
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<41,0,A>, A) (<41,0,B>, ?) (<41,0,C>, ?)
(<41,1,A>, A) (<41,1,B>, ?) (<41,1,C>, ?)
(<42,0,A>, A) (<42,0,B>, ?) (<42,0,C>, ?)
(<42,1,A>, A) (<42,1,B>, ?) (<42,1,C>, ?)
(<43,0,A>, A) (<43,0,B>, ?) (<43,0,C>, ?)
(<43,1,A>, A) (<43,1,B>, ?) (<43,1,C>, ?)
(<44,0,A>, A) (<44,0,B>, ?) (<44,0,C>, ?)
(<44,1,A>, A) (<44,1,B>, ?) (<44,1,C>, ?)
(<45,0,A>, A) (<45,0,B>, ?) (<45,0,C>, ?)
(<45,1,A>, A) (<45,1,B>, ?) (<45,1,C>, ?)
(<46,0,A>, A) (<46,0,B>, ?) (<46,0,C>, ?)
(<46,1,A>, A) (<46,1,B>, ?) (<46,1,C>, ?)
(<47,0,A>, A) (<47,0,B>, ?) (<47,0,C>, ?)
(<47,1,A>, A) (<47,1,B>, ?) (<47,1,C>, ?)
(<48,0,A>, A) (<48,0,B>, ?) (<48,0,C>, ?)
(<48,1,A>, A) (<48,1,B>, ?) (<48,1,C>, ?)
(<49,0,A>, A) (<49,0,B>, ?) (<49,0,C>, ?)
(<49,1,A>, A) (<49,1,B>, ?) (<49,1,C>, ?)
(<50,0,A>, A) (<50,0,B>, 0) (<50,0,C>, C)
(<50,1,A>, A) (<50,1,B>, 0) (<50,1,C>, C)
(<51,0,A>, A) (<51,0,B>, 0) (<51,0,C>, C)
(<51,1,A>, A) (<51,1,B>, 0) (<51,1,C>, C)
(<52,0,A>, A) (<52,0,B>, 0) (<52,0,C>, C)
(<52,1,A>, A) (<52,1,B>, 0) (<52,1,C>, C)
+ Applied Processor:
LocationConstraintsProc
+ Details:
We computed the location constraints 28 : True 41 : True 42 : True 43 : True 44 : True 45 : True 46 : True 47 : True 48 : True 49 : True 50 : [A >= 0] 51 : [A >= 0] 52 : [A >= 0] .
* Step 34: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
41. n8(A,B,C) -> c2(n8(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
42. n8(A,B,C) -> c2(n9(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
43. n8(A,B,C) -> c2(o0(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
44. n9(A,B,C) -> c2(n8(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
45. n9(A,B,C) -> c2(n9(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
46. n9(A,B,C) -> c2(o0(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
47. o0(A,B,C) -> c2(n8(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
48. o0(A,B,C) -> c2(n9(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
49. o0(A,B,C) -> c2(o0(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
50. o1(A,B,C) -> c2(n5(A,0,C),n8(A,0,C)) [A >= 0 && A >= 0] (2,5)
51. o1(A,B,C) -> c2(n5(A,0,C),n9(A,0,C)) [A >= 0 && A >= 0] (2,5)
52. o1(A,B,C) -> c2(n5(A,0,C),o0(A,0,C)) [A >= 0 && A >= 0] (2,5)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[28->{50,51,52},41->{41,42,43},42->{44,45,46},43->{47,48,49},44->{41,42,43},45->{44,45,46},46->{47,48,49}
,47->{41,42,43},48->{44,45,46},49->{47,48,49},50->{41,42,43},51->{44,45,46},52->{47,48,49}]
Sizebounds:
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<41,0,A>, A) (<41,0,B>, ?) (<41,0,C>, ?)
(<41,1,A>, A) (<41,1,B>, ?) (<41,1,C>, ?)
(<42,0,A>, A) (<42,0,B>, ?) (<42,0,C>, ?)
(<42,1,A>, A) (<42,1,B>, ?) (<42,1,C>, ?)
(<43,0,A>, A) (<43,0,B>, ?) (<43,0,C>, ?)
(<43,1,A>, A) (<43,1,B>, ?) (<43,1,C>, ?)
(<44,0,A>, A) (<44,0,B>, ?) (<44,0,C>, ?)
(<44,1,A>, A) (<44,1,B>, ?) (<44,1,C>, ?)
(<45,0,A>, A) (<45,0,B>, ?) (<45,0,C>, ?)
(<45,1,A>, A) (<45,1,B>, ?) (<45,1,C>, ?)
(<46,0,A>, A) (<46,0,B>, ?) (<46,0,C>, ?)
(<46,1,A>, A) (<46,1,B>, ?) (<46,1,C>, ?)
(<47,0,A>, A) (<47,0,B>, ?) (<47,0,C>, ?)
(<47,1,A>, A) (<47,1,B>, ?) (<47,1,C>, ?)
(<48,0,A>, A) (<48,0,B>, ?) (<48,0,C>, ?)
(<48,1,A>, A) (<48,1,B>, ?) (<48,1,C>, ?)
(<49,0,A>, A) (<49,0,B>, ?) (<49,0,C>, ?)
(<49,1,A>, A) (<49,1,B>, ?) (<49,1,C>, ?)
(<50,0,A>, A) (<50,0,B>, 0) (<50,0,C>, C)
(<50,1,A>, A) (<50,1,B>, 0) (<50,1,C>, C)
(<51,0,A>, A) (<51,0,B>, 0) (<51,0,C>, C)
(<51,1,A>, A) (<51,1,B>, 0) (<51,1,C>, C)
(<52,0,A>, A) (<52,0,B>, 0) (<52,0,C>, C)
(<52,1,A>, A) (<52,1,B>, 0) (<52,1,C>, C)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(add) = 2*x1
p(n5) = 0
p(n8) = 2*x1 + -2*x2
p(n81) = 0
p(n9) = 2*x1 + -2*x2
p(n91) = 0
p(o0) = 2*x1 + -2*x2
p(o01) = 0
p(o1) = 2*x1
The following rules are strictly oriented:
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 2*A + -2*B
> 2*A + -2*E
= c2(o0(A,E,B),o01(A,E,B))
The following rules are weakly oriented:
[A >= 0 && A >= 0] ==>
add(A,B,C) = 2*A
>= 2*A
= o1(A,B,C)
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 2*A + -2*B
>= 2*A + -2*E
= c2(n8(A,E,B),n81(A,E,B))
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 2*A + -2*B
>= 2*A + -2*E
= c2(n9(A,E,B),n81(A,E,B))
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 2*A + -2*B
>= 2*A + -2*E
= c2(o0(A,E,B),n81(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 2*A + -2*B
>= 2*A + -2*E
= c2(n8(A,E,B),n91(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 2*A + -2*B
>= 2*A + -2*E
= c2(n9(A,E,B),n91(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 2*A + -2*B
>= 2*A + -2*E
= c2(o0(A,E,B),n91(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 2*A + -2*B
>= 2*A + -2*E
= c2(n8(A,E,B),o01(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 2*A + -2*B
>= 2*A + -2*E
= c2(n9(A,E,B),o01(A,E,B))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 2*A
>= 2*A
= c2(n5(A,0,C),n8(A,0,C))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 2*A
>= 2*A
= c2(n5(A,0,C),n9(A,0,C))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 2*A
>= 2*A
= c2(n5(A,0,C),o0(A,0,C))
* Step 35: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
41. n8(A,B,C) -> c2(n8(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
42. n8(A,B,C) -> c2(n9(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
43. n8(A,B,C) -> c2(o0(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
44. n9(A,B,C) -> c2(n8(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
45. n9(A,B,C) -> c2(n9(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
46. n9(A,B,C) -> c2(o0(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
47. o0(A,B,C) -> c2(n8(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
48. o0(A,B,C) -> c2(n9(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
49. o0(A,B,C) -> c2(o0(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
50. o1(A,B,C) -> c2(n5(A,0,C),n8(A,0,C)) [A >= 0 && A >= 0] (2,5)
51. o1(A,B,C) -> c2(n5(A,0,C),n9(A,0,C)) [A >= 0 && A >= 0] (2,5)
52. o1(A,B,C) -> c2(n5(A,0,C),o0(A,0,C)) [A >= 0 && A >= 0] (2,5)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[28->{50,51,52},41->{41,42,43},42->{44,45,46},43->{47,48,49},44->{41,42,43},45->{44,45,46},46->{47,48,49}
,47->{41,42,43},48->{44,45,46},49->{47,48,49},50->{41,42,43},51->{44,45,46},52->{47,48,49}]
Sizebounds:
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<41,0,A>, A) (<41,0,B>, ?) (<41,0,C>, ?)
(<41,1,A>, A) (<41,1,B>, ?) (<41,1,C>, ?)
(<42,0,A>, A) (<42,0,B>, ?) (<42,0,C>, ?)
(<42,1,A>, A) (<42,1,B>, ?) (<42,1,C>, ?)
(<43,0,A>, A) (<43,0,B>, ?) (<43,0,C>, ?)
(<43,1,A>, A) (<43,1,B>, ?) (<43,1,C>, ?)
(<44,0,A>, A) (<44,0,B>, ?) (<44,0,C>, ?)
(<44,1,A>, A) (<44,1,B>, ?) (<44,1,C>, ?)
(<45,0,A>, A) (<45,0,B>, ?) (<45,0,C>, ?)
(<45,1,A>, A) (<45,1,B>, ?) (<45,1,C>, ?)
(<46,0,A>, A) (<46,0,B>, ?) (<46,0,C>, ?)
(<46,1,A>, A) (<46,1,B>, ?) (<46,1,C>, ?)
(<47,0,A>, A) (<47,0,B>, ?) (<47,0,C>, ?)
(<47,1,A>, A) (<47,1,B>, ?) (<47,1,C>, ?)
(<48,0,A>, A) (<48,0,B>, ?) (<48,0,C>, ?)
(<48,1,A>, A) (<48,1,B>, ?) (<48,1,C>, ?)
(<49,0,A>, A) (<49,0,B>, ?) (<49,0,C>, ?)
(<49,1,A>, A) (<49,1,B>, ?) (<49,1,C>, ?)
(<50,0,A>, A) (<50,0,B>, 0) (<50,0,C>, C)
(<50,1,A>, A) (<50,1,B>, 0) (<50,1,C>, C)
(<51,0,A>, A) (<51,0,B>, 0) (<51,0,C>, C)
(<51,1,A>, A) (<51,1,B>, 0) (<51,1,C>, C)
(<52,0,A>, A) (<52,0,B>, 0) (<52,0,C>, C)
(<52,1,A>, A) (<52,1,B>, 0) (<52,1,C>, C)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(add) = 2*x1
p(n5) = 0
p(n8) = 2*x1 + -2*x2
p(n81) = 0
p(n9) = 2*x1 + -2*x2
p(n91) = 0
p(o0) = 2*x1 + -2*x2
p(o01) = 0
p(o1) = 2*x1
The following rules are strictly oriented:
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 2*A + -2*B
> 2*A + -2*E
= c2(n9(A,E,B),o01(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 2*A + -2*B
> 2*A + -2*E
= c2(o0(A,E,B),o01(A,E,B))
The following rules are weakly oriented:
[A >= 0 && A >= 0] ==>
add(A,B,C) = 2*A
>= 2*A
= o1(A,B,C)
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 2*A + -2*B
>= 2*A + -2*E
= c2(n8(A,E,B),n81(A,E,B))
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 2*A + -2*B
>= 2*A + -2*E
= c2(n9(A,E,B),n81(A,E,B))
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 2*A + -2*B
>= 2*A + -2*E
= c2(o0(A,E,B),n81(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 2*A + -2*B
>= 2*A + -2*E
= c2(n8(A,E,B),n91(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 2*A + -2*B
>= 2*A + -2*E
= c2(n9(A,E,B),n91(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 2*A + -2*B
>= 2*A + -2*E
= c2(o0(A,E,B),n91(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 2*A + -2*B
>= 2*A + -2*E
= c2(n8(A,E,B),o01(A,E,B))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 2*A
>= 2*A
= c2(n5(A,0,C),n8(A,0,C))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 2*A
>= 2*A
= c2(n5(A,0,C),n9(A,0,C))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 2*A
>= 2*A
= c2(n5(A,0,C),o0(A,0,C))
* Step 36: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
41. n8(A,B,C) -> c2(n8(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
42. n8(A,B,C) -> c2(n9(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
43. n8(A,B,C) -> c2(o0(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
44. n9(A,B,C) -> c2(n8(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
45. n9(A,B,C) -> c2(n9(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
46. n9(A,B,C) -> c2(o0(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
47. o0(A,B,C) -> c2(n8(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (?,7)
48. o0(A,B,C) -> c2(n9(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
49. o0(A,B,C) -> c2(o0(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
50. o1(A,B,C) -> c2(n5(A,0,C),n8(A,0,C)) [A >= 0 && A >= 0] (2,5)
51. o1(A,B,C) -> c2(n5(A,0,C),n9(A,0,C)) [A >= 0 && A >= 0] (2,5)
52. o1(A,B,C) -> c2(n5(A,0,C),o0(A,0,C)) [A >= 0 && A >= 0] (2,5)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[28->{50,51,52},41->{41,42,43},42->{44,45,46},43->{47,48,49},44->{41,42,43},45->{44,45,46},46->{47,48,49}
,47->{41,42,43},48->{44,45,46},49->{47,48,49},50->{41,42,43},51->{44,45,46},52->{47,48,49}]
Sizebounds:
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<41,0,A>, A) (<41,0,B>, ?) (<41,0,C>, ?)
(<41,1,A>, A) (<41,1,B>, ?) (<41,1,C>, ?)
(<42,0,A>, A) (<42,0,B>, ?) (<42,0,C>, ?)
(<42,1,A>, A) (<42,1,B>, ?) (<42,1,C>, ?)
(<43,0,A>, A) (<43,0,B>, ?) (<43,0,C>, ?)
(<43,1,A>, A) (<43,1,B>, ?) (<43,1,C>, ?)
(<44,0,A>, A) (<44,0,B>, ?) (<44,0,C>, ?)
(<44,1,A>, A) (<44,1,B>, ?) (<44,1,C>, ?)
(<45,0,A>, A) (<45,0,B>, ?) (<45,0,C>, ?)
(<45,1,A>, A) (<45,1,B>, ?) (<45,1,C>, ?)
(<46,0,A>, A) (<46,0,B>, ?) (<46,0,C>, ?)
(<46,1,A>, A) (<46,1,B>, ?) (<46,1,C>, ?)
(<47,0,A>, A) (<47,0,B>, ?) (<47,0,C>, ?)
(<47,1,A>, A) (<47,1,B>, ?) (<47,1,C>, ?)
(<48,0,A>, A) (<48,0,B>, ?) (<48,0,C>, ?)
(<48,1,A>, A) (<48,1,B>, ?) (<48,1,C>, ?)
(<49,0,A>, A) (<49,0,B>, ?) (<49,0,C>, ?)
(<49,1,A>, A) (<49,1,B>, ?) (<49,1,C>, ?)
(<50,0,A>, A) (<50,0,B>, 0) (<50,0,C>, C)
(<50,1,A>, A) (<50,1,B>, 0) (<50,1,C>, C)
(<51,0,A>, A) (<51,0,B>, 0) (<51,0,C>, C)
(<51,1,A>, A) (<51,1,B>, 0) (<51,1,C>, C)
(<52,0,A>, A) (<52,0,B>, 0) (<52,0,C>, C)
(<52,1,A>, A) (<52,1,B>, 0) (<52,1,C>, C)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(add) = 3*x1
p(n5) = 0
p(n8) = 3*x1 + -3*x2
p(n81) = 0
p(n9) = 3*x1 + -3*x2
p(n91) = 0
p(o0) = 3*x1 + -3*x2
p(o01) = 0
p(o1) = 3*x1
The following rules are strictly oriented:
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 3*A + -3*B
> 3*A + -3*E
= c2(n8(A,E,B),o01(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 3*A + -3*B
> 3*A + -3*E
= c2(n9(A,E,B),o01(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 3*A + -3*B
> 3*A + -3*E
= c2(o0(A,E,B),o01(A,E,B))
The following rules are weakly oriented:
[A >= 0 && A >= 0] ==>
add(A,B,C) = 3*A
>= 3*A
= o1(A,B,C)
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 3*A + -3*B
>= 3*A + -3*E
= c2(n8(A,E,B),n81(A,E,B))
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 3*A + -3*B
>= 3*A + -3*E
= c2(n9(A,E,B),n81(A,E,B))
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 3*A + -3*B
>= 3*A + -3*E
= c2(o0(A,E,B),n81(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 3*A + -3*B
>= 3*A + -3*E
= c2(n8(A,E,B),n91(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 3*A + -3*B
>= 3*A + -3*E
= c2(n9(A,E,B),n91(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 3*A + -3*B
>= 3*A + -3*E
= c2(o0(A,E,B),n91(A,E,B))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 3*A
>= 3*A
= c2(n5(A,0,C),n8(A,0,C))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 3*A
>= 3*A
= c2(n5(A,0,C),n9(A,0,C))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 3*A
>= 3*A
= c2(n5(A,0,C),o0(A,0,C))
* Step 37: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
41. n8(A,B,C) -> c2(n8(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
42. n8(A,B,C) -> c2(n9(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
43. n8(A,B,C) -> c2(o0(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
44. n9(A,B,C) -> c2(n8(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
45. n9(A,B,C) -> c2(n9(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
46. n9(A,B,C) -> c2(o0(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
47. o0(A,B,C) -> c2(n8(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (3*A,7)
48. o0(A,B,C) -> c2(n9(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
49. o0(A,B,C) -> c2(o0(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
50. o1(A,B,C) -> c2(n5(A,0,C),n8(A,0,C)) [A >= 0 && A >= 0] (2,5)
51. o1(A,B,C) -> c2(n5(A,0,C),n9(A,0,C)) [A >= 0 && A >= 0] (2,5)
52. o1(A,B,C) -> c2(n5(A,0,C),o0(A,0,C)) [A >= 0 && A >= 0] (2,5)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[28->{50,51,52},41->{41,42,43},42->{44,45,46},43->{47,48,49},44->{41,42,43},45->{44,45,46},46->{47,48,49}
,47->{41,42,43},48->{44,45,46},49->{47,48,49},50->{41,42,43},51->{44,45,46},52->{47,48,49}]
Sizebounds:
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<41,0,A>, A) (<41,0,B>, ?) (<41,0,C>, ?)
(<41,1,A>, A) (<41,1,B>, ?) (<41,1,C>, ?)
(<42,0,A>, A) (<42,0,B>, ?) (<42,0,C>, ?)
(<42,1,A>, A) (<42,1,B>, ?) (<42,1,C>, ?)
(<43,0,A>, A) (<43,0,B>, ?) (<43,0,C>, ?)
(<43,1,A>, A) (<43,1,B>, ?) (<43,1,C>, ?)
(<44,0,A>, A) (<44,0,B>, ?) (<44,0,C>, ?)
(<44,1,A>, A) (<44,1,B>, ?) (<44,1,C>, ?)
(<45,0,A>, A) (<45,0,B>, ?) (<45,0,C>, ?)
(<45,1,A>, A) (<45,1,B>, ?) (<45,1,C>, ?)
(<46,0,A>, A) (<46,0,B>, ?) (<46,0,C>, ?)
(<46,1,A>, A) (<46,1,B>, ?) (<46,1,C>, ?)
(<47,0,A>, A) (<47,0,B>, ?) (<47,0,C>, ?)
(<47,1,A>, A) (<47,1,B>, ?) (<47,1,C>, ?)
(<48,0,A>, A) (<48,0,B>, ?) (<48,0,C>, ?)
(<48,1,A>, A) (<48,1,B>, ?) (<48,1,C>, ?)
(<49,0,A>, A) (<49,0,B>, ?) (<49,0,C>, ?)
(<49,1,A>, A) (<49,1,B>, ?) (<49,1,C>, ?)
(<50,0,A>, A) (<50,0,B>, 0) (<50,0,C>, C)
(<50,1,A>, A) (<50,1,B>, 0) (<50,1,C>, C)
(<51,0,A>, A) (<51,0,B>, 0) (<51,0,C>, C)
(<51,1,A>, A) (<51,1,B>, 0) (<51,1,C>, C)
(<52,0,A>, A) (<52,0,B>, 0) (<52,0,C>, C)
(<52,1,A>, A) (<52,1,B>, 0) (<52,1,C>, C)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(add) = 2*x1
p(n5) = 0
p(n8) = 2*x1 + -2*x2
p(n81) = 1
p(n9) = 2*x1 + -2*x2
p(n91) = 0
p(o0) = 2*x1 + -2*x2
p(o01) = 0
p(o1) = 2*x1
The following rules are strictly oriented:
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 2*A + -2*B
> 2*A + -2*E
= c2(o0(A,E,B),n91(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 2*A + -2*B
> 2*A + -2*E
= c2(n8(A,E,B),o01(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 2*A + -2*B
> 2*A + -2*E
= c2(n9(A,E,B),o01(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 2*A + -2*B
> 2*A + -2*E
= c2(o0(A,E,B),o01(A,E,B))
The following rules are weakly oriented:
[A >= 0 && A >= 0] ==>
add(A,B,C) = 2*A
>= 2*A
= o1(A,B,C)
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 2*A + -2*B
>= 1 + 2*A + -2*E
= c2(n8(A,E,B),n81(A,E,B))
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 2*A + -2*B
>= 1 + 2*A + -2*E
= c2(n9(A,E,B),n81(A,E,B))
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 2*A + -2*B
>= 1 + 2*A + -2*E
= c2(o0(A,E,B),n81(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 2*A + -2*B
>= 2*A + -2*E
= c2(n8(A,E,B),n91(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 2*A + -2*B
>= 2*A + -2*E
= c2(n9(A,E,B),n91(A,E,B))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 2*A
>= 2*A
= c2(n5(A,0,C),n8(A,0,C))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 2*A
>= 2*A
= c2(n5(A,0,C),n9(A,0,C))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 2*A
>= 2*A
= c2(n5(A,0,C),o0(A,0,C))
* Step 38: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
41. n8(A,B,C) -> c2(n8(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
42. n8(A,B,C) -> c2(n9(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
43. n8(A,B,C) -> c2(o0(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
44. n9(A,B,C) -> c2(n8(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
45. n9(A,B,C) -> c2(n9(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
46. n9(A,B,C) -> c2(o0(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (2*A,7)
47. o0(A,B,C) -> c2(n8(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
48. o0(A,B,C) -> c2(n9(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
49. o0(A,B,C) -> c2(o0(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
50. o1(A,B,C) -> c2(n5(A,0,C),n8(A,0,C)) [A >= 0 && A >= 0] (2,5)
51. o1(A,B,C) -> c2(n5(A,0,C),n9(A,0,C)) [A >= 0 && A >= 0] (2,5)
52. o1(A,B,C) -> c2(n5(A,0,C),o0(A,0,C)) [A >= 0 && A >= 0] (2,5)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[28->{50,51,52},41->{41,42,43},42->{44,45,46},43->{47,48,49},44->{41,42,43},45->{44,45,46},46->{47,48,49}
,47->{41,42,43},48->{44,45,46},49->{47,48,49},50->{41,42,43},51->{44,45,46},52->{47,48,49}]
Sizebounds:
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<41,0,A>, A) (<41,0,B>, ?) (<41,0,C>, ?)
(<41,1,A>, A) (<41,1,B>, ?) (<41,1,C>, ?)
(<42,0,A>, A) (<42,0,B>, ?) (<42,0,C>, ?)
(<42,1,A>, A) (<42,1,B>, ?) (<42,1,C>, ?)
(<43,0,A>, A) (<43,0,B>, ?) (<43,0,C>, ?)
(<43,1,A>, A) (<43,1,B>, ?) (<43,1,C>, ?)
(<44,0,A>, A) (<44,0,B>, ?) (<44,0,C>, ?)
(<44,1,A>, A) (<44,1,B>, ?) (<44,1,C>, ?)
(<45,0,A>, A) (<45,0,B>, ?) (<45,0,C>, ?)
(<45,1,A>, A) (<45,1,B>, ?) (<45,1,C>, ?)
(<46,0,A>, A) (<46,0,B>, ?) (<46,0,C>, ?)
(<46,1,A>, A) (<46,1,B>, ?) (<46,1,C>, ?)
(<47,0,A>, A) (<47,0,B>, ?) (<47,0,C>, ?)
(<47,1,A>, A) (<47,1,B>, ?) (<47,1,C>, ?)
(<48,0,A>, A) (<48,0,B>, ?) (<48,0,C>, ?)
(<48,1,A>, A) (<48,1,B>, ?) (<48,1,C>, ?)
(<49,0,A>, A) (<49,0,B>, ?) (<49,0,C>, ?)
(<49,1,A>, A) (<49,1,B>, ?) (<49,1,C>, ?)
(<50,0,A>, A) (<50,0,B>, 0) (<50,0,C>, C)
(<50,1,A>, A) (<50,1,B>, 0) (<50,1,C>, C)
(<51,0,A>, A) (<51,0,B>, 0) (<51,0,C>, C)
(<51,1,A>, A) (<51,1,B>, 0) (<51,1,C>, C)
(<52,0,A>, A) (<52,0,B>, 0) (<52,0,C>, C)
(<52,1,A>, A) (<52,1,B>, 0) (<52,1,C>, C)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(add) = 3*x1
p(n5) = 0
p(n8) = 3*x1 + -3*x2
p(n81) = 0
p(n9) = 3*x1 + -3*x2
p(n91) = 0
p(o0) = 3*x1 + -3*x2
p(o01) = 0
p(o1) = 3*x1
The following rules are strictly oriented:
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 3*A + -3*B
> 3*A + -3*E
= c2(n9(A,E,B),n91(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 3*A + -3*B
> 3*A + -3*E
= c2(o0(A,E,B),n91(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 3*A + -3*B
> 3*A + -3*E
= c2(n8(A,E,B),o01(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 3*A + -3*B
> 3*A + -3*E
= c2(n9(A,E,B),o01(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 3*A + -3*B
> 3*A + -3*E
= c2(o0(A,E,B),o01(A,E,B))
The following rules are weakly oriented:
[A >= 0 && A >= 0] ==>
add(A,B,C) = 3*A
>= 3*A
= o1(A,B,C)
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 3*A + -3*B
>= 3*A + -3*E
= c2(n8(A,E,B),n81(A,E,B))
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 3*A + -3*B
>= 3*A + -3*E
= c2(n9(A,E,B),n81(A,E,B))
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 3*A + -3*B
>= 3*A + -3*E
= c2(o0(A,E,B),n81(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 3*A + -3*B
>= 3*A + -3*E
= c2(n8(A,E,B),n91(A,E,B))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 3*A
>= 3*A
= c2(n5(A,0,C),n8(A,0,C))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 3*A
>= 3*A
= c2(n5(A,0,C),n9(A,0,C))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 3*A
>= 3*A
= c2(n5(A,0,C),o0(A,0,C))
* Step 39: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
41. n8(A,B,C) -> c2(n8(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
42. n8(A,B,C) -> c2(n9(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
43. n8(A,B,C) -> c2(o0(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
44. n9(A,B,C) -> c2(n8(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (?,7)
45. n9(A,B,C) -> c2(n9(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (3*A,7)
46. n9(A,B,C) -> c2(o0(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (2*A,7)
47. o0(A,B,C) -> c2(n8(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
48. o0(A,B,C) -> c2(n9(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
49. o0(A,B,C) -> c2(o0(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
50. o1(A,B,C) -> c2(n5(A,0,C),n8(A,0,C)) [A >= 0 && A >= 0] (2,5)
51. o1(A,B,C) -> c2(n5(A,0,C),n9(A,0,C)) [A >= 0 && A >= 0] (2,5)
52. o1(A,B,C) -> c2(n5(A,0,C),o0(A,0,C)) [A >= 0 && A >= 0] (2,5)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[28->{50,51,52},41->{41,42,43},42->{44,45,46},43->{47,48,49},44->{41,42,43},45->{44,45,46},46->{47,48,49}
,47->{41,42,43},48->{44,45,46},49->{47,48,49},50->{41,42,43},51->{44,45,46},52->{47,48,49}]
Sizebounds:
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<41,0,A>, A) (<41,0,B>, ?) (<41,0,C>, ?)
(<41,1,A>, A) (<41,1,B>, ?) (<41,1,C>, ?)
(<42,0,A>, A) (<42,0,B>, ?) (<42,0,C>, ?)
(<42,1,A>, A) (<42,1,B>, ?) (<42,1,C>, ?)
(<43,0,A>, A) (<43,0,B>, ?) (<43,0,C>, ?)
(<43,1,A>, A) (<43,1,B>, ?) (<43,1,C>, ?)
(<44,0,A>, A) (<44,0,B>, ?) (<44,0,C>, ?)
(<44,1,A>, A) (<44,1,B>, ?) (<44,1,C>, ?)
(<45,0,A>, A) (<45,0,B>, ?) (<45,0,C>, ?)
(<45,1,A>, A) (<45,1,B>, ?) (<45,1,C>, ?)
(<46,0,A>, A) (<46,0,B>, ?) (<46,0,C>, ?)
(<46,1,A>, A) (<46,1,B>, ?) (<46,1,C>, ?)
(<47,0,A>, A) (<47,0,B>, ?) (<47,0,C>, ?)
(<47,1,A>, A) (<47,1,B>, ?) (<47,1,C>, ?)
(<48,0,A>, A) (<48,0,B>, ?) (<48,0,C>, ?)
(<48,1,A>, A) (<48,1,B>, ?) (<48,1,C>, ?)
(<49,0,A>, A) (<49,0,B>, ?) (<49,0,C>, ?)
(<49,1,A>, A) (<49,1,B>, ?) (<49,1,C>, ?)
(<50,0,A>, A) (<50,0,B>, 0) (<50,0,C>, C)
(<50,1,A>, A) (<50,1,B>, 0) (<50,1,C>, C)
(<51,0,A>, A) (<51,0,B>, 0) (<51,0,C>, C)
(<51,1,A>, A) (<51,1,B>, 0) (<51,1,C>, C)
(<52,0,A>, A) (<52,0,B>, 0) (<52,0,C>, C)
(<52,1,A>, A) (<52,1,B>, 0) (<52,1,C>, C)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(add) = 4*x1
p(n5) = 0
p(n8) = 4*x1 + -4*x2
p(n81) = 0
p(n9) = 4*x1 + -4*x2
p(n91) = 0
p(o0) = 4*x1 + -4*x2
p(o01) = 0
p(o1) = 4*x1
The following rules are strictly oriented:
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 4*A + -4*B
> 4*A + -4*E
= c2(n8(A,E,B),n91(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 4*A + -4*B
> 4*A + -4*E
= c2(n9(A,E,B),n91(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 4*A + -4*B
> 4*A + -4*E
= c2(o0(A,E,B),n91(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 4*A + -4*B
> 4*A + -4*E
= c2(n8(A,E,B),o01(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 4*A + -4*B
> 4*A + -4*E
= c2(n9(A,E,B),o01(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 4*A + -4*B
> 4*A + -4*E
= c2(o0(A,E,B),o01(A,E,B))
The following rules are weakly oriented:
[A >= 0 && A >= 0] ==>
add(A,B,C) = 4*A
>= 4*A
= o1(A,B,C)
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 4*A + -4*B
>= 4*A + -4*E
= c2(n8(A,E,B),n81(A,E,B))
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 4*A + -4*B
>= 4*A + -4*E
= c2(n9(A,E,B),n81(A,E,B))
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 4*A + -4*B
>= 4*A + -4*E
= c2(o0(A,E,B),n81(A,E,B))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 4*A
>= 4*A
= c2(n5(A,0,C),n8(A,0,C))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 4*A
>= 4*A
= c2(n5(A,0,C),n9(A,0,C))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 4*A
>= 4*A
= c2(n5(A,0,C),o0(A,0,C))
* Step 40: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
41. n8(A,B,C) -> c2(n8(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
42. n8(A,B,C) -> c2(n9(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
43. n8(A,B,C) -> c2(o0(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
44. n9(A,B,C) -> c2(n8(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (4*A,7)
45. n9(A,B,C) -> c2(n9(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (3*A,7)
46. n9(A,B,C) -> c2(o0(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (2*A,7)
47. o0(A,B,C) -> c2(n8(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
48. o0(A,B,C) -> c2(n9(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
49. o0(A,B,C) -> c2(o0(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
50. o1(A,B,C) -> c2(n5(A,0,C),n8(A,0,C)) [A >= 0 && A >= 0] (2,5)
51. o1(A,B,C) -> c2(n5(A,0,C),n9(A,0,C)) [A >= 0 && A >= 0] (2,5)
52. o1(A,B,C) -> c2(n5(A,0,C),o0(A,0,C)) [A >= 0 && A >= 0] (2,5)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[28->{50,51,52},41->{41,42,43},42->{44,45,46},43->{47,48,49},44->{41,42,43},45->{44,45,46},46->{47,48,49}
,47->{41,42,43},48->{44,45,46},49->{47,48,49},50->{41,42,43},51->{44,45,46},52->{47,48,49}]
Sizebounds:
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<41,0,A>, A) (<41,0,B>, ?) (<41,0,C>, ?)
(<41,1,A>, A) (<41,1,B>, ?) (<41,1,C>, ?)
(<42,0,A>, A) (<42,0,B>, ?) (<42,0,C>, ?)
(<42,1,A>, A) (<42,1,B>, ?) (<42,1,C>, ?)
(<43,0,A>, A) (<43,0,B>, ?) (<43,0,C>, ?)
(<43,1,A>, A) (<43,1,B>, ?) (<43,1,C>, ?)
(<44,0,A>, A) (<44,0,B>, ?) (<44,0,C>, ?)
(<44,1,A>, A) (<44,1,B>, ?) (<44,1,C>, ?)
(<45,0,A>, A) (<45,0,B>, ?) (<45,0,C>, ?)
(<45,1,A>, A) (<45,1,B>, ?) (<45,1,C>, ?)
(<46,0,A>, A) (<46,0,B>, ?) (<46,0,C>, ?)
(<46,1,A>, A) (<46,1,B>, ?) (<46,1,C>, ?)
(<47,0,A>, A) (<47,0,B>, ?) (<47,0,C>, ?)
(<47,1,A>, A) (<47,1,B>, ?) (<47,1,C>, ?)
(<48,0,A>, A) (<48,0,B>, ?) (<48,0,C>, ?)
(<48,1,A>, A) (<48,1,B>, ?) (<48,1,C>, ?)
(<49,0,A>, A) (<49,0,B>, ?) (<49,0,C>, ?)
(<49,1,A>, A) (<49,1,B>, ?) (<49,1,C>, ?)
(<50,0,A>, A) (<50,0,B>, 0) (<50,0,C>, C)
(<50,1,A>, A) (<50,1,B>, 0) (<50,1,C>, C)
(<51,0,A>, A) (<51,0,B>, 0) (<51,0,C>, C)
(<51,1,A>, A) (<51,1,B>, 0) (<51,1,C>, C)
(<52,0,A>, A) (<52,0,B>, 0) (<52,0,C>, C)
(<52,1,A>, A) (<52,1,B>, 0) (<52,1,C>, C)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(add) = 5*x1
p(n5) = 0
p(n8) = 5*x1 + -5*x2
p(n81) = 4
p(n9) = 5*x1 + -5*x2
p(n91) = 0
p(o0) = 5*x1 + -5*x2
p(o01) = 2
p(o1) = 5*x1
The following rules are strictly oriented:
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 5*A + -5*B
> 4 + 5*A + -5*E
= c2(o0(A,E,B),n81(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 5*A + -5*B
> 5*A + -5*E
= c2(n8(A,E,B),n91(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 5*A + -5*B
> 5*A + -5*E
= c2(n9(A,E,B),n91(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 5*A + -5*B
> 5*A + -5*E
= c2(o0(A,E,B),n91(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 5*A + -5*B
> 2 + 5*A + -5*E
= c2(n8(A,E,B),o01(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 5*A + -5*B
> 2 + 5*A + -5*E
= c2(n9(A,E,B),o01(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 5*A + -5*B
> 2 + 5*A + -5*E
= c2(o0(A,E,B),o01(A,E,B))
The following rules are weakly oriented:
[A >= 0 && A >= 0] ==>
add(A,B,C) = 5*A
>= 5*A
= o1(A,B,C)
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 5*A + -5*B
>= 4 + 5*A + -5*E
= c2(n8(A,E,B),n81(A,E,B))
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 5*A + -5*B
>= 4 + 5*A + -5*E
= c2(n9(A,E,B),n81(A,E,B))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 5*A
>= 5*A
= c2(n5(A,0,C),n8(A,0,C))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 5*A
>= 5*A
= c2(n5(A,0,C),n9(A,0,C))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 5*A
>= 5*A
= c2(n5(A,0,C),o0(A,0,C))
* Step 41: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
41. n8(A,B,C) -> c2(n8(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
42. n8(A,B,C) -> c2(n9(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
43. n8(A,B,C) -> c2(o0(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (5*A,7)
44. n9(A,B,C) -> c2(n8(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (4*A,7)
45. n9(A,B,C) -> c2(n9(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (3*A,7)
46. n9(A,B,C) -> c2(o0(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (2*A,7)
47. o0(A,B,C) -> c2(n8(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
48. o0(A,B,C) -> c2(n9(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
49. o0(A,B,C) -> c2(o0(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
50. o1(A,B,C) -> c2(n5(A,0,C),n8(A,0,C)) [A >= 0 && A >= 0] (2,5)
51. o1(A,B,C) -> c2(n5(A,0,C),n9(A,0,C)) [A >= 0 && A >= 0] (2,5)
52. o1(A,B,C) -> c2(n5(A,0,C),o0(A,0,C)) [A >= 0 && A >= 0] (2,5)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[28->{50,51,52},41->{41,42,43},42->{44,45,46},43->{47,48,49},44->{41,42,43},45->{44,45,46},46->{47,48,49}
,47->{41,42,43},48->{44,45,46},49->{47,48,49},50->{41,42,43},51->{44,45,46},52->{47,48,49}]
Sizebounds:
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<41,0,A>, A) (<41,0,B>, ?) (<41,0,C>, ?)
(<41,1,A>, A) (<41,1,B>, ?) (<41,1,C>, ?)
(<42,0,A>, A) (<42,0,B>, ?) (<42,0,C>, ?)
(<42,1,A>, A) (<42,1,B>, ?) (<42,1,C>, ?)
(<43,0,A>, A) (<43,0,B>, ?) (<43,0,C>, ?)
(<43,1,A>, A) (<43,1,B>, ?) (<43,1,C>, ?)
(<44,0,A>, A) (<44,0,B>, ?) (<44,0,C>, ?)
(<44,1,A>, A) (<44,1,B>, ?) (<44,1,C>, ?)
(<45,0,A>, A) (<45,0,B>, ?) (<45,0,C>, ?)
(<45,1,A>, A) (<45,1,B>, ?) (<45,1,C>, ?)
(<46,0,A>, A) (<46,0,B>, ?) (<46,0,C>, ?)
(<46,1,A>, A) (<46,1,B>, ?) (<46,1,C>, ?)
(<47,0,A>, A) (<47,0,B>, ?) (<47,0,C>, ?)
(<47,1,A>, A) (<47,1,B>, ?) (<47,1,C>, ?)
(<48,0,A>, A) (<48,0,B>, ?) (<48,0,C>, ?)
(<48,1,A>, A) (<48,1,B>, ?) (<48,1,C>, ?)
(<49,0,A>, A) (<49,0,B>, ?) (<49,0,C>, ?)
(<49,1,A>, A) (<49,1,B>, ?) (<49,1,C>, ?)
(<50,0,A>, A) (<50,0,B>, 0) (<50,0,C>, C)
(<50,1,A>, A) (<50,1,B>, 0) (<50,1,C>, C)
(<51,0,A>, A) (<51,0,B>, 0) (<51,0,C>, C)
(<51,1,A>, A) (<51,1,B>, 0) (<51,1,C>, C)
(<52,0,A>, A) (<52,0,B>, 0) (<52,0,C>, C)
(<52,1,A>, A) (<52,1,B>, 0) (<52,1,C>, C)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(add) = 7*x1
p(n5) = 0
p(n8) = 7*x1 + -7*x2
p(n81) = 6
p(n9) = 7*x1 + -7*x2
p(n91) = 0
p(o0) = 7*x1 + -7*x2
p(o01) = 5
p(o1) = 7*x1
The following rules are strictly oriented:
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 7*A + -7*B
> 6 + 7*A + -7*E
= c2(n9(A,E,B),n81(A,E,B))
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 7*A + -7*B
> 6 + 7*A + -7*E
= c2(o0(A,E,B),n81(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 7*A + -7*B
> 7*A + -7*E
= c2(n8(A,E,B),n91(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 7*A + -7*B
> 7*A + -7*E
= c2(n9(A,E,B),n91(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 7*A + -7*B
> 7*A + -7*E
= c2(o0(A,E,B),n91(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 7*A + -7*B
> 5 + 7*A + -7*E
= c2(n8(A,E,B),o01(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 7*A + -7*B
> 5 + 7*A + -7*E
= c2(n9(A,E,B),o01(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 7*A + -7*B
> 5 + 7*A + -7*E
= c2(o0(A,E,B),o01(A,E,B))
The following rules are weakly oriented:
[A >= 0 && A >= 0] ==>
add(A,B,C) = 7*A
>= 7*A
= o1(A,B,C)
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 7*A + -7*B
>= 6 + 7*A + -7*E
= c2(n8(A,E,B),n81(A,E,B))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 7*A
>= 7*A
= c2(n5(A,0,C),n8(A,0,C))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 7*A
>= 7*A
= c2(n5(A,0,C),n9(A,0,C))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 7*A
>= 7*A
= c2(n5(A,0,C),o0(A,0,C))
* Step 42: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
41. n8(A,B,C) -> c2(n8(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (?,7)
42. n8(A,B,C) -> c2(n9(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (7*A,7)
43. n8(A,B,C) -> c2(o0(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (5*A,7)
44. n9(A,B,C) -> c2(n8(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (4*A,7)
45. n9(A,B,C) -> c2(n9(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (3*A,7)
46. n9(A,B,C) -> c2(o0(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (2*A,7)
47. o0(A,B,C) -> c2(n8(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
48. o0(A,B,C) -> c2(n9(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
49. o0(A,B,C) -> c2(o0(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
50. o1(A,B,C) -> c2(n5(A,0,C),n8(A,0,C)) [A >= 0 && A >= 0] (2,5)
51. o1(A,B,C) -> c2(n5(A,0,C),n9(A,0,C)) [A >= 0 && A >= 0] (2,5)
52. o1(A,B,C) -> c2(n5(A,0,C),o0(A,0,C)) [A >= 0 && A >= 0] (2,5)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[28->{50,51,52},41->{41,42,43},42->{44,45,46},43->{47,48,49},44->{41,42,43},45->{44,45,46},46->{47,48,49}
,47->{41,42,43},48->{44,45,46},49->{47,48,49},50->{41,42,43},51->{44,45,46},52->{47,48,49}]
Sizebounds:
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<41,0,A>, A) (<41,0,B>, ?) (<41,0,C>, ?)
(<41,1,A>, A) (<41,1,B>, ?) (<41,1,C>, ?)
(<42,0,A>, A) (<42,0,B>, ?) (<42,0,C>, ?)
(<42,1,A>, A) (<42,1,B>, ?) (<42,1,C>, ?)
(<43,0,A>, A) (<43,0,B>, ?) (<43,0,C>, ?)
(<43,1,A>, A) (<43,1,B>, ?) (<43,1,C>, ?)
(<44,0,A>, A) (<44,0,B>, ?) (<44,0,C>, ?)
(<44,1,A>, A) (<44,1,B>, ?) (<44,1,C>, ?)
(<45,0,A>, A) (<45,0,B>, ?) (<45,0,C>, ?)
(<45,1,A>, A) (<45,1,B>, ?) (<45,1,C>, ?)
(<46,0,A>, A) (<46,0,B>, ?) (<46,0,C>, ?)
(<46,1,A>, A) (<46,1,B>, ?) (<46,1,C>, ?)
(<47,0,A>, A) (<47,0,B>, ?) (<47,0,C>, ?)
(<47,1,A>, A) (<47,1,B>, ?) (<47,1,C>, ?)
(<48,0,A>, A) (<48,0,B>, ?) (<48,0,C>, ?)
(<48,1,A>, A) (<48,1,B>, ?) (<48,1,C>, ?)
(<49,0,A>, A) (<49,0,B>, ?) (<49,0,C>, ?)
(<49,1,A>, A) (<49,1,B>, ?) (<49,1,C>, ?)
(<50,0,A>, A) (<50,0,B>, 0) (<50,0,C>, C)
(<50,1,A>, A) (<50,1,B>, 0) (<50,1,C>, C)
(<51,0,A>, A) (<51,0,B>, 0) (<51,0,C>, C)
(<51,1,A>, A) (<51,1,B>, 0) (<51,1,C>, C)
(<52,0,A>, A) (<52,0,B>, 0) (<52,0,C>, C)
(<52,1,A>, A) (<52,1,B>, 0) (<52,1,C>, C)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(add) = 2*x1
p(n5) = 0
p(n8) = 2*x1 + -2*x2
p(n81) = 1
p(n9) = 2*x1 + -2*x2
p(n91) = 0
p(o0) = 2*x1 + -2*x2
p(o01) = 0
p(o1) = 2*x1
The following rules are strictly oriented:
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 2*A + -2*B
> 1 + 2*A + -2*E
= c2(n8(A,E,B),n81(A,E,B))
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 2*A + -2*B
> 1 + 2*A + -2*E
= c2(n9(A,E,B),n81(A,E,B))
[A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] ==>
n8(A,B,C) = 2*A + -2*B
> 1 + 2*A + -2*E
= c2(o0(A,E,B),n81(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 2*A + -2*B
> 2*A + -2*E
= c2(n8(A,E,B),n91(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 2*A + -2*B
> 2*A + -2*E
= c2(n9(A,E,B),n91(A,E,B))
[A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] ==>
n9(A,B,C) = 2*A + -2*B
> 2*A + -2*E
= c2(o0(A,E,B),n91(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 2*A + -2*B
> 2*A + -2*E
= c2(n8(A,E,B),o01(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 2*A + -2*B
> 2*A + -2*E
= c2(n9(A,E,B),o01(A,E,B))
[A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] ==>
o0(A,B,C) = 2*A + -2*B
> 2*A + -2*E
= c2(o0(A,E,B),o01(A,E,B))
The following rules are weakly oriented:
[A >= 0 && A >= 0] ==>
add(A,B,C) = 2*A
>= 2*A
= o1(A,B,C)
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 2*A
>= 2*A
= c2(n5(A,0,C),n8(A,0,C))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 2*A
>= 2*A
= c2(n5(A,0,C),n9(A,0,C))
[A >= 0 && A >= 0] ==>
o1(A,B,C) = 2*A
>= 2*A
= c2(n5(A,0,C),o0(A,0,C))
* Step 43: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
28. add(A,B,C) -> o1(A,B,C) [A >= 0 && A >= 0] (1,2)
41. n8(A,B,C) -> c2(n8(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (2*A,7)
42. n8(A,B,C) -> c2(n9(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (2*A,7)
43. n8(A,B,C) -> c2(o0(A,E,B),n81(A,E,B)) [A >= B && 1 + B >= E && E >= 1 + B && 3 + A >= E && A >= E] (2*A,7)
44. n9(A,B,C) -> c2(n8(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (2*A,7)
45. n9(A,B,C) -> c2(n9(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (2*A,7)
46. n9(A,B,C) -> c2(o0(A,E,B),n91(A,E,B)) [A >= B && 2 + B >= E && E >= 2 + B && 3 + A >= E && A >= E] (2*A,7)
47. o0(A,B,C) -> c2(n8(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
48. o0(A,B,C) -> c2(n9(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
49. o0(A,B,C) -> c2(o0(A,E,B),o01(A,E,B)) [A >= B && 3 + B >= E && E >= 3 + B && 3 + A >= E && A >= E] (2*A,7)
50. o1(A,B,C) -> c2(n5(A,0,C),n8(A,0,C)) [A >= 0 && A >= 0] (2,5)
51. o1(A,B,C) -> c2(n5(A,0,C),n9(A,0,C)) [A >= 0 && A >= 0] (2,5)
52. o1(A,B,C) -> c2(n5(A,0,C),o0(A,0,C)) [A >= 0 && A >= 0] (2,5)
Signature:
{(add,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)
;(n6,3)
;(n7,3)
;(n8,3)
;(n80,3)
;(n81,3)
;(n9,3)
;(n90,3)
;(n91,3)
;(o0,3)
;(o00,3)
;(o01,3)
;(o1,3)
;(o2,3)
;(o3,3)}
Flow Graph:
[28->{50,51,52},41->{41,42,43},42->{44,45,46},43->{47,48,49},44->{41,42,43},45->{44,45,46},46->{47,48,49}
,47->{41,42,43},48->{44,45,46},49->{47,48,49},50->{41,42,43},51->{44,45,46},52->{47,48,49}]
Sizebounds:
(<28,0,A>, A) (<28,0,B>, B) (<28,0,C>, C)
(<41,0,A>, A) (<41,0,B>, ?) (<41,0,C>, ?)
(<41,1,A>, A) (<41,1,B>, ?) (<41,1,C>, ?)
(<42,0,A>, A) (<42,0,B>, ?) (<42,0,C>, ?)
(<42,1,A>, A) (<42,1,B>, ?) (<42,1,C>, ?)
(<43,0,A>, A) (<43,0,B>, ?) (<43,0,C>, ?)
(<43,1,A>, A) (<43,1,B>, ?) (<43,1,C>, ?)
(<44,0,A>, A) (<44,0,B>, ?) (<44,0,C>, ?)
(<44,1,A>, A) (<44,1,B>, ?) (<44,1,C>, ?)
(<45,0,A>, A) (<45,0,B>, ?) (<45,0,C>, ?)
(<45,1,A>, A) (<45,1,B>, ?) (<45,1,C>, ?)
(<46,0,A>, A) (<46,0,B>, ?) (<46,0,C>, ?)
(<46,1,A>, A) (<46,1,B>, ?) (<46,1,C>, ?)
(<47,0,A>, A) (<47,0,B>, ?) (<47,0,C>, ?)
(<47,1,A>, A) (<47,1,B>, ?) (<47,1,C>, ?)
(<48,0,A>, A) (<48,0,B>, ?) (<48,0,C>, ?)
(<48,1,A>, A) (<48,1,B>, ?) (<48,1,C>, ?)
(<49,0,A>, A) (<49,0,B>, ?) (<49,0,C>, ?)
(<49,1,A>, A) (<49,1,B>, ?) (<49,1,C>, ?)
(<50,0,A>, A) (<50,0,B>, 0) (<50,0,C>, C)
(<50,1,A>, A) (<50,1,B>, 0) (<50,1,C>, C)
(<51,0,A>, A) (<51,0,B>, 0) (<51,0,C>, C)
(<51,1,A>, A) (<51,1,B>, 0) (<51,1,C>, C)
(<52,0,A>, A) (<52,0,B>, 0) (<52,0,C>, C)
(<52,1,A>, A) (<52,1,B>, 0) (<52,1,C>, C)
+ Applied Processor:
UnsatPaths
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))