At:
adjm-edge-accum-properties
1
3
1.
M: AdjMatrix
2.
T: Type
3.
s: T
4.
x: 
M.size
5.
f: T
M.sizeT
6.
y: M.size
7.
(y 
upto(0;M.size))
8.
M.adj(x,y)
e:{p:(M.size
M.size)| M.adj(1of(p),2of(p)) }. e = < x,y >
By:
InstConcl [ < x,y > ]
THEN
Analyze
THEN
Reduce 0
Generated subgoals:
None
About:
