Nuprl - Proof: adjm to adjl graph 1 2 2 1 1 1 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))||
7. m1(x,filter(j.m1(x,j);upto(0;size))[a2])
8. x = x1
9. filter(j.m1(x,j);upto(0;size))[a2] = filter(j.m1(x1,j);upto(0;size))[a3]

a2 = a3 ||filter(j.m1(x,j);upto(0;size))||

By: Assert no_repeats(size;filter(j.m1(x,j);upto(0;size)))

Generated subgoals:

1 no_repeats(size;filter(j.m1(x,j);upto(0;size))) 4 steps

2 10. no_repeats(size;filter(j.m1(x,j);upto(0;size)))
a2 = a3 ||filter(j.m1(x,j);upto(0;size))|| 7 steps

About:

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

1	`no_repeats(size;filter(j.m1(x,j);upto(0;size)))`	4 steps

2	10. `no_repeats(size;filter(j.m1(x,j);upto(0;size)))` `a2 = a3 \|\|filter(j.m1(x,j);upto(0;size))\|\|`	7 steps