WORST_CASE(?,O(1))
* Step 1: TrivialSCCs WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f12(A,B,C,D,E,F) -> f5(400,0,0,D,E,F) True (1,1)
1. f5(A,B,C,D,E,F) -> f11(A,B,0,0,0,F) [B >= A && C = 0] (?,1)
2. f5(A,B,C,D,E,F) -> f10(A,B,C,C,C,F) [C >= 1] (?,1)
3. f5(A,B,C,D,E,F) -> f10(A,B,C,C,C,F) [0 >= 1 + C] (?,1)
4. f7(A,B,C,D,E,F) -> f5(A,1 + B,G,H,E,G) True (?,1)
5. f8(A,B,C,D,E,F) -> f5(A,1 + B,G,H,E,G) True (?,1)
6. f5(A,B,C,D,E,F) -> f5(A,1 + B,G,H,E,G) [A >= 1 + B && C = 0] (?,1)
Signature:
{(f10,6);(f11,6);(f12,6);(f5,6);(f7,6);(f8,6)}
Flow Graph:
[0->{1,2,3,6},1->{},2->{},3->{},4->{1,2,3,6},5->{1,2,3,6},6->{1,2,3,6}]
+ Applied Processor:
TrivialSCCs
+ Details:
All trivial SCCs of the transition graph admit timebound 1.
* Step 2: RestrictVarsProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f12(A,B,C,D,E,F) -> f5(400,0,0,D,E,F) True (1,1)
1. f5(A,B,C,D,E,F) -> f11(A,B,0,0,0,F) [B >= A && C = 0] (?,1)
2. f5(A,B,C,D,E,F) -> f10(A,B,C,C,C,F) [C >= 1] (?,1)
3. f5(A,B,C,D,E,F) -> f10(A,B,C,C,C,F) [0 >= 1 + C] (?,1)
4. f7(A,B,C,D,E,F) -> f5(A,1 + B,G,H,E,G) True (1,1)
5. f8(A,B,C,D,E,F) -> f5(A,1 + B,G,H,E,G) True (1,1)
6. f5(A,B,C,D,E,F) -> f5(A,1 + B,G,H,E,G) [A >= 1 + B && C = 0] (?,1)
Signature:
{(f10,6);(f11,6);(f12,6);(f5,6);(f7,6);(f8,6)}
Flow Graph:
[0->{1,2,3,6},1->{},2->{},3->{},4->{1,2,3,6},5->{1,2,3,6},6->{1,2,3,6}]
+ Applied Processor:
RestrictVarsProcessor
+ Details:
We removed the arguments [D,E,F] .
* Step 3: UnreachableRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f12(A,B,C) -> f5(400,0,0) True (1,1)
1. f5(A,B,C) -> f11(A,B,0) [B >= A && C = 0] (?,1)
2. f5(A,B,C) -> f10(A,B,C) [C >= 1] (?,1)
3. f5(A,B,C) -> f10(A,B,C) [0 >= 1 + C] (?,1)
4. f7(A,B,C) -> f5(A,1 + B,G) True (?,1)
5. f8(A,B,C) -> f5(A,1 + B,G) True (?,1)
6. f5(A,B,C) -> f5(A,1 + B,G) [A >= 1 + B && C = 0] (?,1)
Signature:
{(f10,3);(f11,3);(f12,3);(f5,3);(f7,3);(f8,3)}
Flow Graph:
[0->{1,2,3,6},1->{},2->{},3->{},4->{1,2,3,6},5->{1,2,3,6},6->{1,2,3,6}]
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [4,5]
* Step 4: LocalSizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f12(A,B,C) -> f5(400,0,0) True (1,1)
1. f5(A,B,C) -> f11(A,B,0) [B >= A && C = 0] (?,1)
2. f5(A,B,C) -> f10(A,B,C) [C >= 1] (?,1)
3. f5(A,B,C) -> f10(A,B,C) [0 >= 1 + C] (?,1)
6. f5(A,B,C) -> f5(A,1 + B,G) [A >= 1 + B && C = 0] (?,1)
Signature:
{(f10,3);(f11,3);(f12,3);(f5,3);(f7,3);(f8,3)}
Flow Graph:
[0->{1,2,3,6},1->{},2->{},3->{},6->{1,2,3,6}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<0,0,A>, 400, .= 400) (<0,0,B>, 0, .= 0) (<0,0,C>, 0, .= 0)
(<1,0,A>, A, .= 0) (<1,0,B>, B, .= 0) (<1,0,C>, 0, .= 0)
(<2,0,A>, A, .= 0) (<2,0,B>, B, .= 0) (<2,0,C>, C, .= 0)
(<3,0,A>, A, .= 0) (<3,0,B>, B, .= 0) (<3,0,C>, C, .= 0)
(<6,0,A>, A, .= 0) (<6,0,B>, 1 + B, .+ 1) (<6,0,C>, ?, .?)
* Step 5: SizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f12(A,B,C) -> f5(400,0,0) True (1,1)
1. f5(A,B,C) -> f11(A,B,0) [B >= A && C = 0] (?,1)
2. f5(A,B,C) -> f10(A,B,C) [C >= 1] (?,1)
3. f5(A,B,C) -> f10(A,B,C) [0 >= 1 + C] (?,1)
6. f5(A,B,C) -> f5(A,1 + B,G) [A >= 1 + B && C = 0] (?,1)
Signature:
{(f10,3);(f11,3);(f12,3);(f5,3);(f7,3);(f8,3)}
Flow Graph:
[0->{1,2,3,6},1->{},2->{},3->{},6->{1,2,3,6}]
Sizebounds:
(<0,0,A>, ?) (<0,0,B>, ?) (<0,0,C>, ?)
(<1,0,A>, ?) (<1,0,B>, ?) (<1,0,C>, ?)
(<2,0,A>, ?) (<2,0,B>, ?) (<2,0,C>, ?)
(<3,0,A>, ?) (<3,0,B>, ?) (<3,0,C>, ?)
(<6,0,A>, ?) (<6,0,B>, ?) (<6,0,C>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<0,0,A>, 400) (<0,0,B>, 0) (<0,0,C>, 0)
(<1,0,A>, 400) (<1,0,B>, 400) (<1,0,C>, 0)
(<2,0,A>, 400) (<2,0,B>, 400) (<2,0,C>, ?)
(<3,0,A>, 400) (<3,0,B>, 400) (<3,0,C>, ?)
(<6,0,A>, 400) (<6,0,B>, 400) (<6,0,C>, ?)
* Step 6: UnsatPaths WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f12(A,B,C) -> f5(400,0,0) True (1,1)
1. f5(A,B,C) -> f11(A,B,0) [B >= A && C = 0] (?,1)
2. f5(A,B,C) -> f10(A,B,C) [C >= 1] (?,1)
3. f5(A,B,C) -> f10(A,B,C) [0 >= 1 + C] (?,1)
6. f5(A,B,C) -> f5(A,1 + B,G) [A >= 1 + B && C = 0] (?,1)
Signature:
{(f10,3);(f11,3);(f12,3);(f5,3);(f7,3);(f8,3)}
Flow Graph:
[0->{1,2,3,6},1->{},2->{},3->{},6->{1,2,3,6}]
Sizebounds:
(<0,0,A>, 400) (<0,0,B>, 0) (<0,0,C>, 0)
(<1,0,A>, 400) (<1,0,B>, 400) (<1,0,C>, 0)
(<2,0,A>, 400) (<2,0,B>, 400) (<2,0,C>, ?)
(<3,0,A>, 400) (<3,0,B>, 400) (<3,0,C>, ?)
(<6,0,A>, 400) (<6,0,B>, 400) (<6,0,C>, ?)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(0,1),(0,2),(0,3)]
* Step 7: LeafRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f12(A,B,C) -> f5(400,0,0) True (1,1)
1. f5(A,B,C) -> f11(A,B,0) [B >= A && C = 0] (?,1)
2. f5(A,B,C) -> f10(A,B,C) [C >= 1] (?,1)
3. f5(A,B,C) -> f10(A,B,C) [0 >= 1 + C] (?,1)
6. f5(A,B,C) -> f5(A,1 + B,G) [A >= 1 + B && C = 0] (?,1)
Signature:
{(f10,3);(f11,3);(f12,3);(f5,3);(f7,3);(f8,3)}
Flow Graph:
[0->{6},1->{},2->{},3->{},6->{1,2,3,6}]
Sizebounds:
(<0,0,A>, 400) (<0,0,B>, 0) (<0,0,C>, 0)
(<1,0,A>, 400) (<1,0,B>, 400) (<1,0,C>, 0)
(<2,0,A>, 400) (<2,0,B>, 400) (<2,0,C>, ?)
(<3,0,A>, 400) (<3,0,B>, 400) (<3,0,C>, ?)
(<6,0,A>, 400) (<6,0,B>, 400) (<6,0,C>, ?)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [1,2,3]
* Step 8: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f12(A,B,C) -> f5(400,0,0) True (1,1)
6. f5(A,B,C) -> f5(A,1 + B,G) [A >= 1 + B && C = 0] (?,1)
Signature:
{(f10,3);(f11,3);(f12,3);(f5,3);(f7,3);(f8,3)}
Flow Graph:
[0->{6},6->{6}]
Sizebounds:
(<0,0,A>, 400) (<0,0,B>, 0) (<0,0,C>, 0)
(<6,0,A>, 400) (<6,0,B>, 400) (<6,0,C>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f12) = 400
p(f5) = x1 + -1*x2
The following rules are strictly oriented:
[A >= 1 + B && C = 0] ==>
f5(A,B,C) = A + -1*B
> -1 + A + -1*B
= f5(A,1 + B,G)
The following rules are weakly oriented:
True ==>
f12(A,B,C) = 400
>= 400
= f5(400,0,0)
* Step 9: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f12(A,B,C) -> f5(400,0,0) True (1,1)
6. f5(A,B,C) -> f5(A,1 + B,G) [A >= 1 + B && C = 0] (400,1)
Signature:
{(f10,3);(f11,3);(f12,3);(f5,3);(f7,3);(f8,3)}
Flow Graph:
[0->{6},6->{6}]
Sizebounds:
(<0,0,A>, 400) (<0,0,B>, 0) (<0,0,C>, 0)
(<6,0,A>, 400) (<6,0,B>, 400) (<6,0,C>, ?)
+ Applied Processor:
KnowledgePropagation
+ Details:
The problem is already solved.
WORST_CASE(?,O(1))