WORST_CASE(?,O(n^2))
* Step 1: RestrictVarsProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E,F,G) -> f10(H,0,C,D,E,F,G) True (1,1)
1. f10(A,B,C,D,E,F,G) -> f10(A,1 + B,C,D,E,F,G) [C >= 1 + B] (?,1)
2. f18(A,B,C,D,E,F,G) -> f21(A,B,C,D,E,0,G) [D >= 2 + E] (?,1)
3. f21(A,B,C,D,E,F,G) -> f21(A,B,C,D,E,1 + F,G) [D >= 2 + E + F] (?,1)
4. f21(A,B,C,D,E,F,G) -> f21(A,B,C,D,E,1 + F,H) [D >= 2 + E + F] (?,1)
5. f32(A,B,C,D,E,F,G) -> f32(A,B,C,D,1 + E,F,G) [D >= 2 + E] (?,1)
6. f32(A,B,C,D,E,F,G) -> f41(A,B,C,D,E,F,G) [1 + E >= D] (?,1)
7. f21(A,B,C,D,E,F,G) -> f18(A,B,C,D,1 + E,F,G) [1 + E + F >= D] (?,1)
8. f18(A,B,C,D,E,F,G) -> f32(A,B,C,D,0,F,G) [1 + E >= D] (?,1)
9. f10(A,B,C,D,E,F,G) -> f18(A,B,C,C,0,F,G) [B >= C] (?,1)
Signature:
{(f0,7);(f10,7);(f18,7);(f21,7);(f32,7);(f41,7)}
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,G] .
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. f0(B,C,D,E,F) -> f10(0,C,D,E,F) True (1,1)
1. f10(B,C,D,E,F) -> f10(1 + B,C,D,E,F) [C >= 1 + B] (?,1)
2. f18(B,C,D,E,F) -> f21(B,C,D,E,0) [D >= 2 + E] (?,1)
3. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
4. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
5. f32(B,C,D,E,F) -> f32(B,C,D,1 + E,F) [D >= 2 + E] (?,1)
6. f32(B,C,D,E,F) -> f41(B,C,D,E,F) [1 + E >= D] (?,1)
7. f21(B,C,D,E,F) -> f18(B,C,D,1 + E,F) [1 + E + F >= D] (?,1)
8. f18(B,C,D,E,F) -> f32(B,C,D,0,F) [1 + E >= D] (?,1)
9. f10(B,C,D,E,F) -> f18(B,C,C,0,F) [B >= C] (?,1)
Signature:
{(f0,5);(f10,5);(f18,5);(f21,5);(f32,5);(f41,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,F>, F, .= 0)
(<1,0,B>, 1 + B, .+ 1) (<1,0,C>, C, .= 0) (<1,0,D>, D, .= 0) (<1,0,E>, E, .= 0) (<1,0,F>, F, .= 0)
(<2,0,B>, B, .= 0) (<2,0,C>, C, .= 0) (<2,0,D>, D, .= 0) (<2,0,E>, E, .= 0) (<2,0,F>, 0, .= 0)
(<3,0,B>, B, .= 0) (<3,0,C>, C, .= 0) (<3,0,D>, D, .= 0) (<3,0,E>, E, .= 0) (<3,0,F>, 1 + F, .+ 1)
(<4,0,B>, B, .= 0) (<4,0,C>, C, .= 0) (<4,0,D>, D, .= 0) (<4,0,E>, E, .= 0) (<4,0,F>, 1 + F, .+ 1)
(<5,0,B>, B, .= 0) (<5,0,C>, C, .= 0) (<5,0,D>, D, .= 0) (<5,0,E>, 1 + E, .+ 1) (<5,0,F>, F, .= 0)
(<6,0,B>, B, .= 0) (<6,0,C>, C, .= 0) (<6,0,D>, D, .= 0) (<6,0,E>, E, .= 0) (<6,0,F>, F, .= 0)
(<7,0,B>, B, .= 0) (<7,0,C>, C, .= 0) (<7,0,D>, D, .= 0) (<7,0,E>, 1 + E, .+ 1) (<7,0,F>, F, .= 0)
(<8,0,B>, B, .= 0) (<8,0,C>, C, .= 0) (<8,0,D>, D, .= 0) (<8,0,E>, 0, .= 0) (<8,0,F>, F, .= 0)
(<9,0,B>, B, .= 0) (<9,0,C>, C, .= 0) (<9,0,D>, C, .= 0) (<9,0,E>, 0, .= 0) (<9,0,F>, F, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. f0(B,C,D,E,F) -> f10(0,C,D,E,F) True (1,1)
1. f10(B,C,D,E,F) -> f10(1 + B,C,D,E,F) [C >= 1 + B] (?,1)
2. f18(B,C,D,E,F) -> f21(B,C,D,E,0) [D >= 2 + E] (?,1)
3. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
4. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
5. f32(B,C,D,E,F) -> f32(B,C,D,1 + E,F) [D >= 2 + E] (?,1)
6. f32(B,C,D,E,F) -> f41(B,C,D,E,F) [1 + E >= D] (?,1)
7. f21(B,C,D,E,F) -> f18(B,C,D,1 + E,F) [1 + E + F >= D] (?,1)
8. f18(B,C,D,E,F) -> f32(B,C,D,0,F) [1 + E >= D] (?,1)
9. f10(B,C,D,E,F) -> f18(B,C,C,0,F) [B >= C] (?,1)
Signature:
{(f0,5);(f10,5);(f18,5);(f21,5);(f32,5);(f41,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,F>, ?)
(<1,0,B>, ?) (<1,0,C>, ?) (<1,0,D>, ?) (<1,0,E>, ?) (<1,0,F>, ?)
(<2,0,B>, ?) (<2,0,C>, ?) (<2,0,D>, ?) (<2,0,E>, ?) (<2,0,F>, ?)
(<3,0,B>, ?) (<3,0,C>, ?) (<3,0,D>, ?) (<3,0,E>, ?) (<3,0,F>, ?)
(<4,0,B>, ?) (<4,0,C>, ?) (<4,0,D>, ?) (<4,0,E>, ?) (<4,0,F>, ?)
(<5,0,B>, ?) (<5,0,C>, ?) (<5,0,D>, ?) (<5,0,E>, ?) (<5,0,F>, ?)
(<6,0,B>, ?) (<6,0,C>, ?) (<6,0,D>, ?) (<6,0,E>, ?) (<6,0,F>, ?)
(<7,0,B>, ?) (<7,0,C>, ?) (<7,0,D>, ?) (<7,0,E>, ?) (<7,0,F>, ?)
(<8,0,B>, ?) (<8,0,C>, ?) (<8,0,D>, ?) (<8,0,E>, ?) (<8,0,F>, ?)
(<9,0,B>, ?) (<9,0,C>, ?) (<9,0,D>, ?) (<9,0,E>, ?) (<9,0,F>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<0,0,B>, 0) (<0,0,C>, C) (<0,0,D>, D) (<0,0,E>, E) (<0,0,F>, F)
(<1,0,B>, C) (<1,0,C>, C) (<1,0,D>, D) (<1,0,E>, E) (<1,0,F>, F)
(<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, C) (<2,0,E>, C) (<2,0,F>, 0)
(<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, C) (<3,0,E>, C) (<3,0,F>, C)
(<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, C) (<4,0,E>, C) (<4,0,F>, C)
(<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, C) (<5,0,E>, C) (<5,0,F>, C + F)
(<6,0,B>, ?) (<6,0,C>, C) (<6,0,D>, C) (<6,0,E>, C) (<6,0,F>, C + F)
(<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, C) (<7,0,E>, C) (<7,0,F>, C)
(<8,0,B>, ?) (<8,0,C>, C) (<8,0,D>, C) (<8,0,E>, 0) (<8,0,F>, C + F)
(<9,0,B>, C) (<9,0,C>, C) (<9,0,D>, C) (<9,0,E>, 0) (<9,0,F>, F)
* Step 4: UnsatPaths WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. f0(B,C,D,E,F) -> f10(0,C,D,E,F) True (1,1)
1. f10(B,C,D,E,F) -> f10(1 + B,C,D,E,F) [C >= 1 + B] (?,1)
2. f18(B,C,D,E,F) -> f21(B,C,D,E,0) [D >= 2 + E] (?,1)
3. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
4. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
5. f32(B,C,D,E,F) -> f32(B,C,D,1 + E,F) [D >= 2 + E] (?,1)
6. f32(B,C,D,E,F) -> f41(B,C,D,E,F) [1 + E >= D] (?,1)
7. f21(B,C,D,E,F) -> f18(B,C,D,1 + E,F) [1 + E + F >= D] (?,1)
8. f18(B,C,D,E,F) -> f32(B,C,D,0,F) [1 + E >= D] (?,1)
9. f10(B,C,D,E,F) -> f18(B,C,C,0,F) [B >= C] (?,1)
Signature:
{(f0,5);(f10,5);(f18,5);(f21,5);(f32,5);(f41,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,F>, F)
(<1,0,B>, C) (<1,0,C>, C) (<1,0,D>, D) (<1,0,E>, E) (<1,0,F>, F)
(<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, C) (<2,0,E>, C) (<2,0,F>, 0)
(<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, C) (<3,0,E>, C) (<3,0,F>, C)
(<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, C) (<4,0,E>, C) (<4,0,F>, C)
(<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, C) (<5,0,E>, C) (<5,0,F>, C + F)
(<6,0,B>, ?) (<6,0,C>, C) (<6,0,D>, C) (<6,0,E>, C) (<6,0,F>, C + F)
(<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, C) (<7,0,E>, C) (<7,0,F>, C)
(<8,0,B>, ?) (<8,0,C>, C) (<8,0,D>, C) (<8,0,E>, 0) (<8,0,F>, C + F)
(<9,0,B>, C) (<9,0,C>, C) (<9,0,D>, C) (<9,0,E>, 0) (<9,0,F>, F)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(2,7)]
* Step 5: LeafRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. f0(B,C,D,E,F) -> f10(0,C,D,E,F) True (1,1)
1. f10(B,C,D,E,F) -> f10(1 + B,C,D,E,F) [C >= 1 + B] (?,1)
2. f18(B,C,D,E,F) -> f21(B,C,D,E,0) [D >= 2 + E] (?,1)
3. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
4. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
5. f32(B,C,D,E,F) -> f32(B,C,D,1 + E,F) [D >= 2 + E] (?,1)
6. f32(B,C,D,E,F) -> f41(B,C,D,E,F) [1 + E >= D] (?,1)
7. f21(B,C,D,E,F) -> f18(B,C,D,1 + E,F) [1 + E + F >= D] (?,1)
8. f18(B,C,D,E,F) -> f32(B,C,D,0,F) [1 + E >= D] (?,1)
9. f10(B,C,D,E,F) -> f18(B,C,C,0,F) [B >= C] (?,1)
Signature:
{(f0,5);(f10,5);(f18,5);(f21,5);(f32,5);(f41,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,F>, F)
(<1,0,B>, C) (<1,0,C>, C) (<1,0,D>, D) (<1,0,E>, E) (<1,0,F>, F)
(<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, C) (<2,0,E>, C) (<2,0,F>, 0)
(<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, C) (<3,0,E>, C) (<3,0,F>, C)
(<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, C) (<4,0,E>, C) (<4,0,F>, C)
(<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, C) (<5,0,E>, C) (<5,0,F>, C + F)
(<6,0,B>, ?) (<6,0,C>, C) (<6,0,D>, C) (<6,0,E>, C) (<6,0,F>, C + F)
(<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, C) (<7,0,E>, C) (<7,0,F>, C)
(<8,0,B>, ?) (<8,0,C>, C) (<8,0,D>, C) (<8,0,E>, 0) (<8,0,F>, C + F)
(<9,0,B>, C) (<9,0,C>, C) (<9,0,D>, C) (<9,0,E>, 0) (<9,0,F>, F)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [6]
* Step 6: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. f0(B,C,D,E,F) -> f10(0,C,D,E,F) True (1,1)
1. f10(B,C,D,E,F) -> f10(1 + B,C,D,E,F) [C >= 1 + B] (?,1)
2. f18(B,C,D,E,F) -> f21(B,C,D,E,0) [D >= 2 + E] (?,1)
3. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
4. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
5. f32(B,C,D,E,F) -> f32(B,C,D,1 + E,F) [D >= 2 + E] (?,1)
7. f21(B,C,D,E,F) -> f18(B,C,D,1 + E,F) [1 + E + F >= D] (?,1)
8. f18(B,C,D,E,F) -> f32(B,C,D,0,F) [1 + E >= D] (?,1)
9. f10(B,C,D,E,F) -> f18(B,C,C,0,F) [B >= C] (?,1)
Signature:
{(f0,5);(f10,5);(f18,5);(f21,5);(f32,5);(f41,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,F>, F)
(<1,0,B>, C) (<1,0,C>, C) (<1,0,D>, D) (<1,0,E>, E) (<1,0,F>, F)
(<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, C) (<2,0,E>, C) (<2,0,F>, 0)
(<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, C) (<3,0,E>, C) (<3,0,F>, C)
(<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, C) (<4,0,E>, C) (<4,0,F>, C)
(<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, C) (<5,0,E>, C) (<5,0,F>, C + F)
(<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, C) (<7,0,E>, C) (<7,0,F>, C)
(<8,0,B>, ?) (<8,0,C>, C) (<8,0,D>, C) (<8,0,E>, 0) (<8,0,F>, C + F)
(<9,0,B>, C) (<9,0,C>, C) (<9,0,D>, C) (<9,0,E>, 0) (<9,0,F>, F)
+ 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(f21) = 0
p(f32) = 0
The following rules are strictly oriented:
[B >= C] ==>
f10(B,C,D,E,F) = 1
> 0
= f18(B,C,C,0,F)
The following rules are weakly oriented:
True ==>
f0(B,C,D,E,F) = 1
>= 1
= f10(0,C,D,E,F)
[C >= 1 + B] ==>
f10(B,C,D,E,F) = 1
>= 1
= f10(1 + B,C,D,E,F)
[D >= 2 + E] ==>
f18(B,C,D,E,F) = 0
>= 0
= f21(B,C,D,E,0)
[D >= 2 + E + F] ==>
f21(B,C,D,E,F) = 0
>= 0
= f21(B,C,D,E,1 + F)
[D >= 2 + E + F] ==>
f21(B,C,D,E,F) = 0
>= 0
= f21(B,C,D,E,1 + F)
[D >= 2 + E] ==>
f32(B,C,D,E,F) = 0
>= 0
= f32(B,C,D,1 + E,F)
[1 + E + F >= D] ==>
f21(B,C,D,E,F) = 0
>= 0
= f18(B,C,D,1 + E,F)
[1 + E >= D] ==>
f18(B,C,D,E,F) = 0
>= 0
= f32(B,C,D,0,F)
* Step 7: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. f0(B,C,D,E,F) -> f10(0,C,D,E,F) True (1,1)
1. f10(B,C,D,E,F) -> f10(1 + B,C,D,E,F) [C >= 1 + B] (?,1)
2. f18(B,C,D,E,F) -> f21(B,C,D,E,0) [D >= 2 + E] (?,1)
3. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
4. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
5. f32(B,C,D,E,F) -> f32(B,C,D,1 + E,F) [D >= 2 + E] (?,1)
7. f21(B,C,D,E,F) -> f18(B,C,D,1 + E,F) [1 + E + F >= D] (?,1)
8. f18(B,C,D,E,F) -> f32(B,C,D,0,F) [1 + E >= D] (?,1)
9. f10(B,C,D,E,F) -> f18(B,C,C,0,F) [B >= C] (1,1)
Signature:
{(f0,5);(f10,5);(f18,5);(f21,5);(f32,5);(f41,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,F>, F)
(<1,0,B>, C) (<1,0,C>, C) (<1,0,D>, D) (<1,0,E>, E) (<1,0,F>, F)
(<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, C) (<2,0,E>, C) (<2,0,F>, 0)
(<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, C) (<3,0,E>, C) (<3,0,F>, C)
(<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, C) (<4,0,E>, C) (<4,0,F>, C)
(<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, C) (<5,0,E>, C) (<5,0,F>, C + F)
(<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, C) (<7,0,E>, C) (<7,0,F>, C)
(<8,0,B>, ?) (<8,0,C>, C) (<8,0,D>, C) (<8,0,E>, 0) (<8,0,F>, C + F)
(<9,0,B>, C) (<9,0,C>, C) (<9,0,D>, C) (<9,0,E>, 0) (<9,0,F>, F)
+ 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(f21) = 1
p(f32) = 0
The following rules are strictly oriented:
[1 + E >= D] ==>
f18(B,C,D,E,F) = 1
> 0
= f32(B,C,D,0,F)
The following rules are weakly oriented:
True ==>
f0(B,C,D,E,F) = 1
>= 1
= f10(0,C,D,E,F)
[C >= 1 + B] ==>
f10(B,C,D,E,F) = 1
>= 1
= f10(1 + B,C,D,E,F)
[D >= 2 + E] ==>
f18(B,C,D,E,F) = 1
>= 1
= f21(B,C,D,E,0)
[D >= 2 + E + F] ==>
f21(B,C,D,E,F) = 1
>= 1
= f21(B,C,D,E,1 + F)
[D >= 2 + E + F] ==>
f21(B,C,D,E,F) = 1
>= 1
= f21(B,C,D,E,1 + F)
[D >= 2 + E] ==>
f32(B,C,D,E,F) = 0
>= 0
= f32(B,C,D,1 + E,F)
[1 + E + F >= D] ==>
f21(B,C,D,E,F) = 1
>= 1
= f18(B,C,D,1 + E,F)
[B >= C] ==>
f10(B,C,D,E,F) = 1
>= 1
= f18(B,C,C,0,F)
* Step 8: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. f0(B,C,D,E,F) -> f10(0,C,D,E,F) True (1,1)
1. f10(B,C,D,E,F) -> f10(1 + B,C,D,E,F) [C >= 1 + B] (?,1)
2. f18(B,C,D,E,F) -> f21(B,C,D,E,0) [D >= 2 + E] (?,1)
3. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
4. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
5. f32(B,C,D,E,F) -> f32(B,C,D,1 + E,F) [D >= 2 + E] (?,1)
7. f21(B,C,D,E,F) -> f18(B,C,D,1 + E,F) [1 + E + F >= D] (?,1)
8. f18(B,C,D,E,F) -> f32(B,C,D,0,F) [1 + E >= D] (1,1)
9. f10(B,C,D,E,F) -> f18(B,C,C,0,F) [B >= C] (1,1)
Signature:
{(f0,5);(f10,5);(f18,5);(f21,5);(f32,5);(f41,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,F>, F)
(<1,0,B>, C) (<1,0,C>, C) (<1,0,D>, D) (<1,0,E>, E) (<1,0,F>, F)
(<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, C) (<2,0,E>, C) (<2,0,F>, 0)
(<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, C) (<3,0,E>, C) (<3,0,F>, C)
(<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, C) (<4,0,E>, C) (<4,0,F>, C)
(<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, C) (<5,0,E>, C) (<5,0,F>, C + F)
(<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, C) (<7,0,E>, C) (<7,0,F>, C)
(<8,0,B>, ?) (<8,0,C>, C) (<8,0,D>, C) (<8,0,E>, 0) (<8,0,F>, C + F)
(<9,0,B>, C) (<9,0,C>, C) (<9,0,D>, C) (<9,0,E>, 0) (<9,0,F>, F)
+ 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) = x3
p(f21) = x3
p(f32) = -1 + x3 + -1*x4
The following rules are strictly oriented:
[D >= 2 + E] ==>
f32(B,C,D,E,F) = -1 + D + -1*E
> -2 + D + -1*E
= f32(B,C,D,1 + E,F)
The following rules are weakly oriented:
True ==>
f0(B,C,D,E,F) = C
>= C
= f10(0,C,D,E,F)
[C >= 1 + B] ==>
f10(B,C,D,E,F) = C
>= C
= f10(1 + B,C,D,E,F)
[D >= 2 + E] ==>
f18(B,C,D,E,F) = D
>= D
= f21(B,C,D,E,0)
[D >= 2 + E + F] ==>
f21(B,C,D,E,F) = D
>= D
= f21(B,C,D,E,1 + F)
[D >= 2 + E + F] ==>
f21(B,C,D,E,F) = D
>= D
= f21(B,C,D,E,1 + F)
[1 + E + F >= D] ==>
f21(B,C,D,E,F) = D
>= D
= f18(B,C,D,1 + E,F)
[1 + E >= D] ==>
f18(B,C,D,E,F) = D
>= -1 + D
= f32(B,C,D,0,F)
[B >= C] ==>
f10(B,C,D,E,F) = C
>= C
= f18(B,C,C,0,F)
* Step 9: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. f0(B,C,D,E,F) -> f10(0,C,D,E,F) True (1,1)
1. f10(B,C,D,E,F) -> f10(1 + B,C,D,E,F) [C >= 1 + B] (?,1)
2. f18(B,C,D,E,F) -> f21(B,C,D,E,0) [D >= 2 + E] (?,1)
3. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
4. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
5. f32(B,C,D,E,F) -> f32(B,C,D,1 + E,F) [D >= 2 + E] (C,1)
7. f21(B,C,D,E,F) -> f18(B,C,D,1 + E,F) [1 + E + F >= D] (?,1)
8. f18(B,C,D,E,F) -> f32(B,C,D,0,F) [1 + E >= D] (1,1)
9. f10(B,C,D,E,F) -> f18(B,C,C,0,F) [B >= C] (1,1)
Signature:
{(f0,5);(f10,5);(f18,5);(f21,5);(f32,5);(f41,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,F>, F)
(<1,0,B>, C) (<1,0,C>, C) (<1,0,D>, D) (<1,0,E>, E) (<1,0,F>, F)
(<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, C) (<2,0,E>, C) (<2,0,F>, 0)
(<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, C) (<3,0,E>, C) (<3,0,F>, C)
(<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, C) (<4,0,E>, C) (<4,0,F>, C)
(<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, C) (<5,0,E>, C) (<5,0,F>, C + F)
(<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, C) (<7,0,E>, C) (<7,0,F>, C)
(<8,0,B>, ?) (<8,0,C>, C) (<8,0,D>, C) (<8,0,E>, 0) (<8,0,F>, C + F)
(<9,0,B>, C) (<9,0,C>, C) (<9,0,D>, C) (<9,0,E>, 0) (<9,0,F>, F)
+ 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(f21) = -1*x1 + x2
p(f32) = -1*x1 + x2
The following rules are strictly oriented:
[C >= 1 + B] ==>
f10(B,C,D,E,F) = -1*B + C
> -1 + -1*B + C
= f10(1 + B,C,D,E,F)
The following rules are weakly oriented:
True ==>
f0(B,C,D,E,F) = C
>= C
= f10(0,C,D,E,F)
[D >= 2 + E] ==>
f18(B,C,D,E,F) = -1*B + C
>= -1*B + C
= f21(B,C,D,E,0)
[D >= 2 + E + F] ==>
f21(B,C,D,E,F) = -1*B + C
>= -1*B + C
= f21(B,C,D,E,1 + F)
[D >= 2 + E + F] ==>
f21(B,C,D,E,F) = -1*B + C
>= -1*B + C
= f21(B,C,D,E,1 + F)
[D >= 2 + E] ==>
f32(B,C,D,E,F) = -1*B + C
>= -1*B + C
= f32(B,C,D,1 + E,F)
[1 + E + F >= D] ==>
f21(B,C,D,E,F) = -1*B + C
>= -1*B + C
= f18(B,C,D,1 + E,F)
[1 + E >= D] ==>
f18(B,C,D,E,F) = -1*B + C
>= -1*B + C
= f32(B,C,D,0,F)
[B >= C] ==>
f10(B,C,D,E,F) = -1*B + C
>= -1*B + C
= f18(B,C,C,0,F)
* Step 10: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. f0(B,C,D,E,F) -> f10(0,C,D,E,F) True (1,1)
1. f10(B,C,D,E,F) -> f10(1 + B,C,D,E,F) [C >= 1 + B] (C,1)
2. f18(B,C,D,E,F) -> f21(B,C,D,E,0) [D >= 2 + E] (?,1)
3. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
4. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
5. f32(B,C,D,E,F) -> f32(B,C,D,1 + E,F) [D >= 2 + E] (C,1)
7. f21(B,C,D,E,F) -> f18(B,C,D,1 + E,F) [1 + E + F >= D] (?,1)
8. f18(B,C,D,E,F) -> f32(B,C,D,0,F) [1 + E >= D] (1,1)
9. f10(B,C,D,E,F) -> f18(B,C,C,0,F) [B >= C] (1,1)
Signature:
{(f0,5);(f10,5);(f18,5);(f21,5);(f32,5);(f41,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,F>, F)
(<1,0,B>, C) (<1,0,C>, C) (<1,0,D>, D) (<1,0,E>, E) (<1,0,F>, F)
(<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, C) (<2,0,E>, C) (<2,0,F>, 0)
(<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, C) (<3,0,E>, C) (<3,0,F>, C)
(<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, C) (<4,0,E>, C) (<4,0,F>, C)
(<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, C) (<5,0,E>, C) (<5,0,F>, C + F)
(<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, C) (<7,0,E>, C) (<7,0,F>, C)
(<8,0,B>, ?) (<8,0,C>, C) (<8,0,D>, C) (<8,0,E>, 0) (<8,0,F>, C + F)
(<9,0,B>, C) (<9,0,C>, C) (<9,0,D>, C) (<9,0,E>, 0) (<9,0,F>, F)
+ 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(f21) = 1 + x3 + -1*x4
The following rules are strictly oriented:
[D >= 2 + E] ==>
f18(B,C,D,E,F) = 2 + D + -1*E
> 1 + D + -1*E
= f21(B,C,D,E,0)
The following rules are weakly oriented:
[D >= 2 + E + F] ==>
f21(B,C,D,E,F) = 1 + D + -1*E
>= 1 + D + -1*E
= f21(B,C,D,E,1 + F)
[D >= 2 + E + F] ==>
f21(B,C,D,E,F) = 1 + D + -1*E
>= 1 + D + -1*E
= f21(B,C,D,E,1 + F)
[1 + E + F >= D] ==>
f21(B,C,D,E,F) = 1 + D + -1*E
>= 1 + D + -1*E
= f18(B,C,D,1 + E,F)
We use the following global sizebounds:
(<0,0,B>, 0) (<0,0,C>, C) (<0,0,D>, D) (<0,0,E>, E) (<0,0,F>, F)
(<1,0,B>, C) (<1,0,C>, C) (<1,0,D>, D) (<1,0,E>, E) (<1,0,F>, F)
(<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, C) (<2,0,E>, C) (<2,0,F>, 0)
(<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, C) (<3,0,E>, C) (<3,0,F>, C)
(<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, C) (<4,0,E>, C) (<4,0,F>, C)
(<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, C) (<5,0,E>, C) (<5,0,F>, C + F)
(<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, C) (<7,0,E>, C) (<7,0,F>, C)
(<8,0,B>, ?) (<8,0,C>, C) (<8,0,D>, C) (<8,0,E>, 0) (<8,0,F>, C + F)
(<9,0,B>, C) (<9,0,C>, C) (<9,0,D>, C) (<9,0,E>, 0) (<9,0,F>, F)
* Step 11: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. f0(B,C,D,E,F) -> f10(0,C,D,E,F) True (1,1)
1. f10(B,C,D,E,F) -> f10(1 + B,C,D,E,F) [C >= 1 + B] (C,1)
2. f18(B,C,D,E,F) -> f21(B,C,D,E,0) [D >= 2 + E] (2 + C,1)
3. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
4. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
5. f32(B,C,D,E,F) -> f32(B,C,D,1 + E,F) [D >= 2 + E] (C,1)
7. f21(B,C,D,E,F) -> f18(B,C,D,1 + E,F) [1 + E + F >= D] (?,1)
8. f18(B,C,D,E,F) -> f32(B,C,D,0,F) [1 + E >= D] (1,1)
9. f10(B,C,D,E,F) -> f18(B,C,C,0,F) [B >= C] (1,1)
Signature:
{(f0,5);(f10,5);(f18,5);(f21,5);(f32,5);(f41,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,F>, F)
(<1,0,B>, C) (<1,0,C>, C) (<1,0,D>, D) (<1,0,E>, E) (<1,0,F>, F)
(<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, C) (<2,0,E>, C) (<2,0,F>, 0)
(<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, C) (<3,0,E>, C) (<3,0,F>, C)
(<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, C) (<4,0,E>, C) (<4,0,F>, C)
(<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, C) (<5,0,E>, C) (<5,0,F>, C + F)
(<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, C) (<7,0,E>, C) (<7,0,F>, C)
(<8,0,B>, ?) (<8,0,C>, C) (<8,0,D>, C) (<8,0,E>, 0) (<8,0,F>, C + F)
(<9,0,B>, C) (<9,0,C>, C) (<9,0,D>, C) (<9,0,E>, 0) (<9,0,F>, F)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [3,4], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f21) = -1 + x3 + -1*x4 + -1*x5
The following rules are strictly oriented:
[D >= 2 + E + F] ==>
f21(B,C,D,E,F) = -1 + D + -1*E + -1*F
> -2 + D + -1*E + -1*F
= f21(B,C,D,E,1 + F)
The following rules are weakly oriented:
[D >= 2 + E + F] ==>
f21(B,C,D,E,F) = -1 + D + -1*E + -1*F
>= -2 + D + -1*E + -1*F
= f21(B,C,D,E,1 + F)
We use the following global sizebounds:
(<0,0,B>, 0) (<0,0,C>, C) (<0,0,D>, D) (<0,0,E>, E) (<0,0,F>, F)
(<1,0,B>, C) (<1,0,C>, C) (<1,0,D>, D) (<1,0,E>, E) (<1,0,F>, F)
(<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, C) (<2,0,E>, C) (<2,0,F>, 0)
(<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, C) (<3,0,E>, C) (<3,0,F>, C)
(<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, C) (<4,0,E>, C) (<4,0,F>, C)
(<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, C) (<5,0,E>, C) (<5,0,F>, C + F)
(<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, C) (<7,0,E>, C) (<7,0,F>, C)
(<8,0,B>, ?) (<8,0,C>, C) (<8,0,D>, C) (<8,0,E>, 0) (<8,0,F>, C + F)
(<9,0,B>, C) (<9,0,C>, C) (<9,0,D>, C) (<9,0,E>, 0) (<9,0,F>, F)
* Step 12: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. f0(B,C,D,E,F) -> f10(0,C,D,E,F) True (1,1)
1. f10(B,C,D,E,F) -> f10(1 + B,C,D,E,F) [C >= 1 + B] (C,1)
2. f18(B,C,D,E,F) -> f21(B,C,D,E,0) [D >= 2 + E] (2 + C,1)
3. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
4. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (2 + 5*C + 2*C^2,1)
5. f32(B,C,D,E,F) -> f32(B,C,D,1 + E,F) [D >= 2 + E] (C,1)
7. f21(B,C,D,E,F) -> f18(B,C,D,1 + E,F) [1 + E + F >= D] (?,1)
8. f18(B,C,D,E,F) -> f32(B,C,D,0,F) [1 + E >= D] (1,1)
9. f10(B,C,D,E,F) -> f18(B,C,C,0,F) [B >= C] (1,1)
Signature:
{(f0,5);(f10,5);(f18,5);(f21,5);(f32,5);(f41,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,F>, F)
(<1,0,B>, C) (<1,0,C>, C) (<1,0,D>, D) (<1,0,E>, E) (<1,0,F>, F)
(<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, C) (<2,0,E>, C) (<2,0,F>, 0)
(<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, C) (<3,0,E>, C) (<3,0,F>, C)
(<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, C) (<4,0,E>, C) (<4,0,F>, C)
(<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, C) (<5,0,E>, C) (<5,0,F>, C + F)
(<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, C) (<7,0,E>, C) (<7,0,F>, C)
(<8,0,B>, ?) (<8,0,C>, C) (<8,0,D>, C) (<8,0,E>, 0) (<8,0,F>, C + F)
(<9,0,B>, C) (<9,0,C>, C) (<9,0,D>, C) (<9,0,E>, 0) (<9,0,F>, F)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [7,3,4], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f18) = 0
p(f21) = 1
The following rules are strictly oriented:
[1 + E + F >= D] ==>
f21(B,C,D,E,F) = 1
> 0
= f18(B,C,D,1 + E,F)
The following rules are weakly oriented:
[D >= 2 + E + F] ==>
f21(B,C,D,E,F) = 1
>= 1
= f21(B,C,D,E,1 + F)
[D >= 2 + E + F] ==>
f21(B,C,D,E,F) = 1
>= 1
= f21(B,C,D,E,1 + F)
We use the following global sizebounds:
(<0,0,B>, 0) (<0,0,C>, C) (<0,0,D>, D) (<0,0,E>, E) (<0,0,F>, F)
(<1,0,B>, C) (<1,0,C>, C) (<1,0,D>, D) (<1,0,E>, E) (<1,0,F>, F)
(<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, C) (<2,0,E>, C) (<2,0,F>, 0)
(<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, C) (<3,0,E>, C) (<3,0,F>, C)
(<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, C) (<4,0,E>, C) (<4,0,F>, C)
(<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, C) (<5,0,E>, C) (<5,0,F>, C + F)
(<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, C) (<7,0,E>, C) (<7,0,F>, C)
(<8,0,B>, ?) (<8,0,C>, C) (<8,0,D>, C) (<8,0,E>, 0) (<8,0,F>, C + F)
(<9,0,B>, C) (<9,0,C>, C) (<9,0,D>, C) (<9,0,E>, 0) (<9,0,F>, F)
* Step 13: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. f0(B,C,D,E,F) -> f10(0,C,D,E,F) True (1,1)
1. f10(B,C,D,E,F) -> f10(1 + B,C,D,E,F) [C >= 1 + B] (C,1)
2. f18(B,C,D,E,F) -> f21(B,C,D,E,0) [D >= 2 + E] (2 + C,1)
3. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (?,1)
4. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (2 + 5*C + 2*C^2,1)
5. f32(B,C,D,E,F) -> f32(B,C,D,1 + E,F) [D >= 2 + E] (C,1)
7. f21(B,C,D,E,F) -> f18(B,C,D,1 + E,F) [1 + E + F >= D] (2 + C,1)
8. f18(B,C,D,E,F) -> f32(B,C,D,0,F) [1 + E >= D] (1,1)
9. f10(B,C,D,E,F) -> f18(B,C,C,0,F) [B >= C] (1,1)
Signature:
{(f0,5);(f10,5);(f18,5);(f21,5);(f32,5);(f41,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,F>, F)
(<1,0,B>, C) (<1,0,C>, C) (<1,0,D>, D) (<1,0,E>, E) (<1,0,F>, F)
(<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, C) (<2,0,E>, C) (<2,0,F>, 0)
(<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, C) (<3,0,E>, C) (<3,0,F>, C)
(<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, C) (<4,0,E>, C) (<4,0,F>, C)
(<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, C) (<5,0,E>, C) (<5,0,F>, C + F)
(<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, C) (<7,0,E>, C) (<7,0,F>, C)
(<8,0,B>, ?) (<8,0,C>, C) (<8,0,D>, C) (<8,0,E>, 0) (<8,0,F>, C + F)
(<9,0,B>, C) (<9,0,C>, C) (<9,0,D>, C) (<9,0,E>, 0) (<9,0,F>, F)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [2,3,4], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f18) = x3 + -1*x4
p(f21) = -1 + x3 + -1*x4 + -1*x5
The following rules are strictly oriented:
[D >= 2 + E + F] ==>
f21(B,C,D,E,F) = -1 + D + -1*E + -1*F
> -2 + D + -1*E + -1*F
= f21(B,C,D,E,1 + F)
[D >= 2 + E + F] ==>
f21(B,C,D,E,F) = -1 + D + -1*E + -1*F
> -2 + D + -1*E + -1*F
= f21(B,C,D,E,1 + F)
The following rules are weakly oriented:
[D >= 2 + E] ==>
f18(B,C,D,E,F) = D + -1*E
>= -1 + D + -1*E
= f21(B,C,D,E,0)
We use the following global sizebounds:
(<0,0,B>, 0) (<0,0,C>, C) (<0,0,D>, D) (<0,0,E>, E) (<0,0,F>, F)
(<1,0,B>, C) (<1,0,C>, C) (<1,0,D>, D) (<1,0,E>, E) (<1,0,F>, F)
(<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, C) (<2,0,E>, C) (<2,0,F>, 0)
(<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, C) (<3,0,E>, C) (<3,0,F>, C)
(<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, C) (<4,0,E>, C) (<4,0,F>, C)
(<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, C) (<5,0,E>, C) (<5,0,F>, C + F)
(<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, C) (<7,0,E>, C) (<7,0,F>, C)
(<8,0,B>, ?) (<8,0,C>, C) (<8,0,D>, C) (<8,0,E>, 0) (<8,0,F>, C + F)
(<9,0,B>, C) (<9,0,C>, C) (<9,0,D>, C) (<9,0,E>, 0) (<9,0,F>, F)
* Step 14: KnowledgePropagation WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. f0(B,C,D,E,F) -> f10(0,C,D,E,F) True (1,1)
1. f10(B,C,D,E,F) -> f10(1 + B,C,D,E,F) [C >= 1 + B] (C,1)
2. f18(B,C,D,E,F) -> f21(B,C,D,E,0) [D >= 2 + E] (2 + C,1)
3. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (5*C + 2*C^2,1)
4. f21(B,C,D,E,F) -> f21(B,C,D,E,1 + F) [D >= 2 + E + F] (5*C + 2*C^2,1)
5. f32(B,C,D,E,F) -> f32(B,C,D,1 + E,F) [D >= 2 + E] (C,1)
7. f21(B,C,D,E,F) -> f18(B,C,D,1 + E,F) [1 + E + F >= D] (2 + C,1)
8. f18(B,C,D,E,F) -> f32(B,C,D,0,F) [1 + E >= D] (1,1)
9. f10(B,C,D,E,F) -> f18(B,C,C,0,F) [B >= C] (1,1)
Signature:
{(f0,5);(f10,5);(f18,5);(f21,5);(f32,5);(f41,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,F>, F)
(<1,0,B>, C) (<1,0,C>, C) (<1,0,D>, D) (<1,0,E>, E) (<1,0,F>, F)
(<2,0,B>, ?) (<2,0,C>, C) (<2,0,D>, C) (<2,0,E>, C) (<2,0,F>, 0)
(<3,0,B>, ?) (<3,0,C>, C) (<3,0,D>, C) (<3,0,E>, C) (<3,0,F>, C)
(<4,0,B>, ?) (<4,0,C>, C) (<4,0,D>, C) (<4,0,E>, C) (<4,0,F>, C)
(<5,0,B>, ?) (<5,0,C>, C) (<5,0,D>, C) (<5,0,E>, C) (<5,0,F>, C + F)
(<7,0,B>, ?) (<7,0,C>, C) (<7,0,D>, C) (<7,0,E>, C) (<7,0,F>, C)
(<8,0,B>, ?) (<8,0,C>, C) (<8,0,D>, C) (<8,0,E>, 0) (<8,0,F>, C + F)
(<9,0,B>, C) (<9,0,C>, C) (<9,0,D>, C) (<9,0,E>, 0) (<9,0,F>, F)
+ Applied Processor:
KnowledgePropagation
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^2))