WORST_CASE(?,O(1))
* Step 1: RestrictVarsProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f11(100,O,1,D,E,F,G,H,I,J,K,L,M,N) True (1,1)
1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f11(100,O,0,D,E,F,G,H,I,J,K,L,M,N) True (1,1)
2. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f23(A,B,1,1,1,100,O,1,I,J,K,L,M,N) [C = 1] (?,1)
3. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f23(A,B,1,1,1,100,O,0,I,J,K,L,M,N) [C = 1] (?,1)
4. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f26(A,B,C,D,H,F,G,H,100,J,K,L,M,N) [0 >= H] (?,1)
5. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f26(A,B,C,D,H,F,G,H,100,J,K,L,M,N) [H >= 2] (?,1)
6. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f36(A,B,C,C,C,F,G,H,I,100,K,L,M,N) [0 >= C] (?,1)
7. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f36(A,B,C,C,C,F,G,H,I,100,K,L,M,N) [C >= 2] (?,1)
8. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,1,F,G,1,I,J,O,P,M,N) [0 >= 2 + O && H = 1] (?,1)
9. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,1,F,G,1,I,J,O,P,M,N) [O >= 0 && H = 1] (?,1)
10. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,1,F,G,1,I,J,-1,L,100,O) [H = 1] (?,1)
11. f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N) [0 >= 1 + O] (?,1)
12. f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N) True (?,1)
13. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N) [0 >= 1 + O] (?,1)
14. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N) True (?,1)
Signature:
{(f0,14);(f11,14);(f23,14);(f26,14);(f32,14);(f36,14)}
Flow Graph:
[0->{2,3,6,7},1->{2,3,6,7},2->{4,5,8,9,10},3->{4,5,8,9,10},4->{13,14},5->{13,14},6->{11,12},7->{11,12}
,8->{},9->{},10->{},11->{},12->{},13->{},14->{}]
+ Applied Processor:
RestrictVarsProcessor
+ Details:
We removed the arguments [A,B,D,E,F,G,I,J,K,L,M,N] .
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(C,H) -> f11(1,H) True (1,1)
1. f0(C,H) -> f11(0,H) True (1,1)
2. f11(C,H) -> f23(1,1) [C = 1] (?,1)
3. f11(C,H) -> f23(1,0) [C = 1] (?,1)
4. f23(C,H) -> f26(C,H) [0 >= H] (?,1)
5. f23(C,H) -> f26(C,H) [H >= 2] (?,1)
6. f11(C,H) -> f36(C,H) [0 >= C] (?,1)
7. f11(C,H) -> f36(C,H) [C >= 2] (?,1)
8. f23(C,H) -> f32(C,1) [0 >= 2 + O && H = 1] (?,1)
9. f23(C,H) -> f32(C,1) [O >= 0 && H = 1] (?,1)
10. f23(C,H) -> f32(C,1) [H = 1] (?,1)
11. f36(C,H) -> f32(C,H) [0 >= 1 + O] (?,1)
12. f36(C,H) -> f32(C,H) True (?,1)
13. f26(C,H) -> f32(C,H) [0 >= 1 + O] (?,1)
14. f26(C,H) -> f32(C,H) True (?,1)
Signature:
{(f0,2);(f11,2);(f23,2);(f26,2);(f32,2);(f36,2)}
Flow Graph:
[0->{2,3,6,7},1->{2,3,6,7},2->{4,5,8,9,10},3->{4,5,8,9,10},4->{13,14},5->{13,14},6->{11,12},7->{11,12}
,8->{},9->{},10->{},11->{},12->{},13->{},14->{}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,C>, 1, .= 1) (< 0,0,H>, H, .= 0)
(< 1,0,C>, 0, .= 0) (< 1,0,H>, H, .= 0)
(< 2,0,C>, 1, .= 1) (< 2,0,H>, 1, .= 1)
(< 3,0,C>, 1, .= 1) (< 3,0,H>, 0, .= 0)
(< 4,0,C>, C, .= 0) (< 4,0,H>, H, .= 0)
(< 5,0,C>, C, .= 0) (< 5,0,H>, H, .= 0)
(< 6,0,C>, C, .= 0) (< 6,0,H>, H, .= 0)
(< 7,0,C>, C, .= 0) (< 7,0,H>, H, .= 0)
(< 8,0,C>, C, .= 0) (< 8,0,H>, 1, .= 1)
(< 9,0,C>, C, .= 0) (< 9,0,H>, 1, .= 1)
(<10,0,C>, C, .= 0) (<10,0,H>, 1, .= 1)
(<11,0,C>, C, .= 0) (<11,0,H>, H, .= 0)
(<12,0,C>, C, .= 0) (<12,0,H>, H, .= 0)
(<13,0,C>, C, .= 0) (<13,0,H>, H, .= 0)
(<14,0,C>, C, .= 0) (<14,0,H>, H, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(C,H) -> f11(1,H) True (1,1)
1. f0(C,H) -> f11(0,H) True (1,1)
2. f11(C,H) -> f23(1,1) [C = 1] (?,1)
3. f11(C,H) -> f23(1,0) [C = 1] (?,1)
4. f23(C,H) -> f26(C,H) [0 >= H] (?,1)
5. f23(C,H) -> f26(C,H) [H >= 2] (?,1)
6. f11(C,H) -> f36(C,H) [0 >= C] (?,1)
7. f11(C,H) -> f36(C,H) [C >= 2] (?,1)
8. f23(C,H) -> f32(C,1) [0 >= 2 + O && H = 1] (?,1)
9. f23(C,H) -> f32(C,1) [O >= 0 && H = 1] (?,1)
10. f23(C,H) -> f32(C,1) [H = 1] (?,1)
11. f36(C,H) -> f32(C,H) [0 >= 1 + O] (?,1)
12. f36(C,H) -> f32(C,H) True (?,1)
13. f26(C,H) -> f32(C,H) [0 >= 1 + O] (?,1)
14. f26(C,H) -> f32(C,H) True (?,1)
Signature:
{(f0,2);(f11,2);(f23,2);(f26,2);(f32,2);(f36,2)}
Flow Graph:
[0->{2,3,6,7},1->{2,3,6,7},2->{4,5,8,9,10},3->{4,5,8,9,10},4->{13,14},5->{13,14},6->{11,12},7->{11,12}
,8->{},9->{},10->{},11->{},12->{},13->{},14->{}]
Sizebounds:
(< 0,0,C>, ?) (< 0,0,H>, ?)
(< 1,0,C>, ?) (< 1,0,H>, ?)
(< 2,0,C>, ?) (< 2,0,H>, ?)
(< 3,0,C>, ?) (< 3,0,H>, ?)
(< 4,0,C>, ?) (< 4,0,H>, ?)
(< 5,0,C>, ?) (< 5,0,H>, ?)
(< 6,0,C>, ?) (< 6,0,H>, ?)
(< 7,0,C>, ?) (< 7,0,H>, ?)
(< 8,0,C>, ?) (< 8,0,H>, ?)
(< 9,0,C>, ?) (< 9,0,H>, ?)
(<10,0,C>, ?) (<10,0,H>, ?)
(<11,0,C>, ?) (<11,0,H>, ?)
(<12,0,C>, ?) (<12,0,H>, ?)
(<13,0,C>, ?) (<13,0,H>, ?)
(<14,0,C>, ?) (<14,0,H>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,C>, 1) (< 0,0,H>, H)
(< 1,0,C>, 0) (< 1,0,H>, H)
(< 2,0,C>, 1) (< 2,0,H>, 1)
(< 3,0,C>, 1) (< 3,0,H>, 0)
(< 4,0,C>, 1) (< 4,0,H>, 1)
(< 5,0,C>, 1) (< 5,0,H>, 1)
(< 6,0,C>, 1) (< 6,0,H>, H)
(< 7,0,C>, 1) (< 7,0,H>, H)
(< 8,0,C>, 1) (< 8,0,H>, 1)
(< 9,0,C>, 1) (< 9,0,H>, 1)
(<10,0,C>, 1) (<10,0,H>, 1)
(<11,0,C>, 1) (<11,0,H>, H)
(<12,0,C>, 1) (<12,0,H>, H)
(<13,0,C>, 1) (<13,0,H>, 1)
(<14,0,C>, 1) (<14,0,H>, 1)
* Step 4: UnsatPaths WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(C,H) -> f11(1,H) True (1,1)
1. f0(C,H) -> f11(0,H) True (1,1)
2. f11(C,H) -> f23(1,1) [C = 1] (?,1)
3. f11(C,H) -> f23(1,0) [C = 1] (?,1)
4. f23(C,H) -> f26(C,H) [0 >= H] (?,1)
5. f23(C,H) -> f26(C,H) [H >= 2] (?,1)
6. f11(C,H) -> f36(C,H) [0 >= C] (?,1)
7. f11(C,H) -> f36(C,H) [C >= 2] (?,1)
8. f23(C,H) -> f32(C,1) [0 >= 2 + O && H = 1] (?,1)
9. f23(C,H) -> f32(C,1) [O >= 0 && H = 1] (?,1)
10. f23(C,H) -> f32(C,1) [H = 1] (?,1)
11. f36(C,H) -> f32(C,H) [0 >= 1 + O] (?,1)
12. f36(C,H) -> f32(C,H) True (?,1)
13. f26(C,H) -> f32(C,H) [0 >= 1 + O] (?,1)
14. f26(C,H) -> f32(C,H) True (?,1)
Signature:
{(f0,2);(f11,2);(f23,2);(f26,2);(f32,2);(f36,2)}
Flow Graph:
[0->{2,3,6,7},1->{2,3,6,7},2->{4,5,8,9,10},3->{4,5,8,9,10},4->{13,14},5->{13,14},6->{11,12},7->{11,12}
,8->{},9->{},10->{},11->{},12->{},13->{},14->{}]
Sizebounds:
(< 0,0,C>, 1) (< 0,0,H>, H)
(< 1,0,C>, 0) (< 1,0,H>, H)
(< 2,0,C>, 1) (< 2,0,H>, 1)
(< 3,0,C>, 1) (< 3,0,H>, 0)
(< 4,0,C>, 1) (< 4,0,H>, 1)
(< 5,0,C>, 1) (< 5,0,H>, 1)
(< 6,0,C>, 1) (< 6,0,H>, H)
(< 7,0,C>, 1) (< 7,0,H>, H)
(< 8,0,C>, 1) (< 8,0,H>, 1)
(< 9,0,C>, 1) (< 9,0,H>, 1)
(<10,0,C>, 1) (<10,0,H>, 1)
(<11,0,C>, 1) (<11,0,H>, H)
(<12,0,C>, 1) (<12,0,H>, H)
(<13,0,C>, 1) (<13,0,H>, 1)
(<14,0,C>, 1) (<14,0,H>, 1)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(0,6)
,(0,7)
,(1,2)
,(1,3)
,(1,7)
,(2,4)
,(2,5)
,(3,5)
,(3,8)
,(3,9)
,(3,10)]
* Step 5: UnreachableRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(C,H) -> f11(1,H) True (1,1)
1. f0(C,H) -> f11(0,H) True (1,1)
2. f11(C,H) -> f23(1,1) [C = 1] (?,1)
3. f11(C,H) -> f23(1,0) [C = 1] (?,1)
4. f23(C,H) -> f26(C,H) [0 >= H] (?,1)
5. f23(C,H) -> f26(C,H) [H >= 2] (?,1)
6. f11(C,H) -> f36(C,H) [0 >= C] (?,1)
7. f11(C,H) -> f36(C,H) [C >= 2] (?,1)
8. f23(C,H) -> f32(C,1) [0 >= 2 + O && H = 1] (?,1)
9. f23(C,H) -> f32(C,1) [O >= 0 && H = 1] (?,1)
10. f23(C,H) -> f32(C,1) [H = 1] (?,1)
11. f36(C,H) -> f32(C,H) [0 >= 1 + O] (?,1)
12. f36(C,H) -> f32(C,H) True (?,1)
13. f26(C,H) -> f32(C,H) [0 >= 1 + O] (?,1)
14. f26(C,H) -> f32(C,H) True (?,1)
Signature:
{(f0,2);(f11,2);(f23,2);(f26,2);(f32,2);(f36,2)}
Flow Graph:
[0->{2,3},1->{6},2->{8,9,10},3->{4},4->{13,14},5->{13,14},6->{11,12},7->{11,12},8->{},9->{},10->{},11->{}
,12->{},13->{},14->{}]
Sizebounds:
(< 0,0,C>, 1) (< 0,0,H>, H)
(< 1,0,C>, 0) (< 1,0,H>, H)
(< 2,0,C>, 1) (< 2,0,H>, 1)
(< 3,0,C>, 1) (< 3,0,H>, 0)
(< 4,0,C>, 1) (< 4,0,H>, 1)
(< 5,0,C>, 1) (< 5,0,H>, 1)
(< 6,0,C>, 1) (< 6,0,H>, H)
(< 7,0,C>, 1) (< 7,0,H>, H)
(< 8,0,C>, 1) (< 8,0,H>, 1)
(< 9,0,C>, 1) (< 9,0,H>, 1)
(<10,0,C>, 1) (<10,0,H>, 1)
(<11,0,C>, 1) (<11,0,H>, H)
(<12,0,C>, 1) (<12,0,H>, H)
(<13,0,C>, 1) (<13,0,H>, 1)
(<14,0,C>, 1) (<14,0,H>, 1)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [5,7]
* Step 6: LeafRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(C,H) -> f11(1,H) True (1,1)
1. f0(C,H) -> f11(0,H) True (1,1)
2. f11(C,H) -> f23(1,1) [C = 1] (?,1)
3. f11(C,H) -> f23(1,0) [C = 1] (?,1)
4. f23(C,H) -> f26(C,H) [0 >= H] (?,1)
6. f11(C,H) -> f36(C,H) [0 >= C] (?,1)
8. f23(C,H) -> f32(C,1) [0 >= 2 + O && H = 1] (?,1)
9. f23(C,H) -> f32(C,1) [O >= 0 && H = 1] (?,1)
10. f23(C,H) -> f32(C,1) [H = 1] (?,1)
11. f36(C,H) -> f32(C,H) [0 >= 1 + O] (?,1)
12. f36(C,H) -> f32(C,H) True (?,1)
13. f26(C,H) -> f32(C,H) [0 >= 1 + O] (?,1)
14. f26(C,H) -> f32(C,H) True (?,1)
Signature:
{(f0,2);(f11,2);(f23,2);(f26,2);(f32,2);(f36,2)}
Flow Graph:
[0->{2,3},1->{6},2->{8,9,10},3->{4},4->{13,14},6->{11,12},8->{},9->{},10->{},11->{},12->{},13->{},14->{}]
Sizebounds:
(< 0,0,C>, 1) (< 0,0,H>, H)
(< 1,0,C>, 0) (< 1,0,H>, H)
(< 2,0,C>, 1) (< 2,0,H>, 1)
(< 3,0,C>, 1) (< 3,0,H>, 0)
(< 4,0,C>, 1) (< 4,0,H>, 1)
(< 6,0,C>, 1) (< 6,0,H>, H)
(< 8,0,C>, 1) (< 8,0,H>, 1)
(< 9,0,C>, 1) (< 9,0,H>, 1)
(<10,0,C>, 1) (<10,0,H>, 1)
(<11,0,C>, 1) (<11,0,H>, H)
(<12,0,C>, 1) (<12,0,H>, H)
(<13,0,C>, 1) (<13,0,H>, 1)
(<14,0,C>, 1) (<14,0,H>, 1)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [3,2,4,6,8,9,10,11,12,13,14]
* Step 7: LocalSizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(C,H) -> f11(1,H) True (1,1)
1. f0(C,H) -> f11(0,H) True (1,1)
Signature:
{(f0,2);(f11,2);(f23,2);(f26,2);(f32,2);(f36,2)}
Flow Graph:
[0->{},1->{}]
Sizebounds:
(<0,0,C>, 1) (<0,0,H>, H)
(<1,0,C>, 0) (<1,0,H>, H)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
The problem is already solved.
WORST_CASE(?,O(1))