WORST_CASE(?,O(1))
* Step 1: RestrictVarsProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E,F,G) -> f9(0,0,H,D,E,F,G) True (1,1)
1. f9(A,B,C,D,E,F,G) -> f10(A,B,C,C,E,F,G) [0 >= 1 + C] (?,1)
2. f9(A,B,C,D,E,F,G) -> f10(A,B,C,C,E,F,G) [C >= 1] (?,1)
3. f10(A,B,C,D,E,F,G) -> f9(1 + A,1 + A,H,D,E,F,G) [9 >= A] (?,1)
4. f16(A,B,C,D,E,F,G) -> f28(A,B,C,D,E,F,G) [A >= 10] (?,1)
5. f16(A,B,C,D,E,F,G) -> f16(1 + A,B,C,D,A,H,H) [9 >= A && 0 >= 1 + H] (?,1)
6. f16(A,B,C,D,E,F,G) -> f16(1 + A,B,C,D,A,H,H) [9 >= A && H >= 1] (?,1)
7. f16(A,B,C,D,E,F,G) -> f28(A,B,C,D,A,0,0) [9 >= A] (?,1)
8. f10(A,B,C,D,E,F,G) -> f16(0,B,C,D,E,F,G) [A >= 10] (?,1)
9. f9(A,B,C,D,E,F,G) -> f16(0,B,0,0,E,F,G) [C = 0] (?,1)
Signature:
{(f0,7);(f10,7);(f16,7);(f28,7);(f9,7)}
Flow Graph:
[0->{1,2,9},1->{3,8},2->{3,8},3->{1,2,9},4->{},5->{4,5,6,7},6->{4,5,6,7},7->{},8->{4,5,6,7},9->{4,5,6,7}]
+ Applied Processor:
RestrictVarsProcessor
+ Details:
We removed the arguments [B,D,E,F,G] .
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C) -> f9(0,H) True (1,1)
1. f9(A,C) -> f10(A,C) [0 >= 1 + C] (?,1)
2. f9(A,C) -> f10(A,C) [C >= 1] (?,1)
3. f10(A,C) -> f9(1 + A,H) [9 >= A] (?,1)
4. f16(A,C) -> f28(A,C) [A >= 10] (?,1)
5. f16(A,C) -> f16(1 + A,C) [9 >= A && 0 >= 1 + H] (?,1)
6. f16(A,C) -> f16(1 + A,C) [9 >= A && H >= 1] (?,1)
7. f16(A,C) -> f28(A,C) [9 >= A] (?,1)
8. f10(A,C) -> f16(0,C) [A >= 10] (?,1)
9. f9(A,C) -> f16(0,0) [C = 0] (?,1)
Signature:
{(f0,2);(f10,2);(f16,2);(f28,2);(f9,2)}
Flow Graph:
[0->{1,2,9},1->{3,8},2->{3,8},3->{1,2,9},4->{},5->{4,5,6,7},6->{4,5,6,7},7->{},8->{4,5,6,7},9->{4,5,6,7}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<0,0,A>, 0, .= 0) (<0,0,C>, ?, .?)
(<1,0,A>, A, .= 0) (<1,0,C>, C, .= 0)
(<2,0,A>, A, .= 0) (<2,0,C>, C, .= 0)
(<3,0,A>, 1 + A, .+ 1) (<3,0,C>, ?, .?)
(<4,0,A>, A, .= 0) (<4,0,C>, C, .= 0)
(<5,0,A>, 1 + A, .+ 1) (<5,0,C>, C, .= 0)
(<6,0,A>, 1 + A, .+ 1) (<6,0,C>, C, .= 0)
(<7,0,A>, A, .= 0) (<7,0,C>, C, .= 0)
(<8,0,A>, 0, .= 0) (<8,0,C>, C, .= 0)
(<9,0,A>, 0, .= 0) (<9,0,C>, 0, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C) -> f9(0,H) True (1,1)
1. f9(A,C) -> f10(A,C) [0 >= 1 + C] (?,1)
2. f9(A,C) -> f10(A,C) [C >= 1] (?,1)
3. f10(A,C) -> f9(1 + A,H) [9 >= A] (?,1)
4. f16(A,C) -> f28(A,C) [A >= 10] (?,1)
5. f16(A,C) -> f16(1 + A,C) [9 >= A && 0 >= 1 + H] (?,1)
6. f16(A,C) -> f16(1 + A,C) [9 >= A && H >= 1] (?,1)
7. f16(A,C) -> f28(A,C) [9 >= A] (?,1)
8. f10(A,C) -> f16(0,C) [A >= 10] (?,1)
9. f9(A,C) -> f16(0,0) [C = 0] (?,1)
Signature:
{(f0,2);(f10,2);(f16,2);(f28,2);(f9,2)}
Flow Graph:
[0->{1,2,9},1->{3,8},2->{3,8},3->{1,2,9},4->{},5->{4,5,6,7},6->{4,5,6,7},7->{},8->{4,5,6,7},9->{4,5,6,7}]
Sizebounds:
(<0,0,A>, ?) (<0,0,C>, ?)
(<1,0,A>, ?) (<1,0,C>, ?)
(<2,0,A>, ?) (<2,0,C>, ?)
(<3,0,A>, ?) (<3,0,C>, ?)
(<4,0,A>, ?) (<4,0,C>, ?)
(<5,0,A>, ?) (<5,0,C>, ?)
(<6,0,A>, ?) (<6,0,C>, ?)
(<7,0,A>, ?) (<7,0,C>, ?)
(<8,0,A>, ?) (<8,0,C>, ?)
(<9,0,A>, ?) (<9,0,C>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<0,0,A>, 0) (<0,0,C>, ?)
(<1,0,A>, 10) (<1,0,C>, ?)
(<2,0,A>, 10) (<2,0,C>, ?)
(<3,0,A>, 10) (<3,0,C>, ?)
(<4,0,A>, 10) (<4,0,C>, ?)
(<5,0,A>, 10) (<5,0,C>, ?)
(<6,0,A>, 10) (<6,0,C>, ?)
(<7,0,A>, 10) (<7,0,C>, ?)
(<8,0,A>, 0) (<8,0,C>, ?)
(<9,0,A>, 0) (<9,0,C>, 0)
* Step 4: UnsatPaths WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C) -> f9(0,H) True (1,1)
1. f9(A,C) -> f10(A,C) [0 >= 1 + C] (?,1)
2. f9(A,C) -> f10(A,C) [C >= 1] (?,1)
3. f10(A,C) -> f9(1 + A,H) [9 >= A] (?,1)
4. f16(A,C) -> f28(A,C) [A >= 10] (?,1)
5. f16(A,C) -> f16(1 + A,C) [9 >= A && 0 >= 1 + H] (?,1)
6. f16(A,C) -> f16(1 + A,C) [9 >= A && H >= 1] (?,1)
7. f16(A,C) -> f28(A,C) [9 >= A] (?,1)
8. f10(A,C) -> f16(0,C) [A >= 10] (?,1)
9. f9(A,C) -> f16(0,0) [C = 0] (?,1)
Signature:
{(f0,2);(f10,2);(f16,2);(f28,2);(f9,2)}
Flow Graph:
[0->{1,2,9},1->{3,8},2->{3,8},3->{1,2,9},4->{},5->{4,5,6,7},6->{4,5,6,7},7->{},8->{4,5,6,7},9->{4,5,6,7}]
Sizebounds:
(<0,0,A>, 0) (<0,0,C>, ?)
(<1,0,A>, 10) (<1,0,C>, ?)
(<2,0,A>, 10) (<2,0,C>, ?)
(<3,0,A>, 10) (<3,0,C>, ?)
(<4,0,A>, 10) (<4,0,C>, ?)
(<5,0,A>, 10) (<5,0,C>, ?)
(<6,0,A>, 10) (<6,0,C>, ?)
(<7,0,A>, 10) (<7,0,C>, ?)
(<8,0,A>, 0) (<8,0,C>, ?)
(<9,0,A>, 0) (<9,0,C>, 0)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(8,4),(9,4)]
* Step 5: LeafRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C) -> f9(0,H) True (1,1)
1. f9(A,C) -> f10(A,C) [0 >= 1 + C] (?,1)
2. f9(A,C) -> f10(A,C) [C >= 1] (?,1)
3. f10(A,C) -> f9(1 + A,H) [9 >= A] (?,1)
4. f16(A,C) -> f28(A,C) [A >= 10] (?,1)
5. f16(A,C) -> f16(1 + A,C) [9 >= A && 0 >= 1 + H] (?,1)
6. f16(A,C) -> f16(1 + A,C) [9 >= A && H >= 1] (?,1)
7. f16(A,C) -> f28(A,C) [9 >= A] (?,1)
8. f10(A,C) -> f16(0,C) [A >= 10] (?,1)
9. f9(A,C) -> f16(0,0) [C = 0] (?,1)
Signature:
{(f0,2);(f10,2);(f16,2);(f28,2);(f9,2)}
Flow Graph:
[0->{1,2,9},1->{3,8},2->{3,8},3->{1,2,9},4->{},5->{4,5,6,7},6->{4,5,6,7},7->{},8->{5,6,7},9->{5,6,7}]
Sizebounds:
(<0,0,A>, 0) (<0,0,C>, ?)
(<1,0,A>, 10) (<1,0,C>, ?)
(<2,0,A>, 10) (<2,0,C>, ?)
(<3,0,A>, 10) (<3,0,C>, ?)
(<4,0,A>, 10) (<4,0,C>, ?)
(<5,0,A>, 10) (<5,0,C>, ?)
(<6,0,A>, 10) (<6,0,C>, ?)
(<7,0,A>, 10) (<7,0,C>, ?)
(<8,0,A>, 0) (<8,0,C>, ?)
(<9,0,A>, 0) (<9,0,C>, 0)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [4,7]
* Step 6: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C) -> f9(0,H) True (1,1)
1. f9(A,C) -> f10(A,C) [0 >= 1 + C] (?,1)
2. f9(A,C) -> f10(A,C) [C >= 1] (?,1)
3. f10(A,C) -> f9(1 + A,H) [9 >= A] (?,1)
5. f16(A,C) -> f16(1 + A,C) [9 >= A && 0 >= 1 + H] (?,1)
6. f16(A,C) -> f16(1 + A,C) [9 >= A && H >= 1] (?,1)
8. f10(A,C) -> f16(0,C) [A >= 10] (?,1)
9. f9(A,C) -> f16(0,0) [C = 0] (?,1)
Signature:
{(f0,2);(f10,2);(f16,2);(f28,2);(f9,2)}
Flow Graph:
[0->{1,2,9},1->{3,8},2->{3,8},3->{1,2,9},5->{5,6},6->{5,6},8->{5,6},9->{5,6}]
Sizebounds:
(<0,0,A>, 0) (<0,0,C>, ?)
(<1,0,A>, 10) (<1,0,C>, ?)
(<2,0,A>, 10) (<2,0,C>, ?)
(<3,0,A>, 10) (<3,0,C>, ?)
(<5,0,A>, 10) (<5,0,C>, ?)
(<6,0,A>, 10) (<6,0,C>, ?)
(<8,0,A>, 0) (<8,0,C>, ?)
(<9,0,A>, 0) (<9,0,C>, 0)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 1
p(f10) = 1
p(f16) = 0
p(f9) = 1
The following rules are strictly oriented:
[C = 0] ==>
f9(A,C) = 1
> 0
= f16(0,0)
The following rules are weakly oriented:
True ==>
f0(A,C) = 1
>= 1
= f9(0,H)
[0 >= 1 + C] ==>
f9(A,C) = 1
>= 1
= f10(A,C)
[C >= 1] ==>
f9(A,C) = 1
>= 1
= f10(A,C)
[9 >= A] ==>
f10(A,C) = 1
>= 1
= f9(1 + A,H)
[9 >= A && 0 >= 1 + H] ==>
f16(A,C) = 0
>= 0
= f16(1 + A,C)
[9 >= A && H >= 1] ==>
f16(A,C) = 0
>= 0
= f16(1 + A,C)
[A >= 10] ==>
f10(A,C) = 1
>= 0
= f16(0,C)
* Step 7: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C) -> f9(0,H) True (1,1)
1. f9(A,C) -> f10(A,C) [0 >= 1 + C] (?,1)
2. f9(A,C) -> f10(A,C) [C >= 1] (?,1)
3. f10(A,C) -> f9(1 + A,H) [9 >= A] (?,1)
5. f16(A,C) -> f16(1 + A,C) [9 >= A && 0 >= 1 + H] (?,1)
6. f16(A,C) -> f16(1 + A,C) [9 >= A && H >= 1] (?,1)
8. f10(A,C) -> f16(0,C) [A >= 10] (?,1)
9. f9(A,C) -> f16(0,0) [C = 0] (1,1)
Signature:
{(f0,2);(f10,2);(f16,2);(f28,2);(f9,2)}
Flow Graph:
[0->{1,2,9},1->{3,8},2->{3,8},3->{1,2,9},5->{5,6},6->{5,6},8->{5,6},9->{5,6}]
Sizebounds:
(<0,0,A>, 0) (<0,0,C>, ?)
(<1,0,A>, 10) (<1,0,C>, ?)
(<2,0,A>, 10) (<2,0,C>, ?)
(<3,0,A>, 10) (<3,0,C>, ?)
(<5,0,A>, 10) (<5,0,C>, ?)
(<6,0,A>, 10) (<6,0,C>, ?)
(<8,0,A>, 0) (<8,0,C>, ?)
(<9,0,A>, 0) (<9,0,C>, 0)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 1
p(f10) = 1
p(f16) = 0
p(f9) = 1
The following rules are strictly oriented:
[A >= 10] ==>
f10(A,C) = 1
> 0
= f16(0,C)
[C = 0] ==>
f9(A,C) = 1
> 0
= f16(0,0)
The following rules are weakly oriented:
True ==>
f0(A,C) = 1
>= 1
= f9(0,H)
[0 >= 1 + C] ==>
f9(A,C) = 1
>= 1
= f10(A,C)
[C >= 1] ==>
f9(A,C) = 1
>= 1
= f10(A,C)
[9 >= A] ==>
f10(A,C) = 1
>= 1
= f9(1 + A,H)
[9 >= A && 0 >= 1 + H] ==>
f16(A,C) = 0
>= 0
= f16(1 + A,C)
[9 >= A && H >= 1] ==>
f16(A,C) = 0
>= 0
= f16(1 + A,C)
* Step 8: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C) -> f9(0,H) True (1,1)
1. f9(A,C) -> f10(A,C) [0 >= 1 + C] (?,1)
2. f9(A,C) -> f10(A,C) [C >= 1] (?,1)
3. f10(A,C) -> f9(1 + A,H) [9 >= A] (?,1)
5. f16(A,C) -> f16(1 + A,C) [9 >= A && 0 >= 1 + H] (?,1)
6. f16(A,C) -> f16(1 + A,C) [9 >= A && H >= 1] (?,1)
8. f10(A,C) -> f16(0,C) [A >= 10] (1,1)
9. f9(A,C) -> f16(0,0) [C = 0] (1,1)
Signature:
{(f0,2);(f10,2);(f16,2);(f28,2);(f9,2)}
Flow Graph:
[0->{1,2,9},1->{3,8},2->{3,8},3->{1,2,9},5->{5,6},6->{5,6},8->{5,6},9->{5,6}]
Sizebounds:
(<0,0,A>, 0) (<0,0,C>, ?)
(<1,0,A>, 10) (<1,0,C>, ?)
(<2,0,A>, 10) (<2,0,C>, ?)
(<3,0,A>, 10) (<3,0,C>, ?)
(<5,0,A>, 10) (<5,0,C>, ?)
(<6,0,A>, 10) (<6,0,C>, ?)
(<8,0,A>, 0) (<8,0,C>, ?)
(<9,0,A>, 0) (<9,0,C>, 0)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 10
p(f10) = 10
p(f16) = 10 + -1*x1
p(f9) = 10
The following rules are strictly oriented:
[9 >= A && H >= 1] ==>
f16(A,C) = 10 + -1*A
> 9 + -1*A
= f16(1 + A,C)
The following rules are weakly oriented:
True ==>
f0(A,C) = 10
>= 10
= f9(0,H)
[0 >= 1 + C] ==>
f9(A,C) = 10
>= 10
= f10(A,C)
[C >= 1] ==>
f9(A,C) = 10
>= 10
= f10(A,C)
[9 >= A] ==>
f10(A,C) = 10
>= 10
= f9(1 + A,H)
[9 >= A && 0 >= 1 + H] ==>
f16(A,C) = 10 + -1*A
>= 9 + -1*A
= f16(1 + A,C)
[A >= 10] ==>
f10(A,C) = 10
>= 10
= f16(0,C)
[C = 0] ==>
f9(A,C) = 10
>= 10
= f16(0,0)
* Step 9: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C) -> f9(0,H) True (1,1)
1. f9(A,C) -> f10(A,C) [0 >= 1 + C] (?,1)
2. f9(A,C) -> f10(A,C) [C >= 1] (?,1)
3. f10(A,C) -> f9(1 + A,H) [9 >= A] (?,1)
5. f16(A,C) -> f16(1 + A,C) [9 >= A && 0 >= 1 + H] (?,1)
6. f16(A,C) -> f16(1 + A,C) [9 >= A && H >= 1] (10,1)
8. f10(A,C) -> f16(0,C) [A >= 10] (1,1)
9. f9(A,C) -> f16(0,0) [C = 0] (1,1)
Signature:
{(f0,2);(f10,2);(f16,2);(f28,2);(f9,2)}
Flow Graph:
[0->{1,2,9},1->{3,8},2->{3,8},3->{1,2,9},5->{5,6},6->{5,6},8->{5,6},9->{5,6}]
Sizebounds:
(<0,0,A>, 0) (<0,0,C>, ?)
(<1,0,A>, 10) (<1,0,C>, ?)
(<2,0,A>, 10) (<2,0,C>, ?)
(<3,0,A>, 10) (<3,0,C>, ?)
(<5,0,A>, 10) (<5,0,C>, ?)
(<6,0,A>, 10) (<6,0,C>, ?)
(<8,0,A>, 0) (<8,0,C>, ?)
(<9,0,A>, 0) (<9,0,C>, 0)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 10
p(f10) = 10
p(f16) = 10 + -1*x1
p(f9) = 10
The following rules are strictly oriented:
[9 >= A && 0 >= 1 + H] ==>
f16(A,C) = 10 + -1*A
> 9 + -1*A
= f16(1 + A,C)
[9 >= A && H >= 1] ==>
f16(A,C) = 10 + -1*A
> 9 + -1*A
= f16(1 + A,C)
The following rules are weakly oriented:
True ==>
f0(A,C) = 10
>= 10
= f9(0,H)
[0 >= 1 + C] ==>
f9(A,C) = 10
>= 10
= f10(A,C)
[C >= 1] ==>
f9(A,C) = 10
>= 10
= f10(A,C)
[9 >= A] ==>
f10(A,C) = 10
>= 10
= f9(1 + A,H)
[A >= 10] ==>
f10(A,C) = 10
>= 10
= f16(0,C)
[C = 0] ==>
f9(A,C) = 10
>= 10
= f16(0,0)
* Step 10: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C) -> f9(0,H) True (1,1)
1. f9(A,C) -> f10(A,C) [0 >= 1 + C] (?,1)
2. f9(A,C) -> f10(A,C) [C >= 1] (?,1)
3. f10(A,C) -> f9(1 + A,H) [9 >= A] (?,1)
5. f16(A,C) -> f16(1 + A,C) [9 >= A && 0 >= 1 + H] (10,1)
6. f16(A,C) -> f16(1 + A,C) [9 >= A && H >= 1] (10,1)
8. f10(A,C) -> f16(0,C) [A >= 10] (1,1)
9. f9(A,C) -> f16(0,0) [C = 0] (1,1)
Signature:
{(f0,2);(f10,2);(f16,2);(f28,2);(f9,2)}
Flow Graph:
[0->{1,2,9},1->{3,8},2->{3,8},3->{1,2,9},5->{5,6},6->{5,6},8->{5,6},9->{5,6}]
Sizebounds:
(<0,0,A>, 0) (<0,0,C>, ?)
(<1,0,A>, 10) (<1,0,C>, ?)
(<2,0,A>, 10) (<2,0,C>, ?)
(<3,0,A>, 10) (<3,0,C>, ?)
(<5,0,A>, 10) (<5,0,C>, ?)
(<6,0,A>, 10) (<6,0,C>, ?)
(<8,0,A>, 0) (<8,0,C>, ?)
(<9,0,A>, 0) (<9,0,C>, 0)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [1,3,2], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f10) = 10 + -1*x1
p(f9) = 10 + -1*x1
The following rules are strictly oriented:
[9 >= A] ==>
f10(A,C) = 10 + -1*A
> 9 + -1*A
= f9(1 + A,H)
The following rules are weakly oriented:
[0 >= 1 + C] ==>
f9(A,C) = 10 + -1*A
>= 10 + -1*A
= f10(A,C)
[C >= 1] ==>
f9(A,C) = 10 + -1*A
>= 10 + -1*A
= f10(A,C)
We use the following global sizebounds:
(<0,0,A>, 0) (<0,0,C>, ?)
(<1,0,A>, 10) (<1,0,C>, ?)
(<2,0,A>, 10) (<2,0,C>, ?)
(<3,0,A>, 10) (<3,0,C>, ?)
(<5,0,A>, 10) (<5,0,C>, ?)
(<6,0,A>, 10) (<6,0,C>, ?)
(<8,0,A>, 0) (<8,0,C>, ?)
(<9,0,A>, 0) (<9,0,C>, 0)
* Step 11: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C) -> f9(0,H) True (1,1)
1. f9(A,C) -> f10(A,C) [0 >= 1 + C] (?,1)
2. f9(A,C) -> f10(A,C) [C >= 1] (?,1)
3. f10(A,C) -> f9(1 + A,H) [9 >= A] (10,1)
5. f16(A,C) -> f16(1 + A,C) [9 >= A && 0 >= 1 + H] (10,1)
6. f16(A,C) -> f16(1 + A,C) [9 >= A && H >= 1] (10,1)
8. f10(A,C) -> f16(0,C) [A >= 10] (1,1)
9. f9(A,C) -> f16(0,0) [C = 0] (1,1)
Signature:
{(f0,2);(f10,2);(f16,2);(f28,2);(f9,2)}
Flow Graph:
[0->{1,2,9},1->{3,8},2->{3,8},3->{1,2,9},5->{5,6},6->{5,6},8->{5,6},9->{5,6}]
Sizebounds:
(<0,0,A>, 0) (<0,0,C>, ?)
(<1,0,A>, 10) (<1,0,C>, ?)
(<2,0,A>, 10) (<2,0,C>, ?)
(<3,0,A>, 10) (<3,0,C>, ?)
(<5,0,A>, 10) (<5,0,C>, ?)
(<6,0,A>, 10) (<6,0,C>, ?)
(<8,0,A>, 0) (<8,0,C>, ?)
(<9,0,A>, 0) (<9,0,C>, 0)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 12: LocalSizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,C) -> f9(0,H) True (1,1)
1. f9(A,C) -> f10(A,C) [0 >= 1 + C] (11,1)
2. f9(A,C) -> f10(A,C) [C >= 1] (11,1)
3. f10(A,C) -> f9(1 + A,H) [9 >= A] (10,1)
5. f16(A,C) -> f16(1 + A,C) [9 >= A && 0 >= 1 + H] (10,1)
6. f16(A,C) -> f16(1 + A,C) [9 >= A && H >= 1] (10,1)
8. f10(A,C) -> f16(0,C) [A >= 10] (1,1)
9. f9(A,C) -> f16(0,0) [C = 0] (1,1)
Signature:
{(f0,2);(f10,2);(f16,2);(f28,2);(f9,2)}
Flow Graph:
[0->{1,2,9},1->{3,8},2->{3,8},3->{1,2,9},5->{5,6},6->{5,6},8->{5,6},9->{5,6}]
Sizebounds:
(<0,0,A>, 0) (<0,0,C>, ?)
(<1,0,A>, 10) (<1,0,C>, ?)
(<2,0,A>, 10) (<2,0,C>, ?)
(<3,0,A>, 10) (<3,0,C>, ?)
(<5,0,A>, 10) (<5,0,C>, ?)
(<6,0,A>, 10) (<6,0,C>, ?)
(<8,0,A>, 0) (<8,0,C>, ?)
(<9,0,A>, 0) (<9,0,C>, 0)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
The problem is already solved.
WORST_CASE(?,O(1))