WORST_CASE(?,O(n^1))
* Step 1: RestrictVarsProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1)
1. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1)
2. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1)
3. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,D,D,F,F,A,B,I,J,K,L) [A >= 1 + B] (?,1)
4. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,D,D,F,F,A,B,I,J,K,L) [B >= 1 + A] (?,1)
5. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(F,D,D,D,F,F,A,B,I,J,K,L) True (1,1)
6. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(F,D,D,D,F,F,M,N,M,N,K,L) True (1,1)
7. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(O,P,D,M,F,N,A,B,M,N,O,P) True (1,1)
8. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(O,P,D,M,F,N,A,A,M,N,O,P) [A = B] (?,1)
9. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(1 + A,B,D,D,F,F,A,B,I,J,K,L) True (1,1)
10. f4(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(1 + A,B,D,D,F,F,A,B,I,J,K,L) [B >= 1 + A] (?,1)
11. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,1 + B,D,D,F,F,A,B,I,J,K,L) True (1,1)
12. f4(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,1 + B,D,D,F,F,A,B,I,J,K,L) [A >= B] (?,1)
Signature:
{(f0,12);(f3,12);(f4,12);(f8,12)}
Flow Graph:
[0->{3,4,8},1->{10,12},2->{},3->{10,12},4->{10,12},5->{3,4,8},6->{3,4,8},7->{},8->{},9->{3,4,8},10->{3,4
,8},11->{3,4,8},12->{3,4,8}]
+ Applied Processor:
RestrictVarsProcessor
+ Details:
We removed the arguments [C,E,G,H,I,J,K,L] .
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,D,F) -> f3(A,B,D,F) True (1,1)
1. f0(A,B,D,F) -> f4(A,B,D,F) True (1,1)
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
3. f3(A,B,D,F) -> f4(A,B,D,F) [A >= 1 + B] (?,1)
4. f3(A,B,D,F) -> f4(A,B,D,F) [B >= 1 + A] (?,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
8. f3(A,B,D,F) -> f8(O,P,M,N) [A = B] (?,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
10. f4(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (?,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
12. f4(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (?,1)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[0->{3,4,8},1->{10,12},2->{},3->{10,12},4->{10,12},5->{3,4,8},6->{3,4,8},7->{},8->{},9->{3,4,8},10->{3,4
,8},11->{3,4,8},12->{3,4,8}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,A>, A, .= 0) (< 0,0,B>, B, .= 0) (< 0,0,D>, D, .= 0) (< 0,0,F>, F, .= 0)
(< 1,0,A>, A, .= 0) (< 1,0,B>, B, .= 0) (< 1,0,D>, D, .= 0) (< 1,0,F>, F, .= 0)
(< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0) (< 2,0,D>, D, .= 0) (< 2,0,F>, F, .= 0)
(< 3,0,A>, A, .= 0) (< 3,0,B>, B, .= 0) (< 3,0,D>, D, .= 0) (< 3,0,F>, F, .= 0)
(< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 4,0,D>, D, .= 0) (< 4,0,F>, F, .= 0)
(< 5,0,A>, F, .= 0) (< 5,0,B>, D, .= 0) (< 5,0,D>, D, .= 0) (< 5,0,F>, F, .= 0)
(< 6,0,A>, F, .= 0) (< 6,0,B>, D, .= 0) (< 6,0,D>, D, .= 0) (< 6,0,F>, F, .= 0)
(< 7,0,A>, ?, .?) (< 7,0,B>, ?, .?) (< 7,0,D>, ?, .?) (< 7,0,F>, ?, .?)
(< 8,0,A>, ?, .?) (< 8,0,B>, ?, .?) (< 8,0,D>, ?, .?) (< 8,0,F>, ?, .?)
(< 9,0,A>, 1 + A, .+ 1) (< 9,0,B>, B, .= 0) (< 9,0,D>, D, .= 0) (< 9,0,F>, F, .= 0)
(<10,0,A>, 1 + A, .+ 1) (<10,0,B>, B, .= 0) (<10,0,D>, D, .= 0) (<10,0,F>, F, .= 0)
(<11,0,A>, A, .= 0) (<11,0,B>, 1 + B, .+ 1) (<11,0,D>, D, .= 0) (<11,0,F>, F, .= 0)
(<12,0,A>, A, .= 0) (<12,0,B>, 1 + B, .+ 1) (<12,0,D>, D, .= 0) (<12,0,F>, F, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,D,F) -> f3(A,B,D,F) True (1,1)
1. f0(A,B,D,F) -> f4(A,B,D,F) True (1,1)
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
3. f3(A,B,D,F) -> f4(A,B,D,F) [A >= 1 + B] (?,1)
4. f3(A,B,D,F) -> f4(A,B,D,F) [B >= 1 + A] (?,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
8. f3(A,B,D,F) -> f8(O,P,M,N) [A = B] (?,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
10. f4(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (?,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
12. f4(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (?,1)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[0->{3,4,8},1->{10,12},2->{},3->{10,12},4->{10,12},5->{3,4,8},6->{3,4,8},7->{},8->{},9->{3,4,8},10->{3,4
,8},11->{3,4,8},12->{3,4,8}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,D>, ?) (< 0,0,F>, ?)
(< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,D>, ?) (< 1,0,F>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,D>, ?) (< 2,0,F>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,D>, ?) (< 3,0,F>, ?)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,D>, ?) (< 4,0,F>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,D>, ?) (< 5,0,F>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,D>, ?) (< 6,0,F>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,D>, ?) (< 8,0,F>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,D>, ?) (< 9,0,F>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,D>, ?) (<10,0,F>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,D>, ?) (<11,0,F>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,D>, ?) (<12,0,F>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,D>, D) (< 0,0,F>, F)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,D>, D) (< 1,0,F>, F)
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,D>, D) (< 3,0,F>, F)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,D>, D) (< 4,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,D>, ?) (< 8,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,D>, D) (<10,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,D>, D) (<12,0,F>, F)
* Step 4: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,D,F) -> f3(A,B,D,F) True (1,1)
1. f0(A,B,D,F) -> f4(A,B,D,F) True (1,1)
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
3. f3(A,B,D,F) -> f4(A,B,D,F) [A >= 1 + B] (?,1)
4. f3(A,B,D,F) -> f4(A,B,D,F) [B >= 1 + A] (?,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
8. f3(A,B,D,F) -> f8(O,P,M,N) [A = B] (?,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
10. f4(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (?,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
12. f4(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (?,1)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[0->{3,4,8},1->{10,12},2->{},3->{10,12},4->{10,12},5->{3,4,8},6->{3,4,8},7->{},8->{},9->{3,4,8},10->{3,4
,8},11->{3,4,8},12->{3,4,8}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,D>, D) (< 0,0,F>, F)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,D>, D) (< 1,0,F>, F)
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,D>, D) (< 3,0,F>, F)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,D>, D) (< 4,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,D>, ?) (< 8,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,D>, D) (<10,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,D>, D) (<12,0,F>, F)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(3,10),(4,12),(10,3)]
* Step 5: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,D,F) -> f3(A,B,D,F) True (1,1)
1. f0(A,B,D,F) -> f4(A,B,D,F) True (1,1)
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
3. f3(A,B,D,F) -> f4(A,B,D,F) [A >= 1 + B] (?,1)
4. f3(A,B,D,F) -> f4(A,B,D,F) [B >= 1 + A] (?,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
8. f3(A,B,D,F) -> f8(O,P,M,N) [A = B] (?,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
10. f4(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (?,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
12. f4(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (?,1)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[0->{3,4,8},1->{10,12},2->{},3->{12},4->{10},5->{3,4,8},6->{3,4,8},7->{},8->{},9->{3,4,8},10->{4,8},11->{3
,4,8},12->{3,4,8}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,D>, D) (< 0,0,F>, F)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,D>, D) (< 1,0,F>, F)
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,D>, D) (< 3,0,F>, F)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,D>, D) (< 4,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,D>, ?) (< 8,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,D>, D) (<10,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,D>, D) (<12,0,F>, F)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [8]
* Step 6: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,D,F) -> f3(A,B,D,F) True (1,1)
1. f0(A,B,D,F) -> f4(A,B,D,F) True (1,1)
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
3. f3(A,B,D,F) -> f4(A,B,D,F) [A >= 1 + B] (?,1)
4. f3(A,B,D,F) -> f4(A,B,D,F) [B >= 1 + A] (?,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
10. f4(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (?,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
12. f4(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (?,1)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[0->{3,4},1->{10,12},2->{},3->{12},4->{10},5->{3,4},6->{3,4},7->{},9->{3,4},10->{4},11->{3,4},12->{3,4}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,D>, D) (< 0,0,F>, F)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,D>, D) (< 1,0,F>, F)
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,D>, D) (< 3,0,F>, F)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,D>, D) (< 4,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,D>, D) (<10,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,D>, D) (<12,0,F>, F)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [3,12], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f3) = 1 + x1 + -1*x2
p(f4) = 1 + x1 + -1*x2
The following rules are strictly oriented:
[A >= B] ==>
f4(A,B,D,F) = 1 + A + -1*B
> A + -1*B
= f3(A,1 + B,D,F)
The following rules are weakly oriented:
[A >= 1 + B] ==>
f3(A,B,D,F) = 1 + A + -1*B
>= 1 + A + -1*B
= f4(A,B,D,F)
We use the following global sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,D>, D) (< 0,0,F>, F)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,D>, D) (< 1,0,F>, F)
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,D>, D) (< 3,0,F>, F)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,D>, D) (< 4,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,D>, D) (<10,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,D>, D) (<12,0,F>, F)
* Step 7: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,D,F) -> f3(A,B,D,F) True (1,1)
1. f0(A,B,D,F) -> f4(A,B,D,F) True (1,1)
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
3. f3(A,B,D,F) -> f4(A,B,D,F) [A >= 1 + B] (?,1)
4. f3(A,B,D,F) -> f4(A,B,D,F) [B >= 1 + A] (?,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
10. f4(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (?,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
12. f4(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (8 + 4*A + 4*B + 2*D + 2*F,1)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[0->{3,4},1->{10,12},2->{},3->{12},4->{10},5->{3,4},6->{3,4},7->{},9->{3,4},10->{4},11->{3,4},12->{3,4}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,D>, D) (< 0,0,F>, F)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,D>, D) (< 1,0,F>, F)
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,D>, D) (< 3,0,F>, F)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,D>, D) (< 4,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,D>, D) (<10,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,D>, D) (<12,0,F>, F)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 8: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,D,F) -> f3(A,B,D,F) True (1,1)
1. f0(A,B,D,F) -> f4(A,B,D,F) True (1,1)
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
3. f3(A,B,D,F) -> f4(A,B,D,F) [A >= 1 + B] (13 + 4*A + 4*B + 2*D + 2*F,1)
4. f3(A,B,D,F) -> f4(A,B,D,F) [B >= 1 + A] (?,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
10. f4(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (?,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
12. f4(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (8 + 4*A + 4*B + 2*D + 2*F,1)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[0->{3,4},1->{10,12},2->{},3->{12},4->{10},5->{3,4},6->{3,4},7->{},9->{3,4},10->{4},11->{3,4},12->{3,4}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,D>, D) (< 0,0,F>, F)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,D>, D) (< 1,0,F>, F)
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,D>, D) (< 3,0,F>, F)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,D>, D) (< 4,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,D>, D) (<10,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,D>, D) (<12,0,F>, F)
+ Applied Processor:
ChainProcessor False [0,1,2,3,4,5,6,7,9,10,11,12]
+ Details:
We chained rule 0 to obtain the rules [13,14] .
* Step 9: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
1. f0(A,B,D,F) -> f4(A,B,D,F) True (1,1)
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
3. f3(A,B,D,F) -> f4(A,B,D,F) [A >= 1 + B] (13 + 4*A + 4*B + 2*D + 2*F,1)
4. f3(A,B,D,F) -> f4(A,B,D,F) [B >= 1 + A] (?,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
10. f4(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (?,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
12. f4(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (8 + 4*A + 4*B + 2*D + 2*F,1)
13. f0(A,B,D,F) -> f4(A,B,D,F) [A >= 1 + B] (1,2)
14. f0(A,B,D,F) -> f4(A,B,D,F) [B >= 1 + A] (1,2)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[1->{10,12},2->{},3->{10,12},4->{10,12},5->{3,4},6->{3,4},7->{},9->{3,4},10->{3,4},11->{3,4},12->{3,4}
,13->{10,12},14->{10,12}]
Sizebounds:
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,D>, D) (< 1,0,F>, F)
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,D>, D) (< 3,0,F>, F)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,D>, D) (< 4,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,D>, D) (<10,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,D>, D) (<12,0,F>, F)
(<13,0,A>, ?) (<13,0,B>, ?) (<13,0,D>, D) (<13,0,F>, F)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,D>, D) (<14,0,F>, F)
+ Applied Processor:
ChainProcessor False [1,2,3,4,5,6,7,9,10,11,12,13,14]
+ Details:
We chained rule 1 to obtain the rules [15,16] .
* Step 10: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
3. f3(A,B,D,F) -> f4(A,B,D,F) [A >= 1 + B] (13 + 4*A + 4*B + 2*D + 2*F,1)
4. f3(A,B,D,F) -> f4(A,B,D,F) [B >= 1 + A] (?,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
10. f4(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (?,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
12. f4(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (8 + 4*A + 4*B + 2*D + 2*F,1)
13. f0(A,B,D,F) -> f4(A,B,D,F) [A >= 1 + B] (1,2)
14. f0(A,B,D,F) -> f4(A,B,D,F) [B >= 1 + A] (1,2)
15. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (1,2)
16. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (1,2)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[2->{},3->{10,12},4->{10,12},5->{3,4},6->{3,4},7->{},9->{3,4},10->{3,4},11->{3,4},12->{3,4},13->{10,12}
,14->{10,12},15->{3,4},16->{3,4}]
Sizebounds:
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,D>, D) (< 3,0,F>, F)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,D>, D) (< 4,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,D>, D) (<10,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,D>, D) (<12,0,F>, F)
(<13,0,A>, ?) (<13,0,B>, ?) (<13,0,D>, D) (<13,0,F>, F)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,D>, D) (<14,0,F>, F)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,D>, D) (<15,0,F>, F)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,D>, D) (<16,0,F>, F)
+ Applied Processor:
ChainProcessor False [2,3,4,5,6,7,9,10,11,12,13,14,15,16]
+ Details:
We chained rule 3 to obtain the rules [17,18] .
* Step 11: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
4. f3(A,B,D,F) -> f4(A,B,D,F) [B >= 1 + A] (?,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
10. f4(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (?,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
12. f4(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (8 + 4*A + 4*B + 2*D + 2*F,1)
13. f0(A,B,D,F) -> f4(A,B,D,F) [A >= 1 + B] (1,2)
14. f0(A,B,D,F) -> f4(A,B,D,F) [B >= 1 + A] (1,2)
15. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (1,2)
16. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (1,2)
17. f3(A,B,D,F) -> f3(1 + A,B,D,F) [A >= 1 + B && B >= 1 + A] (13 + 4*A + 4*B + 2*D + 2*F,2)
18. f3(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (13 + 4*A + 4*B + 2*D + 2*F,2)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[2->{},4->{10,12},5->{4,17,18},6->{4,17,18},7->{},9->{4,17,18},10->{4,17,18},11->{4,17,18},12->{4,17,18}
,13->{10,12},14->{10,12},15->{4,17,18},16->{4,17,18},17->{4,17,18},18->{4,17,18}]
Sizebounds:
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,D>, D) (< 4,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,D>, D) (<10,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,D>, D) (<12,0,F>, F)
(<13,0,A>, ?) (<13,0,B>, ?) (<13,0,D>, D) (<13,0,F>, F)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,D>, D) (<14,0,F>, F)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,D>, D) (<15,0,F>, F)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,D>, D) (<16,0,F>, F)
(<17,0,A>, ?) (<17,0,B>, ?) (<17,0,D>, D) (<17,0,F>, F)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,D>, D) (<18,0,F>, F)
+ Applied Processor:
ChainProcessor False [2,4,5,6,7,9,10,11,12,13,14,15,16,17,18]
+ Details:
We chained rule 4 to obtain the rules [19,20] .
* Step 12: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
10. f4(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (?,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
12. f4(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (8 + 4*A + 4*B + 2*D + 2*F,1)
13. f0(A,B,D,F) -> f4(A,B,D,F) [A >= 1 + B] (1,2)
14. f0(A,B,D,F) -> f4(A,B,D,F) [B >= 1 + A] (1,2)
15. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (1,2)
16. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (1,2)
17. f3(A,B,D,F) -> f3(1 + A,B,D,F) [A >= 1 + B && B >= 1 + A] (13 + 4*A + 4*B + 2*D + 2*F,2)
18. f3(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (13 + 4*A + 4*B + 2*D + 2*F,2)
19. f3(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A && B >= 1 + A] (?,2)
20. f3(A,B,D,F) -> f3(A,1 + B,D,F) [B >= 1 + A && A >= B] (?,2)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[2->{},5->{17,18,19,20},6->{17,18,19,20},7->{},9->{17,18,19,20},10->{17,18,19,20},11->{17,18,19,20}
,12->{17,18,19,20},13->{10,12},14->{10,12},15->{17,18,19,20},16->{17,18,19,20},17->{17,18,19,20},18->{17,18
,19,20},19->{17,18,19,20},20->{17,18,19,20}]
Sizebounds:
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,D>, D) (<10,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,D>, D) (<12,0,F>, F)
(<13,0,A>, ?) (<13,0,B>, ?) (<13,0,D>, D) (<13,0,F>, F)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,D>, D) (<14,0,F>, F)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,D>, D) (<15,0,F>, F)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,D>, D) (<16,0,F>, F)
(<17,0,A>, ?) (<17,0,B>, ?) (<17,0,D>, D) (<17,0,F>, F)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,D>, D) (<18,0,F>, F)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,D>, D) (<19,0,F>, F)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,D>, D) (<20,0,F>, F)
+ Applied Processor:
ChainProcessor False [2,5,6,7,9,10,11,12,13,14,15,16,17,18,19,20]
+ Details:
We chained rule 13 to obtain the rules [21,22] .
* Step 13: ChainProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
10. f4(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (?,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
12. f4(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (8 + 4*A + 4*B + 2*D + 2*F,1)
14. f0(A,B,D,F) -> f4(A,B,D,F) [B >= 1 + A] (1,2)
15. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (1,2)
16. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (1,2)
17. f3(A,B,D,F) -> f3(1 + A,B,D,F) [A >= 1 + B && B >= 1 + A] (13 + 4*A + 4*B + 2*D + 2*F,2)
18. f3(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (13 + 4*A + 4*B + 2*D + 2*F,2)
19. f3(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A && B >= 1 + A] (?,2)
20. f3(A,B,D,F) -> f3(A,1 + B,D,F) [B >= 1 + A && A >= B] (?,2)
21. f0(A,B,D,F) -> f3(1 + A,B,D,F) [A >= 1 + B && B >= 1 + A] (1,3)
22. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (1,3)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[2->{},5->{17,18,19,20},6->{17,18,19,20},7->{},9->{17,18,19,20},10->{17,18,19,20},11->{17,18,19,20}
,12->{17,18,19,20},14->{10,12},15->{17,18,19,20},16->{17,18,19,20},17->{17,18,19,20},18->{17,18,19,20}
,19->{17,18,19,20},20->{17,18,19,20},21->{17,18,19,20},22->{17,18,19,20}]
Sizebounds:
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,D>, D) (<10,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,D>, D) (<12,0,F>, F)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,D>, D) (<14,0,F>, F)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,D>, D) (<15,0,F>, F)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,D>, D) (<16,0,F>, F)
(<17,0,A>, ?) (<17,0,B>, ?) (<17,0,D>, D) (<17,0,F>, F)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,D>, D) (<18,0,F>, F)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,D>, D) (<19,0,F>, F)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,D>, D) (<20,0,F>, F)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,D>, D) (<21,0,F>, F)
(<22,0,A>, ?) (<22,0,B>, ?) (<22,0,D>, D) (<22,0,F>, F)
+ Applied Processor:
ChainProcessor False [2,5,6,7,9,10,11,12,14,15,16,17,18,19,20,21,22]
+ Details:
We chained rule 14 to obtain the rules [23,24] .
* Step 14: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
10. f4(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (?,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
12. f4(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (8 + 4*A + 4*B + 2*D + 2*F,1)
15. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (1,2)
16. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (1,2)
17. f3(A,B,D,F) -> f3(1 + A,B,D,F) [A >= 1 + B && B >= 1 + A] (13 + 4*A + 4*B + 2*D + 2*F,2)
18. f3(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (13 + 4*A + 4*B + 2*D + 2*F,2)
19. f3(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A && B >= 1 + A] (?,2)
20. f3(A,B,D,F) -> f3(A,1 + B,D,F) [B >= 1 + A && A >= B] (?,2)
21. f0(A,B,D,F) -> f3(1 + A,B,D,F) [A >= 1 + B && B >= 1 + A] (1,3)
22. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (1,3)
23. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A && B >= 1 + A] (1,3)
24. f0(A,B,D,F) -> f3(A,1 + B,D,F) [B >= 1 + A && A >= B] (1,3)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[2->{},5->{17,18,19,20},6->{17,18,19,20},7->{},9->{17,18,19,20},10->{17,18,19,20},11->{17,18,19,20}
,12->{17,18,19,20},15->{17,18,19,20},16->{17,18,19,20},17->{17,18,19,20},18->{17,18,19,20},19->{17,18,19,20}
,20->{17,18,19,20},21->{17,18,19,20},22->{17,18,19,20},23->{17,18,19,20},24->{17,18,19,20}]
Sizebounds:
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,D>, D) (<10,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,D>, D) (<12,0,F>, F)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,D>, D) (<15,0,F>, F)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,D>, D) (<16,0,F>, F)
(<17,0,A>, ?) (<17,0,B>, ?) (<17,0,D>, D) (<17,0,F>, F)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,D>, D) (<18,0,F>, F)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,D>, D) (<19,0,F>, F)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,D>, D) (<20,0,F>, F)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,D>, D) (<21,0,F>, F)
(<22,0,A>, ?) (<22,0,B>, ?) (<22,0,D>, D) (<22,0,F>, F)
(<23,0,A>, ?) (<23,0,B>, ?) (<23,0,D>, D) (<23,0,F>, F)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,D>, D) (<24,0,F>, F)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [10,12]
* Step 15: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
15. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (1,2)
16. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (1,2)
17. f3(A,B,D,F) -> f3(1 + A,B,D,F) [A >= 1 + B && B >= 1 + A] (13 + 4*A + 4*B + 2*D + 2*F,2)
18. f3(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (13 + 4*A + 4*B + 2*D + 2*F,2)
19. f3(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A && B >= 1 + A] (?,2)
20. f3(A,B,D,F) -> f3(A,1 + B,D,F) [B >= 1 + A && A >= B] (?,2)
21. f0(A,B,D,F) -> f3(1 + A,B,D,F) [A >= 1 + B && B >= 1 + A] (1,3)
22. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (1,3)
23. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A && B >= 1 + A] (1,3)
24. f0(A,B,D,F) -> f3(A,1 + B,D,F) [B >= 1 + A && A >= B] (1,3)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[2->{},5->{17,18,19,20},6->{17,18,19,20},7->{},9->{17,18,19,20},11->{17,18,19,20},15->{17,18,19,20}
,16->{17,18,19,20},17->{17,18,19,20},18->{17,18,19,20},19->{17,18,19,20},20->{17,18,19,20},21->{17,18,19,20}
,22->{17,18,19,20},23->{17,18,19,20},24->{17,18,19,20}]
Sizebounds:
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,D>, D) (<15,0,F>, F)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,D>, D) (<16,0,F>, F)
(<17,0,A>, ?) (<17,0,B>, ?) (<17,0,D>, D) (<17,0,F>, F)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,D>, D) (<18,0,F>, F)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,D>, D) (<19,0,F>, F)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,D>, D) (<20,0,F>, F)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,D>, D) (<21,0,F>, F)
(<22,0,A>, ?) (<22,0,B>, ?) (<22,0,D>, D) (<22,0,F>, F)
(<23,0,A>, ?) (<23,0,B>, ?) (<23,0,D>, D) (<23,0,F>, F)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,D>, D) (<24,0,F>, F)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(5,17)
,(5,20)
,(6,17)
,(6,20)
,(9,17)
,(9,20)
,(11,17)
,(11,20)
,(15,17)
,(15,18)
,(15,20)
,(16,17)
,(16,20)
,(17,17)
,(17,18)
,(17,19)
,(17,20)
,(18,17)
,(18,19)
,(18,20)
,(19,17)
,(19,18)
,(19,20)
,(20,17)
,(20,18)
,(20,19)
,(20,20)
,(21,17)
,(21,18)
,(21,19)
,(21,20)
,(22,17)
,(22,19)
,(22,20)
,(23,17)
,(23,18)
,(23,20)
,(24,17)
,(24,18)
,(24,19)
,(24,20)]
* Step 16: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
15. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (1,2)
16. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (1,2)
17. f3(A,B,D,F) -> f3(1 + A,B,D,F) [A >= 1 + B && B >= 1 + A] (13 + 4*A + 4*B + 2*D + 2*F,2)
18. f3(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (13 + 4*A + 4*B + 2*D + 2*F,2)
19. f3(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A && B >= 1 + A] (?,2)
20. f3(A,B,D,F) -> f3(A,1 + B,D,F) [B >= 1 + A && A >= B] (?,2)
21. f0(A,B,D,F) -> f3(1 + A,B,D,F) [A >= 1 + B && B >= 1 + A] (1,3)
22. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (1,3)
23. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A && B >= 1 + A] (1,3)
24. f0(A,B,D,F) -> f3(A,1 + B,D,F) [B >= 1 + A && A >= B] (1,3)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[2->{},5->{18,19},6->{18,19},7->{},9->{18,19},11->{18,19},15->{19},16->{18,19},17->{},18->{18},19->{19}
,20->{},21->{},22->{18},23->{19},24->{}]
Sizebounds:
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,D>, D) (<15,0,F>, F)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,D>, D) (<16,0,F>, F)
(<17,0,A>, ?) (<17,0,B>, ?) (<17,0,D>, D) (<17,0,F>, F)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,D>, D) (<18,0,F>, F)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,D>, D) (<19,0,F>, F)
(<20,0,A>, ?) (<20,0,B>, ?) (<20,0,D>, D) (<20,0,F>, F)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,D>, D) (<21,0,F>, F)
(<22,0,A>, ?) (<22,0,B>, ?) (<22,0,D>, D) (<22,0,F>, F)
(<23,0,A>, ?) (<23,0,B>, ?) (<23,0,D>, D) (<23,0,F>, F)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,D>, D) (<24,0,F>, F)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [17,20]
* Step 17: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
15. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (1,2)
16. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (1,2)
18. f3(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (13 + 4*A + 4*B + 2*D + 2*F,2)
19. f3(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A && B >= 1 + A] (?,2)
21. f0(A,B,D,F) -> f3(1 + A,B,D,F) [A >= 1 + B && B >= 1 + A] (1,3)
22. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (1,3)
23. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A && B >= 1 + A] (1,3)
24. f0(A,B,D,F) -> f3(A,1 + B,D,F) [B >= 1 + A && A >= B] (1,3)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[2->{},5->{18,19},6->{18,19},7->{},9->{18,19},11->{18,19},15->{19},16->{18,19},18->{18},19->{19},21->{}
,22->{18},23->{19},24->{}]
Sizebounds:
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,D>, D) (<15,0,F>, F)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,D>, D) (<16,0,F>, F)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,D>, D) (<18,0,F>, F)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,D>, D) (<19,0,F>, F)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,D>, D) (<21,0,F>, F)
(<22,0,A>, ?) (<22,0,B>, ?) (<22,0,D>, D) (<22,0,F>, F)
(<23,0,A>, ?) (<23,0,B>, ?) (<23,0,D>, D) (<23,0,F>, F)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,D>, D) (<24,0,F>, F)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0) (< 2,0,D>, D, .= 0) (< 2,0,F>, F, .= 0)
(< 5,0,A>, F, .= 0) (< 5,0,B>, D, .= 0) (< 5,0,D>, D, .= 0) (< 5,0,F>, F, .= 0)
(< 6,0,A>, F, .= 0) (< 6,0,B>, D, .= 0) (< 6,0,D>, D, .= 0) (< 6,0,F>, F, .= 0)
(< 7,0,A>, ?, .?) (< 7,0,B>, ?, .?) (< 7,0,D>, ?, .?) (< 7,0,F>, ?, .?)
(< 9,0,A>, 1 + A, .+ 1) (< 9,0,B>, B, .= 0) (< 9,0,D>, D, .= 0) (< 9,0,F>, F, .= 0)
(<11,0,A>, A, .= 0) (<11,0,B>, 1 + B, .+ 1) (<11,0,D>, D, .= 0) (<11,0,F>, F, .= 0)
(<15,0,A>, 1 + A, .+ 1) (<15,0,B>, B, .= 0) (<15,0,D>, D, .= 0) (<15,0,F>, F, .= 0)
(<16,0,A>, A, .= 0) (<16,0,B>, 1 + B, .+ 1) (<16,0,D>, D, .= 0) (<16,0,F>, F, .= 0)
(<18,0,A>, A, .= 0) (<18,0,B>, 1 + B, .+ 1) (<18,0,D>, D, .= 0) (<18,0,F>, F, .= 0)
(<19,0,A>, 1 + A, .+ 1) (<19,0,B>, B, .= 0) (<19,0,D>, D, .= 0) (<19,0,F>, F, .= 0)
(<21,0,A>, 1 + A, .+ 1) (<21,0,B>, B, .= 0) (<21,0,D>, D, .= 0) (<21,0,F>, F, .= 0)
(<22,0,A>, A, .= 0) (<22,0,B>, 1 + B, .+ 1) (<22,0,D>, D, .= 0) (<22,0,F>, F, .= 0)
(<23,0,A>, 1 + A, .+ 1) (<23,0,B>, B, .= 0) (<23,0,D>, D, .= 0) (<23,0,F>, F, .= 0)
(<24,0,A>, A, .= 0) (<24,0,B>, 1 + B, .+ 1) (<24,0,D>, D, .= 0) (<24,0,F>, F, .= 0)
* Step 18: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
15. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (1,2)
16. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (1,2)
18. f3(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (13 + 4*A + 4*B + 2*D + 2*F,2)
19. f3(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A && B >= 1 + A] (?,2)
21. f0(A,B,D,F) -> f3(1 + A,B,D,F) [A >= 1 + B && B >= 1 + A] (1,3)
22. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (1,3)
23. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A && B >= 1 + A] (1,3)
24. f0(A,B,D,F) -> f3(A,1 + B,D,F) [B >= 1 + A && A >= B] (1,3)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[2->{},5->{18,19},6->{18,19},7->{},9->{18,19},11->{18,19},15->{19},16->{18,19},18->{18},19->{19},21->{}
,22->{18},23->{19},24->{}]
Sizebounds:
(< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,D>, ?) (< 2,0,F>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,D>, ?) (< 5,0,F>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,D>, ?) (< 6,0,F>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,D>, ?) (< 9,0,F>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,D>, ?) (<11,0,F>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,D>, ?) (<15,0,F>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,D>, ?) (<16,0,F>, ?)
(<18,0,A>, ?) (<18,0,B>, ?) (<18,0,D>, ?) (<18,0,F>, ?)
(<19,0,A>, ?) (<19,0,B>, ?) (<19,0,D>, ?) (<19,0,F>, ?)
(<21,0,A>, ?) (<21,0,B>, ?) (<21,0,D>, ?) (<21,0,F>, ?)
(<22,0,A>, ?) (<22,0,B>, ?) (<22,0,D>, ?) (<22,0,F>, ?)
(<23,0,A>, ?) (<23,0,B>, ?) (<23,0,D>, ?) (<23,0,F>, ?)
(<24,0,A>, ?) (<24,0,B>, ?) (<24,0,D>, ?) (<24,0,F>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<15,0,A>, 1 + A) (<15,0,B>, B) (<15,0,D>, D) (<15,0,F>, F)
(<16,0,A>, A) (<16,0,B>, 1 + B) (<16,0,D>, D) (<16,0,F>, F)
(<18,0,A>, 1 + A + F) (<18,0,B>, 14 + 4*A + 5*B + 3*D + 2*F) (<18,0,D>, D) (<18,0,F>, F)
(<19,0,A>, 1 + B + D) (<19,0,B>, 1 + B + D) (<19,0,D>, D) (<19,0,F>, F)
(<21,0,A>, 1 + A) (<21,0,B>, B) (<21,0,D>, D) (<21,0,F>, F)
(<22,0,A>, A) (<22,0,B>, 1 + B) (<22,0,D>, D) (<22,0,F>, F)
(<23,0,A>, 1 + A) (<23,0,B>, B) (<23,0,D>, D) (<23,0,F>, F)
(<24,0,A>, A) (<24,0,B>, 1 + B) (<24,0,D>, D) (<24,0,F>, F)
* Step 19: LocationConstraintsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
15. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (1,2)
16. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (1,2)
18. f3(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (13 + 4*A + 4*B + 2*D + 2*F,2)
19. f3(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A && B >= 1 + A] (?,2)
21. f0(A,B,D,F) -> f3(1 + A,B,D,F) [A >= 1 + B && B >= 1 + A] (1,3)
22. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (1,3)
23. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A && B >= 1 + A] (1,3)
24. f0(A,B,D,F) -> f3(A,1 + B,D,F) [B >= 1 + A && A >= B] (1,3)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[2->{},5->{18,19},6->{18,19},7->{},9->{18,19},11->{18,19},15->{19},16->{18,19},18->{18},19->{19},21->{}
,22->{18},23->{19},24->{}]
Sizebounds:
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<15,0,A>, 1 + A) (<15,0,B>, B) (<15,0,D>, D) (<15,0,F>, F)
(<16,0,A>, A) (<16,0,B>, 1 + B) (<16,0,D>, D) (<16,0,F>, F)
(<18,0,A>, 1 + A + F) (<18,0,B>, 14 + 4*A + 5*B + 3*D + 2*F) (<18,0,D>, D) (<18,0,F>, F)
(<19,0,A>, 1 + B + D) (<19,0,B>, 1 + B + D) (<19,0,D>, D) (<19,0,F>, F)
(<21,0,A>, 1 + A) (<21,0,B>, B) (<21,0,D>, D) (<21,0,F>, F)
(<22,0,A>, A) (<22,0,B>, 1 + B) (<22,0,D>, D) (<22,0,F>, F)
(<23,0,A>, 1 + A) (<23,0,B>, B) (<23,0,D>, D) (<23,0,F>, F)
(<24,0,A>, A) (<24,0,B>, 1 + B) (<24,0,D>, D) (<24,0,F>, F)
+ Applied Processor:
LocationConstraintsProc
+ Details:
We computed the location constraints 2 : True 5 : True 6 : True 7 : True 9 : True 11 : True 15 : True 16 : True 18 : True 19 : True 21 : True 22 : True 23 : True 24 : True .
* Step 20: LoopRecurrenceProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
15. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (1,2)
16. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (1,2)
18. f3(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (13 + 4*A + 4*B + 2*D + 2*F,2)
19. f3(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A && B >= 1 + A] (?,2)
21. f0(A,B,D,F) -> f3(1 + A,B,D,F) [A >= 1 + B && B >= 1 + A] (1,3)
22. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (1,3)
23. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A && B >= 1 + A] (1,3)
24. f0(A,B,D,F) -> f3(A,1 + B,D,F) [B >= 1 + A && A >= B] (1,3)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[2->{},5->{18,19},6->{18,19},7->{},9->{18,19},11->{18,19},15->{19},16->{18,19},18->{18},19->{19},21->{}
,22->{18},23->{19},24->{}]
Sizebounds:
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<15,0,A>, 1 + A) (<15,0,B>, B) (<15,0,D>, D) (<15,0,F>, F)
(<16,0,A>, A) (<16,0,B>, 1 + B) (<16,0,D>, D) (<16,0,F>, F)
(<18,0,A>, 1 + A + F) (<18,0,B>, 14 + 4*A + 5*B + 3*D + 2*F) (<18,0,D>, D) (<18,0,F>, F)
(<19,0,A>, 1 + B + D) (<19,0,B>, 1 + B + D) (<19,0,D>, D) (<19,0,F>, F)
(<21,0,A>, 1 + A) (<21,0,B>, B) (<21,0,D>, D) (<21,0,F>, F)
(<22,0,A>, A) (<22,0,B>, 1 + B) (<22,0,D>, D) (<22,0,F>, F)
(<23,0,A>, 1 + A) (<23,0,B>, B) (<23,0,D>, D) (<23,0,F>, F)
(<24,0,A>, A) (<24,0,B>, 1 + B) (<24,0,D>, D) (<24,0,F>, F)
+ Applied Processor:
LoopRecurrenceProcessor [19]
+ Details:
Applying the recurrence pattern linear * f to the expression B-A yields the solution -1*A + B .
* Step 21: LoopRecurrenceProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
15. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (1,2)
16. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (1,2)
18. f3(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (13 + 4*A + 4*B + 2*D + 2*F,2)
19. f3(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A && B >= 1 + A] (5 + 5*A + 5*B + 2*D + 2*F,2)
21. f0(A,B,D,F) -> f3(1 + A,B,D,F) [A >= 1 + B && B >= 1 + A] (1,3)
22. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (1,3)
23. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A && B >= 1 + A] (1,3)
24. f0(A,B,D,F) -> f3(A,1 + B,D,F) [B >= 1 + A && A >= B] (1,3)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[2->{},5->{18,19},6->{18,19},7->{},9->{18,19},11->{18,19},15->{19},16->{18,19},18->{18},19->{19},21->{}
,22->{18},23->{19},24->{}]
Sizebounds:
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<15,0,A>, 1 + A) (<15,0,B>, B) (<15,0,D>, D) (<15,0,F>, F)
(<16,0,A>, A) (<16,0,B>, 1 + B) (<16,0,D>, D) (<16,0,F>, F)
(<18,0,A>, 1 + A + F) (<18,0,B>, 14 + 4*A + 5*B + 3*D + 2*F) (<18,0,D>, D) (<18,0,F>, F)
(<19,0,A>, 1 + B + D) (<19,0,B>, 1 + B + D) (<19,0,D>, D) (<19,0,F>, F)
(<21,0,A>, 1 + A) (<21,0,B>, B) (<21,0,D>, D) (<21,0,F>, F)
(<22,0,A>, A) (<22,0,B>, 1 + B) (<22,0,D>, D) (<22,0,F>, F)
(<23,0,A>, 1 + A) (<23,0,B>, B) (<23,0,D>, D) (<23,0,F>, F)
(<24,0,A>, A) (<24,0,B>, 1 + B) (<24,0,D>, D) (<24,0,F>, F)
+ Applied Processor:
LoopRecurrenceProcessor [18]
+ Details:
Applying the recurrence pattern linear * f to the expression A-B yields the solution A + -1*B .
* Step 22: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
2. f0(A,B,D,F) -> f8(A,B,D,F) True (1,1)
5. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
6. f0(A,B,D,F) -> f3(F,D,D,F) True (1,1)
7. f0(A,B,D,F) -> f8(O,P,M,N) True (1,1)
9. f0(A,B,D,F) -> f3(1 + A,B,D,F) True (1,1)
11. f0(A,B,D,F) -> f3(A,1 + B,D,F) True (1,1)
15. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A] (1,2)
16. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= B] (1,2)
18. f3(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (4 + 4*A + 4*B + 2*D + 2*F,2)
19. f3(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A && B >= 1 + A] (5 + 5*A + 5*B + 2*D + 2*F,2)
21. f0(A,B,D,F) -> f3(1 + A,B,D,F) [A >= 1 + B && B >= 1 + A] (1,3)
22. f0(A,B,D,F) -> f3(A,1 + B,D,F) [A >= 1 + B && A >= B] (1,3)
23. f0(A,B,D,F) -> f3(1 + A,B,D,F) [B >= 1 + A && B >= 1 + A] (1,3)
24. f0(A,B,D,F) -> f3(A,1 + B,D,F) [B >= 1 + A && A >= B] (1,3)
Signature:
{(f0,4);(f3,4);(f4,4);(f8,4)}
Flow Graph:
[2->{},5->{18,19},6->{18,19},7->{},9->{18,19},11->{18,19},15->{19},16->{18,19},18->{18},19->{19},21->{}
,22->{18},23->{19},24->{}]
Sizebounds:
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,D>, D) (< 2,0,F>, F)
(< 5,0,A>, F) (< 5,0,B>, D) (< 5,0,D>, D) (< 5,0,F>, F)
(< 6,0,A>, F) (< 6,0,B>, D) (< 6,0,D>, D) (< 6,0,F>, F)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,D>, ?) (< 7,0,F>, ?)
(< 9,0,A>, 1 + A) (< 9,0,B>, B) (< 9,0,D>, D) (< 9,0,F>, F)
(<11,0,A>, A) (<11,0,B>, 1 + B) (<11,0,D>, D) (<11,0,F>, F)
(<15,0,A>, 1 + A) (<15,0,B>, B) (<15,0,D>, D) (<15,0,F>, F)
(<16,0,A>, A) (<16,0,B>, 1 + B) (<16,0,D>, D) (<16,0,F>, F)
(<18,0,A>, 1 + A + F) (<18,0,B>, 14 + 4*A + 5*B + 3*D + 2*F) (<18,0,D>, D) (<18,0,F>, F)
(<19,0,A>, 1 + B + D) (<19,0,B>, 1 + B + D) (<19,0,D>, D) (<19,0,F>, F)
(<21,0,A>, 1 + A) (<21,0,B>, B) (<21,0,D>, D) (<21,0,F>, F)
(<22,0,A>, A) (<22,0,B>, 1 + B) (<22,0,D>, D) (<22,0,F>, F)
(<23,0,A>, 1 + A) (<23,0,B>, B) (<23,0,D>, D) (<23,0,F>, F)
(<24,0,A>, A) (<24,0,B>, 1 + B) (<24,0,D>, D) (<24,0,F>, F)
+ Applied Processor:
UnsatPaths
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))