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