At:
adjm-vertex-accum-properties
2
1.
M: AdjMatrix
2.
T: Type
3.
s: T
4.
f: T
M.sizeT
5.
y: M.size
(y 
upto(0;M.size))
By:
AssertBY (y upto(0;M.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:
