At:
adjl-vertex-accum-properties
2
1.
A: AdjList
2.
T: Type
3.
s: T
4.
f: T
A.sizeT
5.
y: A.size
(y 
upto(0;A.size))
By:
AssertBY (y upto(0;A.size))
(RWO
Thm* 
i,j,k:. (k upto(i;j)) 
i
k & k < j
0)
THEN
RepeatFor 2 (ParallelOp -1)
THEN
ExRepD
Generated subgoals:
None
About:
