Nuprl - Proof: adjm to adjl graph 1 1 1

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

1. size:
2. m1: sizesize
3. e: x:size||filter(j.m1(x,j);upto(0;size))||
4. x: size
5. i: ||filter(j.m1(x,j);upto(0;size))||
6. e = < x,i > x:size||filter(j.m1(x,j);upto(0;size))||

m1(x,filter(j.m1(x,j);upto(0;size))[i])

By: Assert (x:size, i:||filter(j.m1(x,j);upto(0;size))||. m1(x,filter(j.m1(x,j);upto(0;size))[i]))

Generated subgoals:

1 x:size, i:||filter(j.m1(x,j);upto(0;size))||. m1(x,filter(j.m1(x,j);upto(0;size))[i]) 4 steps

2 7. x:size, i:||filter(j.m1(x,j);upto(0;size))||. m1(x,filter(j.m1(x,j);upto(0;size))[i])
m1(x,filter(j.m1(x,j);upto(0;size))[i]) 1 step

About:

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

1	`x:size, i:\|\|filter(j.m1(x,j);upto(0;size))\|\|. m1(x,filter(j.m1(x,j);upto(0;size))[i])`	4 steps

2	7. `x:size, i:\|\|filter(j.m1(x,j);upto(0;size))\|\|. m1(x,filter(j.m1(x,j);upto(0;size))[i])` `m1(x,filter(j.m1(x,j);upto(0;size))[i])`	1 step