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

(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

y:M.size. x- < vertices = M.size, edges = {p:(M.sizeM.size)| M.adj(1of(p),2of(p)) }, incidence = e.e > - > y (y filter(M.adj(x);upto(0;M.size)))

By: Analyze 0 THEN Unfold `edge` 0 THEN Reduce 0 THEN RWO Thm* P:(T), L:T List, x:T. (x filter(P;L)) (x L) & P(x) 0 THEN ExRepD

Generated subgoals:

1 6. y: M.size
7. e: {p:(M.sizeM.size)| M.adj(1of(p),2of(p)) }
8. e = < x,y >
(y upto(0;M.size)) 2 steps

2 6. y: M.size
7. e: {p:(M.sizeM.size)| M.adj(1of(p),2of(p)) }
8. e = < x,y >
M.adj(x,y) 2 steps

3 6. y: M.size
7. (y upto(0;M.size))
8. M.adj(x,y)
e:{p:(M.sizeM.size)| M.adj(1of(p),2of(p)) }. e = < x,y > 1 step

About:

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

1	6. `y:` `M.size` 7. `e:` `{p:(M.sizeM.size)\| M.adj(1of(p),2of(p)) }` 8. `e = < x,y >` `(y upto(0;M.size))`	2 steps

2	6. `y:` `M.size` 7. `e:` `{p:(M.sizeM.size)\| M.adj(1of(p),2of(p)) }` 8. `e = < x,y >` `M.adj(x,y)`	2 steps

3	6. `y:` `M.size` 7. `(y upto(0;M.size))` 8. `M.adj(x,y)` `e:{p:(M.sizeM.size)\| M.adj(1of(p),2of(p)) }. e = < x,y >`	1 step