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