WORST_CASE(?,O(n^2))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. doSum(A,B) -> m9(A,B) [A >= 0] (1,1)
1. m0(A,B) -> m1(A,B) [A >= 0] (?,1)
2. m2(A,B) -> m3(A,B) [1 + A >= 0] (?,1)
3. m1(A,B) -> m5(A,B) [A >= 0] (?,1)
4. m6(A,B) -> m4(A,B) [A >= 0 && 0 >= A] (?,1)
5. m7(A,B) -> c2(m4(C,B),m0(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A] (?,1)
6. m5(A,B) -> m8(A,B) [A >= 0] (?,1)
7. m8(A,B) -> m7(A,B) True (?,1)
8. m8(A,B) -> m6(A,B) True (?,1)
9. n2(A,B) -> c2(n0(A,B),m2(A,B)) [A >= 0] (?,1)
10. m9(A,B) -> n2(A,B) [A >= 0] (?,1)
11. n30(A,B) -> m2(A,B) True (?,1)
12. n31(A,B) -> m0(B,B) True (?,1)
13. n3(A,B) -> c2(n30(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A] (?,1)
14. m3(A,B) -> n3(A,B) True (?,1)
15. m3(A,B) -> n1(A,B) True (?,1)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[0->{10},1->{3},2->{14,15},3->{6},4->{},5->{1},6->{7,8},7->{5},8->{4},9->{2},10->{9},11->{2},12->{1}
,13->{11,12},14->{13},15->{}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,A>, A, .= 0) (< 0,0,B>, B, .= 0)
(< 1,0,A>, A, .= 0) (< 1,0,B>, B, .= 0)
(< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0)
(< 3,0,A>, A, .= 0) (< 3,0,B>, B, .= 0)
(< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0)
(< 5,0,A>, 1 + A, .+ 1) (< 5,0,B>, B, .= 0)
(< 5,1,A>, 1 + A, .+ 1) (< 5,1,B>, B, .= 0)
(< 6,0,A>, A, .= 0) (< 6,0,B>, B, .= 0)
(< 7,0,A>, A, .= 0) (< 7,0,B>, B, .= 0)
(< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0)
(< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0)
(< 9,1,A>, A, .= 0) (< 9,1,B>, B, .= 0)
(<10,0,A>, A, .= 0) (<10,0,B>, B, .= 0)
(<11,0,A>, A, .= 0) (<11,0,B>, B, .= 0)
(<12,0,A>, B, .= 0) (<12,0,B>, B, .= 0)
(<13,0,A>, 1 + A, .+ 1) (<13,0,B>, A, .= 0)
(<13,1,A>, 1 + A, .+ 1) (<13,1,B>, A, .= 0)
(<14,0,A>, A, .= 0) (<14,0,B>, B, .= 0)
(<15,0,A>, A, .= 0) (<15,0,B>, B, .= 0)
* Step 2: SizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. doSum(A,B) -> m9(A,B) [A >= 0] (1,1)
1. m0(A,B) -> m1(A,B) [A >= 0] (?,1)
2. m2(A,B) -> m3(A,B) [1 + A >= 0] (?,1)
3. m1(A,B) -> m5(A,B) [A >= 0] (?,1)
4. m6(A,B) -> m4(A,B) [A >= 0 && 0 >= A] (?,1)
5. m7(A,B) -> c2(m4(C,B),m0(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A] (?,1)
6. m5(A,B) -> m8(A,B) [A >= 0] (?,1)
7. m8(A,B) -> m7(A,B) True (?,1)
8. m8(A,B) -> m6(A,B) True (?,1)
9. n2(A,B) -> c2(n0(A,B),m2(A,B)) [A >= 0] (?,1)
10. m9(A,B) -> n2(A,B) [A >= 0] (?,1)
11. n30(A,B) -> m2(A,B) True (?,1)
12. n31(A,B) -> m0(B,B) True (?,1)
13. n3(A,B) -> c2(n30(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A] (?,1)
14. m3(A,B) -> n3(A,B) True (?,1)
15. m3(A,B) -> n1(A,B) True (?,1)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[0->{10},1->{3},2->{14,15},3->{6},4->{},5->{1},6->{7,8},7->{5},8->{4},9->{2},10->{9},11->{2},12->{1}
,13->{11,12},14->{13},15->{}]
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>, ?)
(< 5,1,A>, ?) (< 5,1,B>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?)
(< 9,1,A>, ?) (< 9,1,B>, ?)
(<10,0,A>, ?) (<10,0,B>, ?)
(<11,0,A>, ?) (<11,0,B>, ?)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<13,1,A>, ?) (<13,1,B>, ?)
(<14,0,A>, ?) (<14,0,B>, ?)
(<15,0,A>, ?) (<15,0,B>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, A) (< 0,0,B>, 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>, ?)
(< 5,1,A>, ?) (< 5,1,B>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?)
(< 9,0,A>, A) (< 9,0,B>, B)
(< 9,1,A>, A) (< 9,1,B>, B)
(<10,0,A>, A) (<10,0,B>, B)
(<11,0,A>, ?) (<11,0,B>, ?)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<13,1,A>, ?) (<13,1,B>, ?)
(<14,0,A>, ?) (<14,0,B>, ?)
(<15,0,A>, ?) (<15,0,B>, ?)
* Step 3: LeafRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. doSum(A,B) -> m9(A,B) [A >= 0] (1,1)
1. m0(A,B) -> m1(A,B) [A >= 0] (?,1)
2. m2(A,B) -> m3(A,B) [1 + A >= 0] (?,1)
3. m1(A,B) -> m5(A,B) [A >= 0] (?,1)
4. m6(A,B) -> m4(A,B) [A >= 0 && 0 >= A] (?,1)
5. m7(A,B) -> c2(m4(C,B),m0(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A] (?,1)
6. m5(A,B) -> m8(A,B) [A >= 0] (?,1)
7. m8(A,B) -> m7(A,B) True (?,1)
8. m8(A,B) -> m6(A,B) True (?,1)
9. n2(A,B) -> c2(n0(A,B),m2(A,B)) [A >= 0] (?,1)
10. m9(A,B) -> n2(A,B) [A >= 0] (?,1)
11. n30(A,B) -> m2(A,B) True (?,1)
12. n31(A,B) -> m0(B,B) True (?,1)
13. n3(A,B) -> c2(n30(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A] (?,1)
14. m3(A,B) -> n3(A,B) True (?,1)
15. m3(A,B) -> n1(A,B) True (?,1)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[0->{10},1->{3},2->{14,15},3->{6},4->{},5->{1},6->{7,8},7->{5},8->{4},9->{2},10->{9},11->{2},12->{1}
,13->{11,12},14->{13},15->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, 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>, ?)
(< 5,1,A>, ?) (< 5,1,B>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?)
(< 9,0,A>, A) (< 9,0,B>, B)
(< 9,1,A>, A) (< 9,1,B>, B)
(<10,0,A>, A) (<10,0,B>, B)
(<11,0,A>, ?) (<11,0,B>, ?)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<13,1,A>, ?) (<13,1,B>, ?)
(<14,0,A>, ?) (<14,0,B>, ?)
(<15,0,A>, ?) (<15,0,B>, ?)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [8,4,15]
* Step 4: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. doSum(A,B) -> m9(A,B) [A >= 0] (1,1)
1. m0(A,B) -> m1(A,B) [A >= 0] (?,1)
2. m2(A,B) -> m3(A,B) [1 + A >= 0] (?,1)
3. m1(A,B) -> m5(A,B) [A >= 0] (?,1)
5. m7(A,B) -> c2(m4(C,B),m0(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A] (?,1)
6. m5(A,B) -> m8(A,B) [A >= 0] (?,1)
7. m8(A,B) -> m7(A,B) True (?,1)
9. n2(A,B) -> c2(n0(A,B),m2(A,B)) [A >= 0] (?,1)
10. m9(A,B) -> n2(A,B) [A >= 0] (?,1)
11. n30(A,B) -> m2(A,B) True (?,1)
12. n31(A,B) -> m0(B,B) True (?,1)
13. n3(A,B) -> c2(n30(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A] (?,1)
14. m3(A,B) -> n3(A,B) True (?,1)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[0->{10},1->{3},2->{14},3->{6},5->{1},6->{7},7->{5},9->{2},10->{9},11->{2},12->{1},13->{11,12},14->{13}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B)
(< 1,0,A>, ?) (< 1,0,B>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?)
(< 5,1,A>, ?) (< 5,1,B>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 9,0,A>, A) (< 9,0,B>, B)
(< 9,1,A>, A) (< 9,1,B>, B)
(<10,0,A>, A) (<10,0,B>, B)
(<11,0,A>, ?) (<11,0,B>, ?)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<13,1,A>, ?) (<13,1,B>, ?)
(<14,0,A>, ?) (<14,0,B>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(doSum) = 2
p(m0) = 0
p(m1) = 0
p(m2) = 1
p(m3) = 1
p(m4) = 0
p(m5) = 0
p(m7) = 0
p(m8) = 0
p(m9) = 2
p(n0) = 0
p(n2) = 1
p(n3) = 1
p(n30) = 1
p(n31) = 0
The following rules are strictly oriented:
[A >= 0] ==>
m9(A,B) = 2
> 1
= n2(A,B)
The following rules are weakly oriented:
[A >= 0] ==>
doSum(A,B) = 2
>= 2
= m9(A,B)
[A >= 0] ==>
m0(A,B) = 0
>= 0
= m1(A,B)
[1 + A >= 0] ==>
m2(A,B) = 1
>= 1
= m3(A,B)
[A >= 0] ==>
m1(A,B) = 0
>= 0
= m5(A,B)
[A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A] ==>
m7(A,B) = 0
>= 0
= c2(m4(C,B),m0(C,B))
[A >= 0] ==>
m5(A,B) = 0
>= 0
= m8(A,B)
True ==>
m8(A,B) = 0
>= 0
= m7(A,B)
[A >= 0] ==>
n2(A,B) = 1
>= 1
= c2(n0(A,B),m2(A,B))
True ==>
n30(A,B) = 1
>= 1
= m2(A,B)
True ==>
n31(A,B) = 0
>= 0
= m0(B,B)
[A >= 0 && A >= 1 + C && 1 + C >= A] ==>
n3(A,B) = 1
>= 1
= c2(n30(C,A),n31(C,A))
True ==>
m3(A,B) = 1
>= 1
= n3(A,B)
* Step 5: KnowledgePropagation WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. doSum(A,B) -> m9(A,B) [A >= 0] (1,1)
1. m0(A,B) -> m1(A,B) [A >= 0] (?,1)
2. m2(A,B) -> m3(A,B) [1 + A >= 0] (?,1)
3. m1(A,B) -> m5(A,B) [A >= 0] (?,1)
5. m7(A,B) -> c2(m4(C,B),m0(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A] (?,1)
6. m5(A,B) -> m8(A,B) [A >= 0] (?,1)
7. m8(A,B) -> m7(A,B) True (?,1)
9. n2(A,B) -> c2(n0(A,B),m2(A,B)) [A >= 0] (?,1)
10. m9(A,B) -> n2(A,B) [A >= 0] (2,1)
11. n30(A,B) -> m2(A,B) True (?,1)
12. n31(A,B) -> m0(B,B) True (?,1)
13. n3(A,B) -> c2(n30(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A] (?,1)
14. m3(A,B) -> n3(A,B) True (?,1)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[0->{10},1->{3},2->{14},3->{6},5->{1},6->{7},7->{5},9->{2},10->{9},11->{2},12->{1},13->{11,12},14->{13}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B)
(< 1,0,A>, ?) (< 1,0,B>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?)
(< 5,1,A>, ?) (< 5,1,B>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 9,0,A>, A) (< 9,0,B>, B)
(< 9,1,A>, A) (< 9,1,B>, B)
(<10,0,A>, A) (<10,0,B>, B)
(<11,0,A>, ?) (<11,0,B>, ?)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<13,1,A>, ?) (<13,1,B>, ?)
(<14,0,A>, ?) (<14,0,B>, ?)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 6: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. doSum(A,B) -> m9(A,B) [A >= 0] (1,1)
1. m0(A,B) -> m1(A,B) [A >= 0] (?,1)
2. m2(A,B) -> m3(A,B) [1 + A >= 0] (?,1)
3. m1(A,B) -> m5(A,B) [A >= 0] (?,1)
5. m7(A,B) -> c2(m4(C,B),m0(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A] (?,1)
6. m5(A,B) -> m8(A,B) [A >= 0] (?,1)
7. m8(A,B) -> m7(A,B) True (?,1)
9. n2(A,B) -> c2(n0(A,B),m2(A,B)) [A >= 0] (2,1)
10. m9(A,B) -> n2(A,B) [A >= 0] (2,1)
11. n30(A,B) -> m2(A,B) True (?,1)
12. n31(A,B) -> m0(B,B) True (?,1)
13. n3(A,B) -> c2(n30(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A] (?,1)
14. m3(A,B) -> n3(A,B) True (?,1)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[0->{10},1->{3},2->{14},3->{6},5->{1},6->{7},7->{5},9->{2},10->{9},11->{2},12->{1},13->{11,12},14->{13}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B)
(< 1,0,A>, ?) (< 1,0,B>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?)
(< 5,1,A>, ?) (< 5,1,B>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 9,0,A>, A) (< 9,0,B>, B)
(< 9,1,A>, A) (< 9,1,B>, B)
(<10,0,A>, A) (<10,0,B>, B)
(<11,0,A>, ?) (<11,0,B>, ?)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<13,1,A>, ?) (<13,1,B>, ?)
(<14,0,A>, ?) (<14,0,B>, ?)
+ Applied Processor:
ChainProcessor False [0,1,2,3,5,6,7,9,10,11,12,13,14]
+ Details:
We chained rule 0 to obtain the rules [15] .
* Step 7: UnreachableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
1. m0(A,B) -> m1(A,B) [A >= 0] (?,1)
2. m2(A,B) -> m3(A,B) [1 + A >= 0] (?,1)
3. m1(A,B) -> m5(A,B) [A >= 0] (?,1)
5. m7(A,B) -> c2(m4(C,B),m0(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A] (?,1)
6. m5(A,B) -> m8(A,B) [A >= 0] (?,1)
7. m8(A,B) -> m7(A,B) True (?,1)
9. n2(A,B) -> c2(n0(A,B),m2(A,B)) [A >= 0] (2,1)
10. m9(A,B) -> n2(A,B) [A >= 0] (2,1)
11. n30(A,B) -> m2(A,B) True (?,1)
12. n31(A,B) -> m0(B,B) True (?,1)
13. n3(A,B) -> c2(n30(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A] (?,1)
14. m3(A,B) -> n3(A,B) True (?,1)
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[1->{3},2->{14},3->{6},5->{1},6->{7},7->{5},9->{2},10->{9},11->{2},12->{1},13->{11,12},14->{13},15->{9}]
Sizebounds:
(< 1,0,A>, ?) (< 1,0,B>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?)
(< 5,1,A>, ?) (< 5,1,B>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 9,0,A>, A) (< 9,0,B>, B)
(< 9,1,A>, A) (< 9,1,B>, B)
(<10,0,A>, A) (<10,0,B>, B)
(<11,0,A>, ?) (<11,0,B>, ?)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<13,1,A>, ?) (<13,1,B>, ?)
(<14,0,A>, ?) (<14,0,B>, ?)
(<15,0,A>, A) (<15,0,B>, B)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [10]
* Step 8: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
1. m0(A,B) -> m1(A,B) [A >= 0] (?,1)
2. m2(A,B) -> m3(A,B) [1 + A >= 0] (?,1)
3. m1(A,B) -> m5(A,B) [A >= 0] (?,1)
5. m7(A,B) -> c2(m4(C,B),m0(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A] (?,1)
6. m5(A,B) -> m8(A,B) [A >= 0] (?,1)
7. m8(A,B) -> m7(A,B) True (?,1)
9. n2(A,B) -> c2(n0(A,B),m2(A,B)) [A >= 0] (2,1)
11. n30(A,B) -> m2(A,B) True (?,1)
12. n31(A,B) -> m0(B,B) True (?,1)
13. n3(A,B) -> c2(n30(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A] (?,1)
14. m3(A,B) -> n3(A,B) True (?,1)
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[1->{3},2->{14},3->{6},5->{1},6->{7},7->{5},9->{2},11->{2},12->{1},13->{11,12},14->{13},15->{9}]
Sizebounds:
(< 1,0,A>, ?) (< 1,0,B>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?)
(< 5,1,A>, ?) (< 5,1,B>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 9,0,A>, A) (< 9,0,B>, B)
(< 9,1,A>, A) (< 9,1,B>, B)
(<11,0,A>, ?) (<11,0,B>, ?)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<13,1,A>, ?) (<13,1,B>, ?)
(<14,0,A>, ?) (<14,0,B>, ?)
(<15,0,A>, A) (<15,0,B>, B)
+ Applied Processor:
ChainProcessor False [1,2,3,5,6,7,9,11,12,13,14,15]
+ Details:
We chained rule 1 to obtain the rules [16] .
* Step 9: UnreachableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
2. m2(A,B) -> m3(A,B) [1 + A >= 0] (?,1)
3. m1(A,B) -> m5(A,B) [A >= 0] (?,1)
5. m7(A,B) -> c2(m4(C,B),m0(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A] (?,1)
6. m5(A,B) -> m8(A,B) [A >= 0] (?,1)
7. m8(A,B) -> m7(A,B) True (?,1)
9. n2(A,B) -> c2(n0(A,B),m2(A,B)) [A >= 0] (2,1)
11. n30(A,B) -> m2(A,B) True (?,1)
12. n31(A,B) -> m0(B,B) True (?,1)
13. n3(A,B) -> c2(n30(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A] (?,1)
14. m3(A,B) -> n3(A,B) True (?,1)
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
16. m0(A,B) -> m5(A,B) [A >= 0 && A >= 0] (?,2)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[2->{14},3->{6},5->{16},6->{7},7->{5},9->{2},11->{2},12->{16},13->{11,12},14->{13},15->{9},16->{6}]
Sizebounds:
(< 2,0,A>, ?) (< 2,0,B>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?)
(< 5,1,A>, ?) (< 5,1,B>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 9,0,A>, A) (< 9,0,B>, B)
(< 9,1,A>, A) (< 9,1,B>, B)
(<11,0,A>, ?) (<11,0,B>, ?)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<13,1,A>, ?) (<13,1,B>, ?)
(<14,0,A>, ?) (<14,0,B>, ?)
(<15,0,A>, A) (<15,0,B>, B)
(<16,0,A>, ?) (<16,0,B>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [3]
* Step 10: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
2. m2(A,B) -> m3(A,B) [1 + A >= 0] (?,1)
5. m7(A,B) -> c2(m4(C,B),m0(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A] (?,1)
6. m5(A,B) -> m8(A,B) [A >= 0] (?,1)
7. m8(A,B) -> m7(A,B) True (?,1)
9. n2(A,B) -> c2(n0(A,B),m2(A,B)) [A >= 0] (2,1)
11. n30(A,B) -> m2(A,B) True (?,1)
12. n31(A,B) -> m0(B,B) True (?,1)
13. n3(A,B) -> c2(n30(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A] (?,1)
14. m3(A,B) -> n3(A,B) True (?,1)
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
16. m0(A,B) -> m5(A,B) [A >= 0 && A >= 0] (?,2)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[2->{14},5->{16},6->{7},7->{5},9->{2},11->{2},12->{16},13->{11,12},14->{13},15->{9},16->{6}]
Sizebounds:
(< 2,0,A>, ?) (< 2,0,B>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?)
(< 5,1,A>, ?) (< 5,1,B>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 9,0,A>, A) (< 9,0,B>, B)
(< 9,1,A>, A) (< 9,1,B>, B)
(<11,0,A>, ?) (<11,0,B>, ?)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<13,1,A>, ?) (<13,1,B>, ?)
(<14,0,A>, ?) (<14,0,B>, ?)
(<15,0,A>, A) (<15,0,B>, B)
(<16,0,A>, ?) (<16,0,B>, ?)
+ Applied Processor:
ChainProcessor False [2,5,6,7,9,11,12,13,14,15,16]
+ Details:
We chained rule 2 to obtain the rules [17] .
* Step 11: UnreachableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
5. m7(A,B) -> c2(m4(C,B),m0(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A] (?,1)
6. m5(A,B) -> m8(A,B) [A >= 0] (?,1)
7. m8(A,B) -> m7(A,B) True (?,1)
9. n2(A,B) -> c2(n0(A,B),m2(A,B)) [A >= 0] (2,1)
11. n30(A,B) -> m2(A,B) True (?,1)
12. n31(A,B) -> m0(B,B) True (?,1)
13. n3(A,B) -> c2(n30(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A] (?,1)
14. m3(A,B) -> n3(A,B) True (?,1)
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
16. m0(A,B) -> m5(A,B) [A >= 0 && A >= 0] (?,2)
17. m2(A,B) -> n3(A,B) [1 + A >= 0] (?,2)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[5->{16},6->{7},7->{5},9->{17},11->{17},12->{16},13->{11,12},14->{13},15->{9},16->{6},17->{13}]
Sizebounds:
(< 5,0,A>, ?) (< 5,0,B>, ?)
(< 5,1,A>, ?) (< 5,1,B>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 9,0,A>, A) (< 9,0,B>, B)
(< 9,1,A>, A) (< 9,1,B>, B)
(<11,0,A>, ?) (<11,0,B>, ?)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<13,1,A>, ?) (<13,1,B>, ?)
(<14,0,A>, ?) (<14,0,B>, ?)
(<15,0,A>, A) (<15,0,B>, B)
(<16,0,A>, ?) (<16,0,B>, ?)
(<17,0,A>, ?) (<17,0,B>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [14]
* Step 12: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
5. m7(A,B) -> c2(m4(C,B),m0(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A] (?,1)
6. m5(A,B) -> m8(A,B) [A >= 0] (?,1)
7. m8(A,B) -> m7(A,B) True (?,1)
9. n2(A,B) -> c2(n0(A,B),m2(A,B)) [A >= 0] (2,1)
11. n30(A,B) -> m2(A,B) True (?,1)
12. n31(A,B) -> m0(B,B) True (?,1)
13. n3(A,B) -> c2(n30(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A] (?,1)
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
16. m0(A,B) -> m5(A,B) [A >= 0 && A >= 0] (?,2)
17. m2(A,B) -> n3(A,B) [1 + A >= 0] (?,2)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[5->{16},6->{7},7->{5},9->{17},11->{17},12->{16},13->{11,12},15->{9},16->{6},17->{13}]
Sizebounds:
(< 5,0,A>, ?) (< 5,0,B>, ?)
(< 5,1,A>, ?) (< 5,1,B>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 9,0,A>, A) (< 9,0,B>, B)
(< 9,1,A>, A) (< 9,1,B>, B)
(<11,0,A>, ?) (<11,0,B>, ?)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<13,1,A>, ?) (<13,1,B>, ?)
(<15,0,A>, A) (<15,0,B>, B)
(<16,0,A>, ?) (<16,0,B>, ?)
(<17,0,A>, ?) (<17,0,B>, ?)
+ Applied Processor:
ChainProcessor False [5,6,7,9,11,12,13,15,16,17]
+ Details:
We chained rule 5 to obtain the rules [18] .
* Step 13: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
6. m5(A,B) -> m8(A,B) [A >= 0] (?,1)
7. m8(A,B) -> m7(A,B) True (?,1)
9. n2(A,B) -> c2(n0(A,B),m2(A,B)) [A >= 0] (2,1)
11. n30(A,B) -> m2(A,B) True (?,1)
12. n31(A,B) -> m0(B,B) True (?,1)
13. n3(A,B) -> c2(n30(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A] (?,1)
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
16. m0(A,B) -> m5(A,B) [A >= 0 && A >= 0] (?,2)
17. m2(A,B) -> n3(A,B) [1 + A >= 0] (?,2)
18. m7(A,B) -> c2(m4(C,B),m5(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0] (?,3)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[6->{7},7->{18},9->{17},11->{17},12->{16},13->{11,12},15->{9},16->{6},17->{13},18->{6}]
Sizebounds:
(< 6,0,A>, ?) (< 6,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 9,0,A>, A) (< 9,0,B>, B)
(< 9,1,A>, A) (< 9,1,B>, B)
(<11,0,A>, ?) (<11,0,B>, ?)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<13,1,A>, ?) (<13,1,B>, ?)
(<15,0,A>, A) (<15,0,B>, B)
(<16,0,A>, ?) (<16,0,B>, ?)
(<17,0,A>, ?) (<17,0,B>, ?)
(<18,0,A>, ?) (<18,0,B>, ?)
+ Applied Processor:
ChainProcessor False [6,7,9,11,12,13,15,16,17,18]
+ Details:
We chained rule 6 to obtain the rules [19] .
* Step 14: UnreachableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
7. m8(A,B) -> m7(A,B) True (?,1)
9. n2(A,B) -> c2(n0(A,B),m2(A,B)) [A >= 0] (2,1)
11. n30(A,B) -> m2(A,B) True (?,1)
12. n31(A,B) -> m0(B,B) True (?,1)
13. n3(A,B) -> c2(n30(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A] (?,1)
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
16. m0(A,B) -> m5(A,B) [A >= 0 && A >= 0] (?,2)
17. m2(A,B) -> n3(A,B) [1 + A >= 0] (?,2)
18. m7(A,B) -> c2(m4(C,B),m5(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0] (?,3)
19. m5(A,B) -> m7(A,B) [A >= 0] (?,2)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[7->{18},9->{17},11->{17},12->{16},13->{11,12},15->{9},16->{19},17->{13},18->{19},19->{18}]
Sizebounds:
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 9,0,A>, A) (< 9,0,B>, B)
(< 9,1,A>, A) (< 9,1,B>, B)
(<11,0,A>, ?) (<11,0,B>, ?)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<13,1,A>, ?) (<13,1,B>, ?)
(<15,0,A>, A) (<15,0,B>, B)
(<16,0,A>, ?) (<16,0,B>, ?)
(<17,0,A>, ?) (<17,0,B>, ?)
(<18,0,A>, ?) (<18,0,B>, ?)
(<19,0,A>, ?) (<19,0,B>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [7]
* Step 15: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
9. n2(A,B) -> c2(n0(A,B),m2(A,B)) [A >= 0] (2,1)
11. n30(A,B) -> m2(A,B) True (?,1)
12. n31(A,B) -> m0(B,B) True (?,1)
13. n3(A,B) -> c2(n30(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A] (?,1)
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
16. m0(A,B) -> m5(A,B) [A >= 0 && A >= 0] (?,2)
17. m2(A,B) -> n3(A,B) [1 + A >= 0] (?,2)
18. m7(A,B) -> c2(m4(C,B),m5(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0] (?,3)
19. m5(A,B) -> m7(A,B) [A >= 0] (?,2)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[9->{17},11->{17},12->{16},13->{11,12},15->{9},16->{19},17->{13},18->{19},19->{18}]
Sizebounds:
(< 9,0,A>, A) (< 9,0,B>, B)
(< 9,1,A>, A) (< 9,1,B>, B)
(<11,0,A>, ?) (<11,0,B>, ?)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<13,1,A>, ?) (<13,1,B>, ?)
(<15,0,A>, A) (<15,0,B>, B)
(<16,0,A>, ?) (<16,0,B>, ?)
(<17,0,A>, ?) (<17,0,B>, ?)
(<18,0,A>, ?) (<18,0,B>, ?)
(<19,0,A>, ?) (<19,0,B>, ?)
+ Applied Processor:
ChainProcessor False [9,11,12,13,15,16,17,18,19]
+ Details:
We chained rule 9 to obtain the rules [20] .
* Step 16: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
11. n30(A,B) -> m2(A,B) True (?,1)
12. n31(A,B) -> m0(B,B) True (?,1)
13. n3(A,B) -> c2(n30(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A] (?,1)
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
16. m0(A,B) -> m5(A,B) [A >= 0 && A >= 0] (?,2)
17. m2(A,B) -> n3(A,B) [1 + A >= 0] (?,2)
18. m7(A,B) -> c2(m4(C,B),m5(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0] (?,3)
19. m5(A,B) -> m7(A,B) [A >= 0] (?,2)
20. n2(A,B) -> c2(n0(A,B),n3(A,B)) [A >= 0 && 1 + A >= 0] (2,3)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[11->{17},12->{16},13->{11,12},15->{20},16->{19},17->{13},18->{19},19->{18},20->{13}]
Sizebounds:
(<11,0,A>, ?) (<11,0,B>, ?)
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<13,1,A>, ?) (<13,1,B>, ?)
(<15,0,A>, A) (<15,0,B>, B)
(<16,0,A>, ?) (<16,0,B>, ?)
(<17,0,A>, ?) (<17,0,B>, ?)
(<18,0,A>, ?) (<18,0,B>, ?)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, ?) (<20,0,B>, ?)
+ Applied Processor:
ChainProcessor False [11,12,13,15,16,17,18,19,20]
+ Details:
We chained rule 11 to obtain the rules [21] .
* Step 17: UnreachableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
12. n31(A,B) -> m0(B,B) True (?,1)
13. n3(A,B) -> c2(n30(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A] (?,1)
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
16. m0(A,B) -> m5(A,B) [A >= 0 && A >= 0] (?,2)
17. m2(A,B) -> n3(A,B) [1 + A >= 0] (?,2)
18. m7(A,B) -> c2(m4(C,B),m5(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0] (?,3)
19. m5(A,B) -> m7(A,B) [A >= 0] (?,2)
20. n2(A,B) -> c2(n0(A,B),n3(A,B)) [A >= 0 && 1 + A >= 0] (2,3)
21. n30(A,B) -> n3(A,B) [1 + A >= 0] (?,3)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[12->{16},13->{12,21},15->{20},16->{19},17->{13},18->{19},19->{18},20->{13},21->{13}]
Sizebounds:
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<13,1,A>, ?) (<13,1,B>, ?)
(<15,0,A>, A) (<15,0,B>, B)
(<16,0,A>, ?) (<16,0,B>, ?)
(<17,0,A>, ?) (<17,0,B>, ?)
(<18,0,A>, ?) (<18,0,B>, ?)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, ?) (<20,0,B>, ?)
(<21,0,A>, ?) (<21,0,B>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [17]
* Step 18: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
12. n31(A,B) -> m0(B,B) True (?,1)
13. n3(A,B) -> c2(n30(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A] (?,1)
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
16. m0(A,B) -> m5(A,B) [A >= 0 && A >= 0] (?,2)
18. m7(A,B) -> c2(m4(C,B),m5(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0] (?,3)
19. m5(A,B) -> m7(A,B) [A >= 0] (?,2)
20. n2(A,B) -> c2(n0(A,B),n3(A,B)) [A >= 0 && 1 + A >= 0] (2,3)
21. n30(A,B) -> n3(A,B) [1 + A >= 0] (?,3)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[12->{16},13->{12,21},15->{20},16->{19},18->{19},19->{18},20->{13},21->{13}]
Sizebounds:
(<12,0,A>, ?) (<12,0,B>, ?)
(<13,0,A>, ?) (<13,0,B>, ?)
(<13,1,A>, ?) (<13,1,B>, ?)
(<15,0,A>, A) (<15,0,B>, B)
(<16,0,A>, ?) (<16,0,B>, ?)
(<18,0,A>, ?) (<18,0,B>, ?)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, ?) (<20,0,B>, ?)
(<21,0,A>, ?) (<21,0,B>, ?)
+ Applied Processor:
ChainProcessor False [12,13,15,16,18,19,20,21]
+ Details:
We chained rule 12 to obtain the rules [22] .
* Step 19: UnreachableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. n3(A,B) -> c2(n30(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A] (?,1)
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
16. m0(A,B) -> m5(A,B) [A >= 0 && A >= 0] (?,2)
18. m7(A,B) -> c2(m4(C,B),m5(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0] (?,3)
19. m5(A,B) -> m7(A,B) [A >= 0] (?,2)
20. n2(A,B) -> c2(n0(A,B),n3(A,B)) [A >= 0 && 1 + A >= 0] (2,3)
21. n30(A,B) -> n3(A,B) [1 + A >= 0] (?,3)
22. n31(A,B) -> m5(B,B) [B >= 0 && B >= 0] (?,3)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[13->{21,22},15->{20},16->{19},18->{19},19->{18},20->{13},21->{13},22->{19}]
Sizebounds:
(<13,0,A>, ?) (<13,0,B>, ?)
(<13,1,A>, ?) (<13,1,B>, ?)
(<15,0,A>, A) (<15,0,B>, B)
(<16,0,A>, ?) (<16,0,B>, ?)
(<18,0,A>, ?) (<18,0,B>, ?)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, ?) (<20,0,B>, ?)
(<21,0,A>, ?) (<21,0,B>, ?)
(<22,0,A>, ?) (<22,0,B>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [16]
* Step 20: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
13. n3(A,B) -> c2(n30(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A] (?,1)
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
18. m7(A,B) -> c2(m4(C,B),m5(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0] (?,3)
19. m5(A,B) -> m7(A,B) [A >= 0] (?,2)
20. n2(A,B) -> c2(n0(A,B),n3(A,B)) [A >= 0 && 1 + A >= 0] (2,3)
21. n30(A,B) -> n3(A,B) [1 + A >= 0] (?,3)
22. n31(A,B) -> m5(B,B) [B >= 0 && B >= 0] (?,3)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[13->{21,22},15->{20},18->{19},19->{18},20->{13},21->{13},22->{19}]
Sizebounds:
(<13,0,A>, ?) (<13,0,B>, ?)
(<13,1,A>, ?) (<13,1,B>, ?)
(<15,0,A>, A) (<15,0,B>, B)
(<18,0,A>, ?) (<18,0,B>, ?)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, ?) (<20,0,B>, ?)
(<21,0,A>, ?) (<21,0,B>, ?)
(<22,0,A>, ?) (<22,0,B>, ?)
+ Applied Processor:
ChainProcessor False [13,15,18,19,20,21,22]
+ Details:
We chained rule 13 to obtain the rules [23] .
* Step 21: UnreachableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
18. m7(A,B) -> c2(m4(C,B),m5(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0] (?,3)
19. m5(A,B) -> m7(A,B) [A >= 0] (?,2)
20. n2(A,B) -> c2(n0(A,B),n3(A,B)) [A >= 0 && 1 + A >= 0] (2,3)
21. n30(A,B) -> n3(A,B) [1 + A >= 0] (?,3)
22. n31(A,B) -> m5(B,B) [B >= 0 && B >= 0] (?,3)
23. n3(A,B) -> c2(n3(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A && 1 + C >= 0] (?,4)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[15->{20},18->{19},19->{18},20->{23},21->{23},22->{19},23->{22,23}]
Sizebounds:
(<15,0,A>, A) (<15,0,B>, B)
(<18,0,A>, ?) (<18,0,B>, ?)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, ?) (<20,0,B>, ?)
(<21,0,A>, ?) (<21,0,B>, ?)
(<22,0,A>, ?) (<22,0,B>, ?)
(<23,0,A>, ?) (<23,0,B>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [21]
* Step 22: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
18. m7(A,B) -> c2(m4(C,B),m5(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0] (?,3)
19. m5(A,B) -> m7(A,B) [A >= 0] (?,2)
20. n2(A,B) -> c2(n0(A,B),n3(A,B)) [A >= 0 && 1 + A >= 0] (2,3)
22. n31(A,B) -> m5(B,B) [B >= 0 && B >= 0] (?,3)
23. n3(A,B) -> c2(n3(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A && 1 + C >= 0] (?,4)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[15->{20},18->{19},19->{18},20->{23},22->{19},23->{22,23}]
Sizebounds:
(<15,0,A>, A) (<15,0,B>, B)
(<18,0,A>, ?) (<18,0,B>, ?)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, ?) (<20,0,B>, ?)
(<22,0,A>, ?) (<22,0,B>, ?)
(<23,0,A>, ?) (<23,0,B>, ?)
+ Applied Processor:
ChainProcessor False [15,18,19,20,22,23]
+ Details:
We chained rule 18 to obtain the rules [24] .
* Step 23: LocalSizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
19. m5(A,B) -> m7(A,B) [A >= 0] (?,2)
20. n2(A,B) -> c2(n0(A,B),n3(A,B)) [A >= 0 && 1 + A >= 0] (2,3)
22. n31(A,B) -> m5(B,B) [B >= 0 && B >= 0] (?,3)
23. n3(A,B) -> c2(n3(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A && 1 + C >= 0] (?,4)
24. m7(A,B) -> c2(m4(C,B),m7(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0 && C >= 0] (?,5)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[15->{20},19->{24},20->{23},22->{19},23->{22,23},24->{24}]
Sizebounds:
(<15,0,A>, A) (<15,0,B>, B)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, ?) (<20,0,B>, ?)
(<22,0,A>, ?) (<22,0,B>, ?)
(<23,0,A>, ?) (<23,0,B>, ?)
(<24,0,A>, ?) (<24,0,B>, ?)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<15,0,A>, A, .= 0) (<15,0,B>, B, .= 0)
(<19,0,A>, A, .= 0) (<19,0,B>, B, .= 0)
(<20,0,A>, A, .= 0) (<20,0,B>, B, .= 0)
(<20,1,A>, A, .= 0) (<20,1,B>, B, .= 0)
(<22,0,A>, B, .= 0) (<22,0,B>, B, .= 0)
(<23,0,A>, 1 + A, .+ 1) (<23,0,B>, A, .= 0)
(<23,1,A>, 1 + A, .+ 1) (<23,1,B>, A, .= 0)
(<24,0,A>, 1 + A, .+ 1) (<24,0,B>, B, .= 0)
(<24,1,A>, 1 + A, .+ 1) (<24,1,B>, B, .= 0)
* Step 24: SizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
19. m5(A,B) -> m7(A,B) [A >= 0] (?,2)
20. n2(A,B) -> c2(n0(A,B),n3(A,B)) [A >= 0 && 1 + A >= 0] (2,3)
22. n31(A,B) -> m5(B,B) [B >= 0 && B >= 0] (?,3)
23. n3(A,B) -> c2(n3(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A && 1 + C >= 0] (?,4)
24. m7(A,B) -> c2(m4(C,B),m7(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0 && C >= 0] (?,5)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[15->{20},19->{24},20->{23},22->{19},23->{22,23},24->{24}]
Sizebounds:
(<15,0,A>, ?) (<15,0,B>, ?)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, ?) (<20,0,B>, ?)
(<20,1,A>, ?) (<20,1,B>, ?)
(<22,0,A>, ?) (<22,0,B>, ?)
(<23,0,A>, ?) (<23,0,B>, ?)
(<23,1,A>, ?) (<23,1,B>, ?)
(<24,0,A>, ?) (<24,0,B>, ?)
(<24,1,A>, ?) (<24,1,B>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<15,0,A>, A) (<15,0,B>, B)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, A) (<20,0,B>, B)
(<20,1,A>, A) (<20,1,B>, B)
(<22,0,A>, ?) (<22,0,B>, ?)
(<23,0,A>, ?) (<23,0,B>, ?)
(<23,1,A>, ?) (<23,1,B>, ?)
(<24,0,A>, ?) (<24,0,B>, ?)
(<24,1,A>, ?) (<24,1,B>, ?)
* Step 25: LocationConstraintsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
19. m5(A,B) -> m7(A,B) [A >= 0] (?,2)
20. n2(A,B) -> c2(n0(A,B),n3(A,B)) [A >= 0 && 1 + A >= 0] (2,3)
22. n31(A,B) -> m5(B,B) [B >= 0 && B >= 0] (?,3)
23. n3(A,B) -> c2(n3(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A && 1 + C >= 0] (?,4)
24. m7(A,B) -> c2(m4(C,B),m7(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0 && C >= 0] (?,5)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[15->{20},19->{24},20->{23},22->{19},23->{22,23},24->{24}]
Sizebounds:
(<15,0,A>, A) (<15,0,B>, B)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, A) (<20,0,B>, B)
(<20,1,A>, A) (<20,1,B>, B)
(<22,0,A>, ?) (<22,0,B>, ?)
(<23,0,A>, ?) (<23,0,B>, ?)
(<23,1,A>, ?) (<23,1,B>, ?)
(<24,0,A>, ?) (<24,0,B>, ?)
(<24,1,A>, ?) (<24,1,B>, ?)
+ Applied Processor:
LocationConstraintsProc
+ Details:
We computed the location constraints 15 : True 19 : [B >= 0] 20 : [A >= 0] 22 : True 23 : True 24 : [A >= 0] .
* Step 26: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
19. m5(A,B) -> m7(A,B) [A >= 0] (?,2)
20. n2(A,B) -> c2(n0(A,B),n3(A,B)) [A >= 0 && 1 + A >= 0] (2,3)
22. n31(A,B) -> m5(B,B) [B >= 0 && B >= 0] (?,3)
23. n3(A,B) -> c2(n3(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A && 1 + C >= 0] (?,4)
24. m7(A,B) -> c2(m4(C,B),m7(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0 && C >= 0] (?,5)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[15->{20},19->{24},20->{23},22->{19},23->{22,23},24->{24}]
Sizebounds:
(<15,0,A>, A) (<15,0,B>, B)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, A) (<20,0,B>, B)
(<20,1,A>, A) (<20,1,B>, B)
(<22,0,A>, ?) (<22,0,B>, ?)
(<23,0,A>, ?) (<23,0,B>, ?)
(<23,1,A>, ?) (<23,1,B>, ?)
(<24,0,A>, ?) (<24,0,B>, ?)
(<24,1,A>, ?) (<24,1,B>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(doSum) = 1 + x1
p(m4) = 0
p(m5) = 0
p(m7) = 0
p(n0) = 0
p(n2) = 1 + x1
p(n3) = 1 + x1
p(n31) = 0
The following rules are strictly oriented:
[A >= 0 && A >= 1 + C && 1 + C >= A && 1 + C >= 0] ==>
n3(A,B) = 1 + A
> 1 + C
= c2(n3(C,A),n31(C,A))
The following rules are weakly oriented:
[A >= 0 && A >= 0] ==>
doSum(A,B) = 1 + A
>= 1 + A
= n2(A,B)
[A >= 0] ==>
m5(A,B) = 0
>= 0
= m7(A,B)
[A >= 0 && 1 + A >= 0] ==>
n2(A,B) = 1 + A
>= 1 + A
= c2(n0(A,B),n3(A,B))
[B >= 0 && B >= 0] ==>
n31(A,B) = 0
>= 0
= m5(B,B)
[A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0 && C >= 0] ==>
m7(A,B) = 0
>= 0
= c2(m4(C,B),m7(C,B))
* Step 27: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
19. m5(A,B) -> m7(A,B) [A >= 0] (?,2)
20. n2(A,B) -> c2(n0(A,B),n3(A,B)) [A >= 0 && 1 + A >= 0] (2,3)
22. n31(A,B) -> m5(B,B) [B >= 0 && B >= 0] (?,3)
23. n3(A,B) -> c2(n3(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A && 1 + C >= 0] (1 + A,4)
24. m7(A,B) -> c2(m4(C,B),m7(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0 && C >= 0] (?,5)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[15->{20},19->{24},20->{23},22->{19},23->{22,23},24->{24}]
Sizebounds:
(<15,0,A>, A) (<15,0,B>, B)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, A) (<20,0,B>, B)
(<20,1,A>, A) (<20,1,B>, B)
(<22,0,A>, ?) (<22,0,B>, ?)
(<23,0,A>, ?) (<23,0,B>, ?)
(<23,1,A>, ?) (<23,1,B>, ?)
(<24,0,A>, ?) (<24,0,B>, ?)
(<24,1,A>, ?) (<24,1,B>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(doSum) = 1 + x1
p(m4) = 0
p(m5) = 0
p(m7) = 0
p(n0) = 0
p(n2) = 1 + x1
p(n3) = 1 + x1
p(n31) = 1
The following rules are strictly oriented:
[B >= 0 && B >= 0] ==>
n31(A,B) = 1
> 0
= m5(B,B)
The following rules are weakly oriented:
[A >= 0 && A >= 0] ==>
doSum(A,B) = 1 + A
>= 1 + A
= n2(A,B)
[A >= 0] ==>
m5(A,B) = 0
>= 0
= m7(A,B)
[A >= 0 && 1 + A >= 0] ==>
n2(A,B) = 1 + A
>= 1 + A
= c2(n0(A,B),n3(A,B))
[A >= 0 && A >= 1 + C && 1 + C >= A && 1 + C >= 0] ==>
n3(A,B) = 1 + A
>= 2 + C
= c2(n3(C,A),n31(C,A))
[A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0 && C >= 0] ==>
m7(A,B) = 0
>= 0
= c2(m4(C,B),m7(C,B))
* Step 28: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
19. m5(A,B) -> m7(A,B) [A >= 0] (?,2)
20. n2(A,B) -> c2(n0(A,B),n3(A,B)) [A >= 0 && 1 + A >= 0] (2,3)
22. n31(A,B) -> m5(B,B) [B >= 0 && B >= 0] (1 + A,3)
23. n3(A,B) -> c2(n3(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A && 1 + C >= 0] (1 + A,4)
24. m7(A,B) -> c2(m4(C,B),m7(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0 && C >= 0] (?,5)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[15->{20},19->{24},20->{23},22->{19},23->{22,23},24->{24}]
Sizebounds:
(<15,0,A>, A) (<15,0,B>, B)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, A) (<20,0,B>, B)
(<20,1,A>, A) (<20,1,B>, B)
(<22,0,A>, ?) (<22,0,B>, ?)
(<23,0,A>, ?) (<23,0,B>, ?)
(<23,1,A>, ?) (<23,1,B>, ?)
(<24,0,A>, ?) (<24,0,B>, ?)
(<24,1,A>, ?) (<24,1,B>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(doSum) = 1 + x1
p(m4) = 0
p(m5) = 1
p(m7) = 0
p(n0) = 0
p(n2) = 1 + x1
p(n3) = 1 + x1
p(n31) = 1
The following rules are strictly oriented:
[A >= 0] ==>
m5(A,B) = 1
> 0
= m7(A,B)
The following rules are weakly oriented:
[A >= 0 && A >= 0] ==>
doSum(A,B) = 1 + A
>= 1 + A
= n2(A,B)
[A >= 0 && 1 + A >= 0] ==>
n2(A,B) = 1 + A
>= 1 + A
= c2(n0(A,B),n3(A,B))
[B >= 0 && B >= 0] ==>
n31(A,B) = 1
>= 1
= m5(B,B)
[A >= 0 && A >= 1 + C && 1 + C >= A && 1 + C >= 0] ==>
n3(A,B) = 1 + A
>= 2 + C
= c2(n3(C,A),n31(C,A))
[A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0 && C >= 0] ==>
m7(A,B) = 0
>= 0
= c2(m4(C,B),m7(C,B))
* Step 29: LoopRecurrenceProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
19. m5(A,B) -> m7(A,B) [A >= 0] (1 + A,2)
20. n2(A,B) -> c2(n0(A,B),n3(A,B)) [A >= 0 && 1 + A >= 0] (2,3)
22. n31(A,B) -> m5(B,B) [B >= 0 && B >= 0] (1 + A,3)
23. n3(A,B) -> c2(n3(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A && 1 + C >= 0] (1 + A,4)
24. m7(A,B) -> c2(m4(C,B),m7(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0 && C >= 0] (?,5)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[15->{20},19->{24},20->{23},22->{19},23->{22,23},24->{24}]
Sizebounds:
(<15,0,A>, A) (<15,0,B>, B)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, A) (<20,0,B>, B)
(<20,1,A>, A) (<20,1,B>, B)
(<22,0,A>, ?) (<22,0,B>, ?)
(<23,0,A>, ?) (<23,0,B>, ?)
(<23,1,A>, ?) (<23,1,B>, ?)
(<24,0,A>, ?) (<24,0,B>, ?)
(<24,1,A>, ?) (<24,1,B>, ?)
+ Applied Processor:
LoopRecurrenceProcessor [23]
+ Details:
Applying the recurrence pattern linear * f to the expression A yields the solution 3*A + A^2 .
* Step 30: LoopRecurrenceProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
19. m5(A,B) -> m7(A,B) [A >= 0] (1 + A,2)
20. n2(A,B) -> c2(n0(A,B),n3(A,B)) [A >= 0 && 1 + A >= 0] (2,3)
22. n31(A,B) -> m5(B,B) [B >= 0 && B >= 0] (1 + A,3)
23. n3(A,B) -> c2(n3(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A && 1 + C >= 0] (1 + A,4)
24. m7(A,B) -> c2(m4(C,B),m7(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0 && C >= 0] (6*A + 2*A^2,5)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[15->{20},19->{24},20->{23},22->{19},23->{22,23},24->{24}]
Sizebounds:
(<15,0,A>, A) (<15,0,B>, B)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, A) (<20,0,B>, B)
(<20,1,A>, A) (<20,1,B>, B)
(<22,0,A>, ?) (<22,0,B>, ?)
(<23,0,A>, ?) (<23,0,B>, ?)
(<23,1,A>, ?) (<23,1,B>, ?)
(<24,0,A>, ?) (<24,0,B>, ?)
(<24,1,A>, ?) (<24,1,B>, ?)
+ Applied Processor:
LoopRecurrenceProcessor [24]
+ Details:
Applying the recurrence pattern linear * f to the expression A yields the solution A .
* Step 31: UnsatPaths WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
15. doSum(A,B) -> n2(A,B) [A >= 0 && A >= 0] (1,2)
19. m5(A,B) -> m7(A,B) [A >= 0] (1 + A,2)
20. n2(A,B) -> c2(n0(A,B),n3(A,B)) [A >= 0 && 1 + A >= 0] (2,3)
22. n31(A,B) -> m5(B,B) [B >= 0 && B >= 0] (1 + A,3)
23. n3(A,B) -> c2(n3(C,A),n31(C,A)) [A >= 0 && A >= 1 + C && 1 + C >= A && 1 + C >= 0] (1 + A,4)
24. m7(A,B) -> c2(m4(C,B),m7(C,B)) [A >= 0 && A >= 1 && A >= 1 + C && 1 + C >= A && C >= 0 && C >= 0 && C >= 0] (6*A + 2*A^2,5)
Signature:
{(doSum,2)
;(m0,2)
;(m1,2)
;(m2,2)
;(m3,2)
;(m4,2)
;(m5,2)
;(m6,2)
;(m7,2)
;(m8,2)
;(m9,2)
;(n0,2)
;(n1,2)
;(n2,2)
;(n3,2)
;(n30,2)
;(n31,2)}
Flow Graph:
[15->{20},19->{24},20->{23},22->{19},23->{22,23},24->{24}]
Sizebounds:
(<15,0,A>, A) (<15,0,B>, B)
(<19,0,A>, ?) (<19,0,B>, ?)
(<20,0,A>, A) (<20,0,B>, B)
(<20,1,A>, A) (<20,1,B>, B)
(<22,0,A>, ?) (<22,0,B>, ?)
(<23,0,A>, ?) (<23,0,B>, ?)
(<23,1,A>, ?) (<23,1,B>, ?)
(<24,0,A>, ?) (<24,0,B>, ?)
(<24,1,A>, ?) (<24,1,B>, ?)
+ Applied Processor:
UnsatPaths
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^2))