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

At: adjm to adjl graph 1
1. size:
2. m1: sizesize
emap:((x:size||filter(j.m1(x,j);upto(0;size))||){p:(sizesize)| m1(1of(p),2of(p)) }). Bij(size; size; Id) & Bij(x:size||filter(j.m1(x,j);upto(0;size))||; {p:(sizesize)| m1(1of(p),2of(p)) }; emap) & (x. < 1of(x),filter(j.m1(1of(x),j);upto(0;size))[2of(x)] > ) = (e.e) o emap (x:size||filter(j.m1(x,j);upto(0;size))||)sizesize
By: InstConcl [e.e/x,i. < x,filter(j.m1(x,j);upto(0;size))[i] > ]
Generated subgoals:

1 (e.e/x,i. < x,filter(j.m1(x,j);upto(0;size))[i] > ) (x:size||filter(j.m1(x,j);upto(0;size))||){p:(sizesize)| m1(1of(p),2of(p)) }7 steps
 
2 Bij(size; size; Id) & Bij(x:size||filter(j.m1(x,j);upto(0;size))||; {p:(sizesize)| m1(1of(p),2of(p)) }; e.e/x,i. < x,filter(j.m1(x,j);upto(0;size))[i] > ) & (x. < 1of(x),filter(j.m1(1of(x),j);upto(0;size))[2of(x)] > ) = (e.e) o (e.e/x,i. < x,filter(j.m1(x,j);upto(0;size))[i] > ) (x:size||filter(j.m1(x,j);upto(0;size))||)sizesize60 steps
 
33. emap: (x:size||filter(j.m1(x,j);upto(0;size))||){p:(sizesize)| m1(1of(p),2of(p)) }
(Bij(size; size; Id) & Bij(x:size||filter(j.m1(x,j);upto(0;size))||; {p:(sizesize)| m1(1of(p),2of(p)) }; emap) & (x. < 1of(x),filter(j.m1(1of(x),j);upto(0;size))[2of(x)] > ) = (e.e) o emap (x:size||filter(j.m1(x,j);upto(0;size))||)sizesize) Prop		1 step

About:
pairspreadproductproductboolassertnatural_numberset
lambdaapplyfunctionequalmemberpropandexists

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