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