Nuprl - Proof: adjm to adjl graph 1 2 2 2 1 1 2 1 1 1

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

At: adjm to adjl graph 1 2 2 2 1 1 2 1 1 1

1. size:
2. m1: sizesize
3. b1: size
4. b2: size
5. m1(b1,b2)
6. i:
7. i < ||filter(j.m1(b1,j);upto(0;size))||
8. b2 = filter(j.m1(b1,j);upto(0;size))[i]

< b1,filter(j.m1(b1,j);upto(0;size))[i] > = < b1,b2 > {p:(sizesize)| m1(1of(p),2of(p)) }

By: Analyze

Generated subgoals:

1 < b1,filter(j.m1(b1,j);upto(0;size))[i] > = < b1,b2 > 1 step

2 m1(1of( < b1,filter(j.m1(b1,j);upto(0;size))[i] > ),2of( < b1,filter(j.m1(b1,j);upto(0;size))[i] > )) 7 steps

About:

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

1	`< b1,filter(j.m1(b1,j);upto(0;size))[i] > = < b1,b2 >`	1 step

2	`m1(1of( < b1,filter(j.m1(b1,j);upto(0;size))[i] > ),2of( < b1,filter(j.m1(b1,j);upto(0;size))[i] > ))`	7 steps