WORST_CASE(?,O(n^1))
* Step 1: TrivialSCCs WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,1 + B,D,B1,Y,Z,A1,C1,D1,E1,D,F1,B,N,O,P,Q,R,S,T,U,V,W,X) [A >= 1 + B && B >= 0] (?,1)
1. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (?,1)
2. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (?,1)
3. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (?,1)
4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (?,1)
5. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(E1,D1,F1,D,E,F,G,H,G1,J,K,L,M,C1,O,B1,Y,Z,A1,H1,U,V,W,X) [O >= 0 && E1 >= 2 && D1 >= E1 && 0 >= 1 + F1 && P = N] (?,1)
6. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(E1,D1,F1,D,E,F,G,H,G1,J,K,L,M,C1,O,B1,Y,Z,A1,H1,U,V,W,X) [O >= 0 && E1 >= 2 && D1 >= E1 && F1 >= 1 && P = N] (?,1)
7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1)
8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1)
10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,B,C,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [D1 >= 2 && U >= 0 && P = N] (?,1)
12. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1 && 0 >= 1 + C] (?,1)
13. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1)
14. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1)
15. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C && C >= 1] (?,1)
16. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,0,0,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [0 >= D1 && 0 >= A] (1,1)
17. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,2,Y,C1,Z,A1,B1,D1,E1,F1,Y,L,M,N,O,P,Q,R,S,T,U,V,W,G1) [A >= 2] (1,1)
Signature:
{(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)}
Flow Graph:
[0->{0,12,13,14,15},1->{7,8,9,10,11},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{},6->{},7->{7
,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},12->{7,8,9,10,11},13->{7,8,9,10,11}
,14->{7,8,9,10,11},15->{7,8,9,10,11},16->{},17->{0,12,13,14,15}]
+ Applied Processor:
TrivialSCCs
+ Details:
All trivial SCCs of the transition graph admit timebound 1.
* Step 2: RestrictVarsProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,1 + B,D,B1,Y,Z,A1,C1,D1,E1,D,F1,B,N,O,P,Q,R,S,T,U,V,W,X) [A >= 1 + B && B >= 0] (?,1)
1. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (1,1)
2. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (1,1)
3. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (1,1)
4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,U,V,W,X) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (1,1)
5. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(E1,D1,F1,D,E,F,G,H,G1,J,K,L,M,C1,O,B1,Y,Z,A1,H1,U,V,W,X) [O >= 0 && E1 >= 2 && D1 >= E1 && 0 >= 1 + F1 && P = N] (1,1)
6. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(E1,D1,F1,D,E,F,G,H,G1,J,K,L,M,C1,O,B1,Y,Z,A1,H1,U,V,W,X) [O >= 0 && E1 >= 2 && D1 >= E1 && F1 >= 1 && P = N] (1,1)
7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1)
8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1)
10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,B,C,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [D1 >= 2 && U >= 0 && P = N] (?,1)
12. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1 && 0 >= 1 + C] (?,1)
13. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1)
14. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1)
15. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C && C >= 1] (?,1)
16. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,0,0,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [0 >= D1 && 0 >= A] (1,1)
17. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,2,Y,C1,Z,A1,B1,D1,E1,F1,Y,L,M,N,O,P,Q,R,S,T,U,V,W,G1) [A >= 2] (1,1)
Signature:
{(f1,24);(f10,24);(f3,24);(f4,24);(f9,24)}
Flow Graph:
[0->{0,12,13,14,15},1->{7,8,9,10,11},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{},6->{},7->{7
,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},12->{7,8,9,10,11},13->{7,8,9,10,11}
,14->{7,8,9,10,11},15->{7,8,9,10,11},16->{},17->{0,12,13,14,15}]
+ Applied Processor:
RestrictVarsProcessor
+ Details:
We removed the arguments [E,F,G,H,I,J,K,L,M,Q,R,S,T,V,W,X] .
* Step 3: UnsatRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f1(A,B,C,D,N,O,P,U) -> f1(A,1 + B,D,B1,N,O,P,U) [A >= 1 + B && B >= 0] (?,1)
1. f9(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,U) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (?,1)
2. f9(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,U) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (?,1)
3. f9(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,U) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (?,1)
4. f9(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,U) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (?,1)
5. f9(A,B,C,D,N,O,P,U) -> f4(E1,D1,F1,D,C1,O,B1,U) [O >= 0 && E1 >= 2 && D1 >= E1 && 0 >= 1 + F1 && P = N] (?,1)
6. f9(A,B,C,D,N,O,P,U) -> f4(E1,D1,F1,D,C1,O,B1,U) [O >= 0 && E1 >= 2 && D1 >= E1 && F1 >= 1 && P = N] (?,1)
7. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1)
8. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
9. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1)
10. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
11. f10(A,B,C,D,N,O,P,U) -> f4(D1,B,C,D,C1,O,B1,U) [D1 >= 2 && U >= 0 && P = N] (?,1)
12. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1 && 0 >= 1 + C] (?,1)
13. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1)
14. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1)
15. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C && C >= 1] (?,1)
16. f3(A,B,C,D,N,O,P,U) -> f4(D1,0,0,D,C1,O,B1,U) [0 >= D1 && 0 >= A] (1,1)
17. f3(A,B,C,D,N,O,P,U) -> f1(A,2,Y,C1,N,O,P,U) [A >= 2] (1,1)
Signature:
{(f1,8);(f10,8);(f3,8);(f4,8);(f9,8)}
Flow Graph:
[0->{0,12,13,14,15},1->{7,8,9,10,11},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{},6->{},7->{7
,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},12->{7,8,9,10,11},13->{7,8,9,10,11}
,14->{7,8,9,10,11},15->{7,8,9,10,11},16->{},17->{0,12,13,14,15}]
+ Applied Processor:
UnsatRules
+ Details:
The following transitions have unsatisfiable constraints and are removed: [12,15]
* Step 4: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f1(A,B,C,D,N,O,P,U) -> f1(A,1 + B,D,B1,N,O,P,U) [A >= 1 + B && B >= 0] (?,1)
1. f9(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,U) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (?,1)
2. f9(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,U) [B1 >= 1 + N && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (?,1)
3. f9(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,U) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + B1 && P = 0] (?,1)
4. f9(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,U) [N >= 1 + B1 && O >= 0 && A1 >= 2 && Z >= A1 && B1 >= 1 + Y && P = 0] (?,1)
5. f9(A,B,C,D,N,O,P,U) -> f4(E1,D1,F1,D,C1,O,B1,U) [O >= 0 && E1 >= 2 && D1 >= E1 && 0 >= 1 + F1 && P = N] (?,1)
6. f9(A,B,C,D,N,O,P,U) -> f4(E1,D1,F1,D,C1,O,B1,U) [O >= 0 && E1 >= 2 && D1 >= E1 && F1 >= 1 && P = N] (?,1)
7. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1)
8. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
9. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1)
10. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
11. f10(A,B,C,D,N,O,P,U) -> f4(D1,B,C,D,C1,O,B1,U) [D1 >= 2 && U >= 0 && P = N] (?,1)
13. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1)
14. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1)
16. f3(A,B,C,D,N,O,P,U) -> f4(D1,0,0,D,C1,O,B1,U) [0 >= D1 && 0 >= A] (1,1)
17. f3(A,B,C,D,N,O,P,U) -> f1(A,2,Y,C1,N,O,P,U) [A >= 2] (1,1)
Signature:
{(f1,8);(f10,8);(f3,8);(f4,8);(f9,8)}
Flow Graph:
[0->{0,13,14},1->{7,8,9,10,11},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{},6->{},7->{7,8,9,10
,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},13->{7,8,9,10,11},14->{7,8,9,10,11},16->{}
,17->{0,13,14}]
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [1,2,3,4,5,6]
* Step 5: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f1(A,B,C,D,N,O,P,U) -> f1(A,1 + B,D,B1,N,O,P,U) [A >= 1 + B && B >= 0] (?,1)
7. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1)
8. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
9. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1)
10. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
11. f10(A,B,C,D,N,O,P,U) -> f4(D1,B,C,D,C1,O,B1,U) [D1 >= 2 && U >= 0 && P = N] (?,1)
13. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1)
14. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1)
16. f3(A,B,C,D,N,O,P,U) -> f4(D1,0,0,D,C1,O,B1,U) [0 >= D1 && 0 >= A] (1,1)
17. f3(A,B,C,D,N,O,P,U) -> f1(A,2,Y,C1,N,O,P,U) [A >= 2] (1,1)
Signature:
{(f1,8);(f10,8);(f3,8);(f4,8);(f9,8)}
Flow Graph:
[0->{0,13,14},7->{7,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},13->{7,8,9,10
,11},14->{7,8,9,10,11},16->{},17->{0,13,14}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,A>, A, .= 0) (< 0,0,B>, 1 + A + B, .* 1) (< 0,0,C>, D, .= 0) (< 0,0,D>, ?, .?) (< 0,0,N>, N, .= 0) (< 0,0,O>, O, .= 0) (< 0,0,P>, P, .= 0) (< 0,0,U>, U, .= 0)
(< 7,0,A>, ?, .?) (< 7,0,B>, ?, .?) (< 7,0,C>, ?, .?) (< 7,0,D>, D, .= 0) (< 7,0,N>, N, .= 0) (< 7,0,O>, O, .= 0) (< 7,0,P>, 0, .= 0) (< 7,0,U>, 1 + U, .+ 1)
(< 8,0,A>, ?, .?) (< 8,0,B>, ?, .?) (< 8,0,C>, ?, .?) (< 8,0,D>, D, .= 0) (< 8,0,N>, N, .= 0) (< 8,0,O>, O, .= 0) (< 8,0,P>, 0, .= 0) (< 8,0,U>, 1 + U, .+ 1)
(< 9,0,A>, ?, .?) (< 9,0,B>, ?, .?) (< 9,0,C>, ?, .?) (< 9,0,D>, D, .= 0) (< 9,0,N>, N, .= 0) (< 9,0,O>, O, .= 0) (< 9,0,P>, 0, .= 0) (< 9,0,U>, 1 + U, .+ 1)
(<10,0,A>, ?, .?) (<10,0,B>, ?, .?) (<10,0,C>, ?, .?) (<10,0,D>, D, .= 0) (<10,0,N>, N, .= 0) (<10,0,O>, O, .= 0) (<10,0,P>, 0, .= 0) (<10,0,U>, 1 + U, .+ 1)
(<11,0,A>, ?, .?) (<11,0,B>, B, .= 0) (<11,0,C>, C, .= 0) (<11,0,D>, D, .= 0) (<11,0,N>, ?, .?) (<11,0,O>, O, .= 0) (<11,0,P>, ?, .?) (<11,0,U>, U, .= 0)
(<13,0,A>, ?, .?) (<13,0,B>, 1 + U, .+ 1) (<13,0,C>, C, .= 0) (<13,0,D>, D, .= 0) (<13,0,N>, C, .= 0) (<13,0,O>, U, .= 0) (<13,0,P>, 0, .= 0) (<13,0,U>, U, .= 0)
(<14,0,A>, ?, .?) (<14,0,B>, 1 + U, .+ 1) (<14,0,C>, C, .= 0) (<14,0,D>, D, .= 0) (<14,0,N>, C, .= 0) (<14,0,O>, U, .= 0) (<14,0,P>, 0, .= 0) (<14,0,U>, U, .= 0)
(<16,0,A>, ?, .?) (<16,0,B>, 0, .= 0) (<16,0,C>, 0, .= 0) (<16,0,D>, D, .= 0) (<16,0,N>, ?, .?) (<16,0,O>, O, .= 0) (<16,0,P>, ?, .?) (<16,0,U>, U, .= 0)
(<17,0,A>, A, .= 0) (<17,0,B>, 2, .= 2) (<17,0,C>, ?, .?) (<17,0,D>, ?, .?) (<17,0,N>, N, .= 0) (<17,0,O>, O, .= 0) (<17,0,P>, P, .= 0) (<17,0,U>, U, .= 0)
* Step 6: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f1(A,B,C,D,N,O,P,U) -> f1(A,1 + B,D,B1,N,O,P,U) [A >= 1 + B && B >= 0] (?,1)
7. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1)
8. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
9. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1)
10. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
11. f10(A,B,C,D,N,O,P,U) -> f4(D1,B,C,D,C1,O,B1,U) [D1 >= 2 && U >= 0 && P = N] (?,1)
13. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1)
14. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1)
16. f3(A,B,C,D,N,O,P,U) -> f4(D1,0,0,D,C1,O,B1,U) [0 >= D1 && 0 >= A] (1,1)
17. f3(A,B,C,D,N,O,P,U) -> f1(A,2,Y,C1,N,O,P,U) [A >= 2] (1,1)
Signature:
{(f1,8);(f10,8);(f3,8);(f4,8);(f9,8)}
Flow Graph:
[0->{0,13,14},7->{7,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},13->{7,8,9,10
,11},14->{7,8,9,10,11},16->{},17->{0,13,14}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,N>, ?) (< 0,0,O>, ?) (< 0,0,P>, ?) (< 0,0,U>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,N>, ?) (< 7,0,O>, ?) (< 7,0,P>, ?) (< 7,0,U>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,N>, ?) (< 8,0,O>, ?) (< 8,0,P>, ?) (< 8,0,U>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,N>, ?) (< 9,0,O>, ?) (< 9,0,P>, ?) (< 9,0,U>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,N>, ?) (<10,0,O>, ?) (<10,0,P>, ?) (<10,0,U>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,N>, ?) (<11,0,O>, ?) (<11,0,P>, ?) (<11,0,U>, ?)
(<13,0,A>, ?) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,N>, ?) (<13,0,O>, ?) (<13,0,P>, ?) (<13,0,U>, ?)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,N>, ?) (<14,0,O>, ?) (<14,0,P>, ?) (<14,0,U>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,N>, ?) (<16,0,O>, ?) (<16,0,P>, ?) (<16,0,U>, ?)
(<17,0,A>, ?) (<17,0,B>, ?) (<17,0,C>, ?) (<17,0,D>, ?) (<17,0,N>, ?) (<17,0,O>, ?) (<17,0,P>, ?) (<17,0,U>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,N>, N) (< 0,0,O>, O) (< 0,0,P>, P) (< 0,0,U>, U)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,N>, ?) (< 7,0,O>, U) (< 7,0,P>, 0) (< 7,0,U>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,N>, ?) (< 8,0,O>, U) (< 8,0,P>, 0) (< 8,0,U>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,N>, ?) (< 9,0,O>, U) (< 9,0,P>, 0) (< 9,0,U>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,N>, ?) (<10,0,O>, U) (<10,0,P>, 0) (<10,0,U>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,N>, ?) (<11,0,O>, U) (<11,0,P>, ?) (<11,0,U>, ?)
(<13,0,A>, ?) (<13,0,B>, 1 + U) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,N>, ?) (<13,0,O>, U) (<13,0,P>, 0) (<13,0,U>, U)
(<14,0,A>, ?) (<14,0,B>, 1 + U) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,N>, ?) (<14,0,O>, U) (<14,0,P>, 0) (<14,0,U>, U)
(<16,0,A>, ?) (<16,0,B>, 0) (<16,0,C>, 0) (<16,0,D>, D) (<16,0,N>, ?) (<16,0,O>, O) (<16,0,P>, ?) (<16,0,U>, U)
(<17,0,A>, A) (<17,0,B>, 2) (<17,0,C>, ?) (<17,0,D>, ?) (<17,0,N>, N) (<17,0,O>, O) (<17,0,P>, P) (<17,0,U>, U)
* Step 7: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f1(A,B,C,D,N,O,P,U) -> f1(A,1 + B,D,B1,N,O,P,U) [A >= 1 + B && B >= 0] (?,1)
7. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1)
8. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
9. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1)
10. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
11. f10(A,B,C,D,N,O,P,U) -> f4(D1,B,C,D,C1,O,B1,U) [D1 >= 2 && U >= 0 && P = N] (?,1)
13. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1)
14. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1)
16. f3(A,B,C,D,N,O,P,U) -> f4(D1,0,0,D,C1,O,B1,U) [0 >= D1 && 0 >= A] (1,1)
17. f3(A,B,C,D,N,O,P,U) -> f1(A,2,Y,C1,N,O,P,U) [A >= 2] (1,1)
Signature:
{(f1,8);(f10,8);(f3,8);(f4,8);(f9,8)}
Flow Graph:
[0->{0,13,14},7->{7,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},13->{7,8,9,10
,11},14->{7,8,9,10,11},16->{},17->{0,13,14}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,N>, N) (< 0,0,O>, O) (< 0,0,P>, P) (< 0,0,U>, U)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,N>, ?) (< 7,0,O>, U) (< 7,0,P>, 0) (< 7,0,U>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,N>, ?) (< 8,0,O>, U) (< 8,0,P>, 0) (< 8,0,U>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,N>, ?) (< 9,0,O>, U) (< 9,0,P>, 0) (< 9,0,U>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,N>, ?) (<10,0,O>, U) (<10,0,P>, 0) (<10,0,U>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,N>, ?) (<11,0,O>, U) (<11,0,P>, ?) (<11,0,U>, ?)
(<13,0,A>, ?) (<13,0,B>, 1 + U) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,N>, ?) (<13,0,O>, U) (<13,0,P>, 0) (<13,0,U>, U)
(<14,0,A>, ?) (<14,0,B>, 1 + U) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,N>, ?) (<14,0,O>, U) (<14,0,P>, 0) (<14,0,U>, U)
(<16,0,A>, ?) (<16,0,B>, 0) (<16,0,C>, 0) (<16,0,D>, D) (<16,0,N>, ?) (<16,0,O>, O) (<16,0,P>, ?) (<16,0,U>, U)
(<17,0,A>, A) (<17,0,B>, 2) (<17,0,C>, ?) (<17,0,D>, ?) (<17,0,N>, N) (<17,0,O>, O) (<17,0,P>, P) (<17,0,U>, U)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(13,11),(14,11)]
* Step 8: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f1(A,B,C,D,N,O,P,U) -> f1(A,1 + B,D,B1,N,O,P,U) [A >= 1 + B && B >= 0] (?,1)
7. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1)
8. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
9. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1)
10. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
11. f10(A,B,C,D,N,O,P,U) -> f4(D1,B,C,D,C1,O,B1,U) [D1 >= 2 && U >= 0 && P = N] (?,1)
13. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1)
14. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1)
16. f3(A,B,C,D,N,O,P,U) -> f4(D1,0,0,D,C1,O,B1,U) [0 >= D1 && 0 >= A] (1,1)
17. f3(A,B,C,D,N,O,P,U) -> f1(A,2,Y,C1,N,O,P,U) [A >= 2] (1,1)
Signature:
{(f1,8);(f10,8);(f3,8);(f4,8);(f9,8)}
Flow Graph:
[0->{0,13,14},7->{7,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},13->{7,8,9,10}
,14->{7,8,9,10},16->{},17->{0,13,14}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,N>, N) (< 0,0,O>, O) (< 0,0,P>, P) (< 0,0,U>, U)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,N>, ?) (< 7,0,O>, U) (< 7,0,P>, 0) (< 7,0,U>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,N>, ?) (< 8,0,O>, U) (< 8,0,P>, 0) (< 8,0,U>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,N>, ?) (< 9,0,O>, U) (< 9,0,P>, 0) (< 9,0,U>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,N>, ?) (<10,0,O>, U) (<10,0,P>, 0) (<10,0,U>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,N>, ?) (<11,0,O>, U) (<11,0,P>, ?) (<11,0,U>, ?)
(<13,0,A>, ?) (<13,0,B>, 1 + U) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,N>, ?) (<13,0,O>, U) (<13,0,P>, 0) (<13,0,U>, U)
(<14,0,A>, ?) (<14,0,B>, 1 + U) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,N>, ?) (<14,0,O>, U) (<14,0,P>, 0) (<14,0,U>, U)
(<16,0,A>, ?) (<16,0,B>, 0) (<16,0,C>, 0) (<16,0,D>, D) (<16,0,N>, ?) (<16,0,O>, O) (<16,0,P>, ?) (<16,0,U>, U)
(<17,0,A>, A) (<17,0,B>, 2) (<17,0,C>, ?) (<17,0,D>, ?) (<17,0,N>, N) (<17,0,O>, O) (<17,0,P>, P) (<17,0,U>, U)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [11]
* Step 9: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f1(A,B,C,D,N,O,P,U) -> f1(A,1 + B,D,B1,N,O,P,U) [A >= 1 + B && B >= 0] (?,1)
7. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1)
8. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
9. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1)
10. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
13. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1)
14. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1)
16. f3(A,B,C,D,N,O,P,U) -> f4(D1,0,0,D,C1,O,B1,U) [0 >= D1 && 0 >= A] (1,1)
17. f3(A,B,C,D,N,O,P,U) -> f1(A,2,Y,C1,N,O,P,U) [A >= 2] (1,1)
Signature:
{(f1,8);(f10,8);(f3,8);(f4,8);(f9,8)}
Flow Graph:
[0->{0,13,14},7->{7,8,9,10},8->{7,8,9,10},9->{7,8,9,10},10->{7,8,9,10},13->{7,8,9,10},14->{7,8,9,10}
,16->{},17->{0,13,14}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,N>, N) (< 0,0,O>, O) (< 0,0,P>, P) (< 0,0,U>, U)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,N>, ?) (< 7,0,O>, U) (< 7,0,P>, 0) (< 7,0,U>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,N>, ?) (< 8,0,O>, U) (< 8,0,P>, 0) (< 8,0,U>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,N>, ?) (< 9,0,O>, U) (< 9,0,P>, 0) (< 9,0,U>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,N>, ?) (<10,0,O>, U) (<10,0,P>, 0) (<10,0,U>, ?)
(<13,0,A>, ?) (<13,0,B>, 1 + U) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,N>, ?) (<13,0,O>, U) (<13,0,P>, 0) (<13,0,U>, U)
(<14,0,A>, ?) (<14,0,B>, 1 + U) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,N>, ?) (<14,0,O>, U) (<14,0,P>, 0) (<14,0,U>, U)
(<16,0,A>, ?) (<16,0,B>, 0) (<16,0,C>, 0) (<16,0,D>, D) (<16,0,N>, ?) (<16,0,O>, O) (<16,0,P>, ?) (<16,0,U>, U)
(<17,0,A>, A) (<17,0,B>, 2) (<17,0,C>, ?) (<17,0,D>, ?) (<17,0,N>, N) (<17,0,O>, O) (<17,0,P>, P) (<17,0,U>, U)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f1) = 1 + x8
p(f10) = 1 + x8
p(f3) = 1 + x8
p(f4) = 1 + x8
The following rules are strictly oriented:
[C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 1 + U
> U
= f10(A1,Z,Y,D,N,O,0,-1 + U)
The following rules are weakly oriented:
[A >= 1 + B && B >= 0] ==>
f1(A,B,C,D,N,O,P,U) = 1 + U
>= 1 + U
= f1(A,1 + B,D,B1,N,O,P,U)
[C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 1 + U
>= U
= f10(A1,Z,Y,D,N,O,0,-1 + U)
[N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 1 + U
>= U
= f10(A1,Z,Y,D,N,O,0,-1 + U)
[N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 1 + U
>= U
= f10(A1,Z,Y,D,N,O,0,-1 + U)
[B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] ==>
f1(A,B,C,D,N,O,P,U) = 1 + U
>= 1 + U
= f10(Y,1 + U,C,D,C,U,0,U)
[B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] ==>
f1(A,B,C,D,N,O,P,U) = 1 + U
>= 1 + U
= f10(Y,1 + U,C,D,C,U,0,U)
[0 >= D1 && 0 >= A] ==>
f3(A,B,C,D,N,O,P,U) = 1 + U
>= 1 + U
= f4(D1,0,0,D,C1,O,B1,U)
[A >= 2] ==>
f3(A,B,C,D,N,O,P,U) = 1 + U
>= 1 + U
= f1(A,2,Y,C1,N,O,P,U)
* Step 10: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f1(A,B,C,D,N,O,P,U) -> f1(A,1 + B,D,B1,N,O,P,U) [A >= 1 + B && B >= 0] (?,1)
7. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (1 + U,1)
8. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
9. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1)
10. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
13. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1)
14. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1)
16. f3(A,B,C,D,N,O,P,U) -> f4(D1,0,0,D,C1,O,B1,U) [0 >= D1 && 0 >= A] (1,1)
17. f3(A,B,C,D,N,O,P,U) -> f1(A,2,Y,C1,N,O,P,U) [A >= 2] (1,1)
Signature:
{(f1,8);(f10,8);(f3,8);(f4,8);(f9,8)}
Flow Graph:
[0->{0,13,14},7->{7,8,9,10},8->{7,8,9,10},9->{7,8,9,10},10->{7,8,9,10},13->{7,8,9,10},14->{7,8,9,10}
,16->{},17->{0,13,14}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,N>, N) (< 0,0,O>, O) (< 0,0,P>, P) (< 0,0,U>, U)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,N>, ?) (< 7,0,O>, U) (< 7,0,P>, 0) (< 7,0,U>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,N>, ?) (< 8,0,O>, U) (< 8,0,P>, 0) (< 8,0,U>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,N>, ?) (< 9,0,O>, U) (< 9,0,P>, 0) (< 9,0,U>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,N>, ?) (<10,0,O>, U) (<10,0,P>, 0) (<10,0,U>, ?)
(<13,0,A>, ?) (<13,0,B>, 1 + U) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,N>, ?) (<13,0,O>, U) (<13,0,P>, 0) (<13,0,U>, U)
(<14,0,A>, ?) (<14,0,B>, 1 + U) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,N>, ?) (<14,0,O>, U) (<14,0,P>, 0) (<14,0,U>, U)
(<16,0,A>, ?) (<16,0,B>, 0) (<16,0,C>, 0) (<16,0,D>, D) (<16,0,N>, ?) (<16,0,O>, O) (<16,0,P>, ?) (<16,0,U>, U)
(<17,0,A>, A) (<17,0,B>, 2) (<17,0,C>, ?) (<17,0,D>, ?) (<17,0,N>, N) (<17,0,O>, O) (<17,0,P>, P) (<17,0,U>, U)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f1) = 1 + x8
p(f10) = 1 + x8
p(f3) = 1 + x8
p(f4) = 1 + x8
The following rules are strictly oriented:
[C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 1 + U
> U
= f10(A1,Z,Y,D,N,O,0,-1 + U)
[C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 1 + U
> U
= f10(A1,Z,Y,D,N,O,0,-1 + U)
The following rules are weakly oriented:
[A >= 1 + B && B >= 0] ==>
f1(A,B,C,D,N,O,P,U) = 1 + U
>= 1 + U
= f1(A,1 + B,D,B1,N,O,P,U)
[N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 1 + U
>= U
= f10(A1,Z,Y,D,N,O,0,-1 + U)
[N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 1 + U
>= U
= f10(A1,Z,Y,D,N,O,0,-1 + U)
[B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] ==>
f1(A,B,C,D,N,O,P,U) = 1 + U
>= 1 + U
= f10(Y,1 + U,C,D,C,U,0,U)
[B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] ==>
f1(A,B,C,D,N,O,P,U) = 1 + U
>= 1 + U
= f10(Y,1 + U,C,D,C,U,0,U)
[0 >= D1 && 0 >= A] ==>
f3(A,B,C,D,N,O,P,U) = 1 + U
>= 1 + U
= f4(D1,0,0,D,C1,O,B1,U)
[A >= 2] ==>
f3(A,B,C,D,N,O,P,U) = 1 + U
>= 1 + U
= f1(A,2,Y,C1,N,O,P,U)
* Step 11: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f1(A,B,C,D,N,O,P,U) -> f1(A,1 + B,D,B1,N,O,P,U) [A >= 1 + B && B >= 0] (?,1)
7. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (1 + U,1)
8. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (1 + U,1)
9. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (?,1)
10. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
13. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1)
14. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1)
16. f3(A,B,C,D,N,O,P,U) -> f4(D1,0,0,D,C1,O,B1,U) [0 >= D1 && 0 >= A] (1,1)
17. f3(A,B,C,D,N,O,P,U) -> f1(A,2,Y,C1,N,O,P,U) [A >= 2] (1,1)
Signature:
{(f1,8);(f10,8);(f3,8);(f4,8);(f9,8)}
Flow Graph:
[0->{0,13,14},7->{7,8,9,10},8->{7,8,9,10},9->{7,8,9,10},10->{7,8,9,10},13->{7,8,9,10},14->{7,8,9,10}
,16->{},17->{0,13,14}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,N>, N) (< 0,0,O>, O) (< 0,0,P>, P) (< 0,0,U>, U)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,N>, ?) (< 7,0,O>, U) (< 7,0,P>, 0) (< 7,0,U>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,N>, ?) (< 8,0,O>, U) (< 8,0,P>, 0) (< 8,0,U>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,N>, ?) (< 9,0,O>, U) (< 9,0,P>, 0) (< 9,0,U>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,N>, ?) (<10,0,O>, U) (<10,0,P>, 0) (<10,0,U>, ?)
(<13,0,A>, ?) (<13,0,B>, 1 + U) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,N>, ?) (<13,0,O>, U) (<13,0,P>, 0) (<13,0,U>, U)
(<14,0,A>, ?) (<14,0,B>, 1 + U) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,N>, ?) (<14,0,O>, U) (<14,0,P>, 0) (<14,0,U>, U)
(<16,0,A>, ?) (<16,0,B>, 0) (<16,0,C>, 0) (<16,0,D>, D) (<16,0,N>, ?) (<16,0,O>, O) (<16,0,P>, ?) (<16,0,U>, U)
(<17,0,A>, A) (<17,0,B>, 2) (<17,0,C>, ?) (<17,0,D>, ?) (<17,0,N>, N) (<17,0,O>, O) (<17,0,P>, P) (<17,0,U>, U)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f1) = 1 + x8
p(f10) = 1 + x8
p(f3) = 1 + x8
p(f4) = 1 + x8
The following rules are strictly oriented:
[C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 1 + U
> U
= f10(A1,Z,Y,D,N,O,0,-1 + U)
[C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 1 + U
> U
= f10(A1,Z,Y,D,N,O,0,-1 + U)
[N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 1 + U
> U
= f10(A1,Z,Y,D,N,O,0,-1 + U)
The following rules are weakly oriented:
[A >= 1 + B && B >= 0] ==>
f1(A,B,C,D,N,O,P,U) = 1 + U
>= 1 + U
= f1(A,1 + B,D,B1,N,O,P,U)
[N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 1 + U
>= U
= f10(A1,Z,Y,D,N,O,0,-1 + U)
[B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] ==>
f1(A,B,C,D,N,O,P,U) = 1 + U
>= 1 + U
= f10(Y,1 + U,C,D,C,U,0,U)
[B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] ==>
f1(A,B,C,D,N,O,P,U) = 1 + U
>= 1 + U
= f10(Y,1 + U,C,D,C,U,0,U)
[0 >= D1 && 0 >= A] ==>
f3(A,B,C,D,N,O,P,U) = 1 + U
>= 1 + U
= f4(D1,0,0,D,C1,O,B1,U)
[A >= 2] ==>
f3(A,B,C,D,N,O,P,U) = 1 + U
>= 1 + U
= f1(A,2,Y,C1,N,O,P,U)
* Step 12: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f1(A,B,C,D,N,O,P,U) -> f1(A,1 + B,D,B1,N,O,P,U) [A >= 1 + B && B >= 0] (?,1)
7. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (1 + U,1)
8. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (1 + U,1)
9. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (1 + U,1)
10. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (?,1)
13. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1)
14. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1)
16. f3(A,B,C,D,N,O,P,U) -> f4(D1,0,0,D,C1,O,B1,U) [0 >= D1 && 0 >= A] (1,1)
17. f3(A,B,C,D,N,O,P,U) -> f1(A,2,Y,C1,N,O,P,U) [A >= 2] (1,1)
Signature:
{(f1,8);(f10,8);(f3,8);(f4,8);(f9,8)}
Flow Graph:
[0->{0,13,14},7->{7,8,9,10},8->{7,8,9,10},9->{7,8,9,10},10->{7,8,9,10},13->{7,8,9,10},14->{7,8,9,10}
,16->{},17->{0,13,14}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,N>, N) (< 0,0,O>, O) (< 0,0,P>, P) (< 0,0,U>, U)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,N>, ?) (< 7,0,O>, U) (< 7,0,P>, 0) (< 7,0,U>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,N>, ?) (< 8,0,O>, U) (< 8,0,P>, 0) (< 8,0,U>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,N>, ?) (< 9,0,O>, U) (< 9,0,P>, 0) (< 9,0,U>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,N>, ?) (<10,0,O>, U) (<10,0,P>, 0) (<10,0,U>, ?)
(<13,0,A>, ?) (<13,0,B>, 1 + U) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,N>, ?) (<13,0,O>, U) (<13,0,P>, 0) (<13,0,U>, U)
(<14,0,A>, ?) (<14,0,B>, 1 + U) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,N>, ?) (<14,0,O>, U) (<14,0,P>, 0) (<14,0,U>, U)
(<16,0,A>, ?) (<16,0,B>, 0) (<16,0,C>, 0) (<16,0,D>, D) (<16,0,N>, ?) (<16,0,O>, O) (<16,0,P>, ?) (<16,0,U>, U)
(<17,0,A>, A) (<17,0,B>, 2) (<17,0,C>, ?) (<17,0,D>, ?) (<17,0,N>, N) (<17,0,O>, O) (<17,0,P>, P) (<17,0,U>, U)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f1) = 1 + x8
p(f10) = 1 + x8
p(f3) = 1 + x8
p(f4) = 1 + x8
The following rules are strictly oriented:
[C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 1 + U
> U
= f10(A1,Z,Y,D,N,O,0,-1 + U)
[C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 1 + U
> U
= f10(A1,Z,Y,D,N,O,0,-1 + U)
[N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 1 + U
> U
= f10(A1,Z,Y,D,N,O,0,-1 + U)
[N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 1 + U
> U
= f10(A1,Z,Y,D,N,O,0,-1 + U)
The following rules are weakly oriented:
[A >= 1 + B && B >= 0] ==>
f1(A,B,C,D,N,O,P,U) = 1 + U
>= 1 + U
= f1(A,1 + B,D,B1,N,O,P,U)
[B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] ==>
f1(A,B,C,D,N,O,P,U) = 1 + U
>= 1 + U
= f10(Y,1 + U,C,D,C,U,0,U)
[B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] ==>
f1(A,B,C,D,N,O,P,U) = 1 + U
>= 1 + U
= f10(Y,1 + U,C,D,C,U,0,U)
[0 >= D1 && 0 >= A] ==>
f3(A,B,C,D,N,O,P,U) = 1 + U
>= 1 + U
= f4(D1,0,0,D,C1,O,B1,U)
[A >= 2] ==>
f3(A,B,C,D,N,O,P,U) = 1 + U
>= 1 + U
= f1(A,2,Y,C1,N,O,P,U)
* Step 13: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f1(A,B,C,D,N,O,P,U) -> f1(A,1 + B,D,B1,N,O,P,U) [A >= 1 + B && B >= 0] (?,1)
7. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (1 + U,1)
8. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (1 + U,1)
9. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (1 + U,1)
10. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (1 + U,1)
13. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (?,1)
14. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1)
16. f3(A,B,C,D,N,O,P,U) -> f4(D1,0,0,D,C1,O,B1,U) [0 >= D1 && 0 >= A] (1,1)
17. f3(A,B,C,D,N,O,P,U) -> f1(A,2,Y,C1,N,O,P,U) [A >= 2] (1,1)
Signature:
{(f1,8);(f10,8);(f3,8);(f4,8);(f9,8)}
Flow Graph:
[0->{0,13,14},7->{7,8,9,10},8->{7,8,9,10},9->{7,8,9,10},10->{7,8,9,10},13->{7,8,9,10},14->{7,8,9,10}
,16->{},17->{0,13,14}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,N>, N) (< 0,0,O>, O) (< 0,0,P>, P) (< 0,0,U>, U)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,N>, ?) (< 7,0,O>, U) (< 7,0,P>, 0) (< 7,0,U>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,N>, ?) (< 8,0,O>, U) (< 8,0,P>, 0) (< 8,0,U>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,N>, ?) (< 9,0,O>, U) (< 9,0,P>, 0) (< 9,0,U>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,N>, ?) (<10,0,O>, U) (<10,0,P>, 0) (<10,0,U>, ?)
(<13,0,A>, ?) (<13,0,B>, 1 + U) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,N>, ?) (<13,0,O>, U) (<13,0,P>, 0) (<13,0,U>, U)
(<14,0,A>, ?) (<14,0,B>, 1 + U) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,N>, ?) (<14,0,O>, U) (<14,0,P>, 0) (<14,0,U>, U)
(<16,0,A>, ?) (<16,0,B>, 0) (<16,0,C>, 0) (<16,0,D>, D) (<16,0,N>, ?) (<16,0,O>, O) (<16,0,P>, ?) (<16,0,U>, U)
(<17,0,A>, A) (<17,0,B>, 2) (<17,0,C>, ?) (<17,0,D>, ?) (<17,0,N>, N) (<17,0,O>, O) (<17,0,P>, P) (<17,0,U>, U)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f1) = 1
p(f10) = 0
p(f3) = 1
p(f4) = 1
The following rules are strictly oriented:
[B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] ==>
f1(A,B,C,D,N,O,P,U) = 1
> 0
= f10(Y,1 + U,C,D,C,U,0,U)
The following rules are weakly oriented:
[A >= 1 + B && B >= 0] ==>
f1(A,B,C,D,N,O,P,U) = 1
>= 1
= f1(A,1 + B,D,B1,N,O,P,U)
[C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 0
>= 0
= f10(A1,Z,Y,D,N,O,0,-1 + U)
[C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 0
>= 0
= f10(A1,Z,Y,D,N,O,0,-1 + U)
[N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 0
>= 0
= f10(A1,Z,Y,D,N,O,0,-1 + U)
[N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 0
>= 0
= f10(A1,Z,Y,D,N,O,0,-1 + U)
[B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] ==>
f1(A,B,C,D,N,O,P,U) = 1
>= 0
= f10(Y,1 + U,C,D,C,U,0,U)
[0 >= D1 && 0 >= A] ==>
f3(A,B,C,D,N,O,P,U) = 1
>= 1
= f4(D1,0,0,D,C1,O,B1,U)
[A >= 2] ==>
f3(A,B,C,D,N,O,P,U) = 1
>= 1
= f1(A,2,Y,C1,N,O,P,U)
* Step 14: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f1(A,B,C,D,N,O,P,U) -> f1(A,1 + B,D,B1,N,O,P,U) [A >= 1 + B && B >= 0] (?,1)
7. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (1 + U,1)
8. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (1 + U,1)
9. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (1 + U,1)
10. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (1 + U,1)
13. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (1,1)
14. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (?,1)
16. f3(A,B,C,D,N,O,P,U) -> f4(D1,0,0,D,C1,O,B1,U) [0 >= D1 && 0 >= A] (1,1)
17. f3(A,B,C,D,N,O,P,U) -> f1(A,2,Y,C1,N,O,P,U) [A >= 2] (1,1)
Signature:
{(f1,8);(f10,8);(f3,8);(f4,8);(f9,8)}
Flow Graph:
[0->{0,13,14},7->{7,8,9,10},8->{7,8,9,10},9->{7,8,9,10},10->{7,8,9,10},13->{7,8,9,10},14->{7,8,9,10}
,16->{},17->{0,13,14}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,N>, N) (< 0,0,O>, O) (< 0,0,P>, P) (< 0,0,U>, U)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,N>, ?) (< 7,0,O>, U) (< 7,0,P>, 0) (< 7,0,U>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,N>, ?) (< 8,0,O>, U) (< 8,0,P>, 0) (< 8,0,U>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,N>, ?) (< 9,0,O>, U) (< 9,0,P>, 0) (< 9,0,U>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,N>, ?) (<10,0,O>, U) (<10,0,P>, 0) (<10,0,U>, ?)
(<13,0,A>, ?) (<13,0,B>, 1 + U) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,N>, ?) (<13,0,O>, U) (<13,0,P>, 0) (<13,0,U>, U)
(<14,0,A>, ?) (<14,0,B>, 1 + U) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,N>, ?) (<14,0,O>, U) (<14,0,P>, 0) (<14,0,U>, U)
(<16,0,A>, ?) (<16,0,B>, 0) (<16,0,C>, 0) (<16,0,D>, D) (<16,0,N>, ?) (<16,0,O>, O) (<16,0,P>, ?) (<16,0,U>, U)
(<17,0,A>, A) (<17,0,B>, 2) (<17,0,C>, ?) (<17,0,D>, ?) (<17,0,N>, N) (<17,0,O>, O) (<17,0,P>, P) (<17,0,U>, U)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f1) = 1
p(f10) = 0
p(f3) = 1
p(f4) = 1
The following rules are strictly oriented:
[B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] ==>
f1(A,B,C,D,N,O,P,U) = 1
> 0
= f10(Y,1 + U,C,D,C,U,0,U)
[B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] ==>
f1(A,B,C,D,N,O,P,U) = 1
> 0
= f10(Y,1 + U,C,D,C,U,0,U)
The following rules are weakly oriented:
[A >= 1 + B && B >= 0] ==>
f1(A,B,C,D,N,O,P,U) = 1
>= 1
= f1(A,1 + B,D,B1,N,O,P,U)
[C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 0
>= 0
= f10(A1,Z,Y,D,N,O,0,-1 + U)
[C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 0
>= 0
= f10(A1,Z,Y,D,N,O,0,-1 + U)
[N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 0
>= 0
= f10(A1,Z,Y,D,N,O,0,-1 + U)
[N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] ==>
f10(A,B,C,D,N,O,P,U) = 0
>= 0
= f10(A1,Z,Y,D,N,O,0,-1 + U)
[0 >= D1 && 0 >= A] ==>
f3(A,B,C,D,N,O,P,U) = 1
>= 1
= f4(D1,0,0,D,C1,O,B1,U)
[A >= 2] ==>
f3(A,B,C,D,N,O,P,U) = 1
>= 1
= f1(A,2,Y,C1,N,O,P,U)
* Step 15: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f1(A,B,C,D,N,O,P,U) -> f1(A,1 + B,D,B1,N,O,P,U) [A >= 1 + B && B >= 0] (?,1)
7. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (1 + U,1)
8. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (1 + U,1)
9. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (1 + U,1)
10. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (1 + U,1)
13. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (1,1)
14. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (1,1)
16. f3(A,B,C,D,N,O,P,U) -> f4(D1,0,0,D,C1,O,B1,U) [0 >= D1 && 0 >= A] (1,1)
17. f3(A,B,C,D,N,O,P,U) -> f1(A,2,Y,C1,N,O,P,U) [A >= 2] (1,1)
Signature:
{(f1,8);(f10,8);(f3,8);(f4,8);(f9,8)}
Flow Graph:
[0->{0,13,14},7->{7,8,9,10},8->{7,8,9,10},9->{7,8,9,10},10->{7,8,9,10},13->{7,8,9,10},14->{7,8,9,10}
,16->{},17->{0,13,14}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,N>, N) (< 0,0,O>, O) (< 0,0,P>, P) (< 0,0,U>, U)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,N>, ?) (< 7,0,O>, U) (< 7,0,P>, 0) (< 7,0,U>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,N>, ?) (< 8,0,O>, U) (< 8,0,P>, 0) (< 8,0,U>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,N>, ?) (< 9,0,O>, U) (< 9,0,P>, 0) (< 9,0,U>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,N>, ?) (<10,0,O>, U) (<10,0,P>, 0) (<10,0,U>, ?)
(<13,0,A>, ?) (<13,0,B>, 1 + U) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,N>, ?) (<13,0,O>, U) (<13,0,P>, 0) (<13,0,U>, U)
(<14,0,A>, ?) (<14,0,B>, 1 + U) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,N>, ?) (<14,0,O>, U) (<14,0,P>, 0) (<14,0,U>, U)
(<16,0,A>, ?) (<16,0,B>, 0) (<16,0,C>, 0) (<16,0,D>, D) (<16,0,N>, ?) (<16,0,O>, O) (<16,0,P>, ?) (<16,0,U>, U)
(<17,0,A>, A) (<17,0,B>, 2) (<17,0,C>, ?) (<17,0,D>, ?) (<17,0,N>, N) (<17,0,O>, O) (<17,0,P>, P) (<17,0,U>, U)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [0], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f1) = x1 + -1*x2
The following rules are strictly oriented:
[A >= 1 + B && B >= 0] ==>
f1(A,B,C,D,N,O,P,U) = A + -1*B
> -1 + A + -1*B
= f1(A,1 + B,D,B1,N,O,P,U)
The following rules are weakly oriented:
We use the following global sizebounds:
(< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,N>, N) (< 0,0,O>, O) (< 0,0,P>, P) (< 0,0,U>, U)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,N>, ?) (< 7,0,O>, U) (< 7,0,P>, 0) (< 7,0,U>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,N>, ?) (< 8,0,O>, U) (< 8,0,P>, 0) (< 8,0,U>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,N>, ?) (< 9,0,O>, U) (< 9,0,P>, 0) (< 9,0,U>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,N>, ?) (<10,0,O>, U) (<10,0,P>, 0) (<10,0,U>, ?)
(<13,0,A>, ?) (<13,0,B>, 1 + U) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,N>, ?) (<13,0,O>, U) (<13,0,P>, 0) (<13,0,U>, U)
(<14,0,A>, ?) (<14,0,B>, 1 + U) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,N>, ?) (<14,0,O>, U) (<14,0,P>, 0) (<14,0,U>, U)
(<16,0,A>, ?) (<16,0,B>, 0) (<16,0,C>, 0) (<16,0,D>, D) (<16,0,N>, ?) (<16,0,O>, O) (<16,0,P>, ?) (<16,0,U>, U)
(<17,0,A>, A) (<17,0,B>, 2) (<17,0,C>, ?) (<17,0,D>, ?) (<17,0,N>, N) (<17,0,O>, O) (<17,0,P>, P) (<17,0,U>, U)
* Step 16: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f1(A,B,C,D,N,O,P,U) -> f1(A,1 + B,D,B1,N,O,P,U) [A >= 1 + B && B >= 0] (2 + A,1)
7. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (1 + U,1)
8. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (1 + U,1)
9. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] (1 + U,1)
10. f10(A,B,C,D,N,O,P,U) -> f10(A1,Z,Y,D,N,O,0,-1 + U) [N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] (1 + U,1)
13. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] (1,1)
14. f1(A,B,C,D,N,O,P,U) -> f10(Y,1 + U,C,D,C,U,0,U) [B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] (1,1)
16. f3(A,B,C,D,N,O,P,U) -> f4(D1,0,0,D,C1,O,B1,U) [0 >= D1 && 0 >= A] (1,1)
17. f3(A,B,C,D,N,O,P,U) -> f1(A,2,Y,C1,N,O,P,U) [A >= 2] (1,1)
Signature:
{(f1,8);(f10,8);(f3,8);(f4,8);(f9,8)}
Flow Graph:
[0->{0,13,14},7->{7,8,9,10},8->{7,8,9,10},9->{7,8,9,10},10->{7,8,9,10},13->{7,8,9,10},14->{7,8,9,10}
,16->{},17->{0,13,14}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,N>, N) (< 0,0,O>, O) (< 0,0,P>, P) (< 0,0,U>, U)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,N>, ?) (< 7,0,O>, U) (< 7,0,P>, 0) (< 7,0,U>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,N>, ?) (< 8,0,O>, U) (< 8,0,P>, 0) (< 8,0,U>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,N>, ?) (< 9,0,O>, U) (< 9,0,P>, 0) (< 9,0,U>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,N>, ?) (<10,0,O>, U) (<10,0,P>, 0) (<10,0,U>, ?)
(<13,0,A>, ?) (<13,0,B>, 1 + U) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,N>, ?) (<13,0,O>, U) (<13,0,P>, 0) (<13,0,U>, U)
(<14,0,A>, ?) (<14,0,B>, 1 + U) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,N>, ?) (<14,0,O>, U) (<14,0,P>, 0) (<14,0,U>, U)
(<16,0,A>, ?) (<16,0,B>, 0) (<16,0,C>, 0) (<16,0,D>, D) (<16,0,N>, ?) (<16,0,O>, O) (<16,0,P>, ?) (<16,0,U>, U)
(<17,0,A>, A) (<17,0,B>, 2) (<17,0,C>, ?) (<17,0,D>, ?) (<17,0,N>, N) (<17,0,O>, O) (<17,0,P>, P) (<17,0,U>, U)
+ Applied Processor:
KnowledgePropagation
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))