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

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

1. size:
2. m1: sizesize
3. x: size
4. a2: ||filter(j.m1(x,j);upto(0;size))||
5. x1: size
6. a3: ||filter(j.m1(x1,j);upto(0;size))||

< x,filter(j.m1(x,j);upto(0;size))[a2] > = < x1,filter(j.m1(x1,j);upto(0;size))[a3] > {p:(sizesize)| m1(1of(p),2of(p)) } < x,a2 > = < x1,a3 > x:size||filter(j.m1(x,j);upto(0;size))||

By: (Analyze 0) THENA (Auto THEN Analyze THEN (Reduce 0))

Generated subgoals:

1 7. < x,filter(j.m1(x,j);upto(0;size))[a2] > = < x1,filter(j.m1(x1,j);upto(0;size))[a3] > {p:(sizesize)| m1(1of(p),2of(p)) }
< x,a2 > = < x1,a3 > x:size||filter(j.m1(x,j);upto(0;size))|| 14 steps

2 m1(x,filter(j.m1(x,j);upto(0;size))[a2]) 6 steps

3 m1(x1,filter(j.m1(x1,j);upto(0;size))[a3]) 6 steps

About:

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

1	7. `< x,filter(j.m1(x,j);upto(0;size))[a2] > = < x1,filter(j.m1(x1,j);upto(0;size))[a3] > {p:(sizesize)\| m1(1of(p),2of(p)) }` `< x,a2 > = < x1,a3 > x:size\|\|filter(j.m1(x,j);upto(0;size))\|\|`	14 steps

2	`m1(x,filter(j.m1(x,j);upto(0;size))[a2])`	6 steps

3	`m1(x1,filter(j.m1(x1,j);upto(0;size))[a3])`	6 steps