Nuprl - Proof: adjm-edge-accum-properties 1 2

(8steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc

1. M: AdjMatrix
2. T: Type
3. s: T
4. x: M.size
5. f: TM.sizeT
6. y: M.size
7. e: {p:(M.sizeM.size)| M.adj(1of(p),2of(p)) }
8. e = < x,y >

M.adj(x,y)

By: Analyze -2 THEN Unhide THEN Analyze -3 THEN All Reduce

Generated subgoal:

1 7. e1: M.size
8. e2: M.size
9. M.adj(e1,e2)
10. < e1,e2 > = < x,y >
M.adj(x,y) 1 step

About:

(8steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc