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

At: adjm to adjl graph 1 2 2
1. size:
2. m1: sizesize
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] > )
By:
Unfold `biject` 0
THEN
Unfolds [`surject`;`inject`] 0
THEN
Reduce 0
THEN
Analyze 0
Generated subgoals:

1 a1,a2:(x:size||filter(j.m1(x,j);upto(0;size))||). (a1/x,i. < x,filter(j.m1(x,j);upto(0;size))[i] > ) = (a2/x,i. < x,filter(j.m1(x,j);upto(0;size))[i] > ) {p:(sizesize)| m1(1of(p),2of(p)) } a1 = a228 steps
 
2 b:{p:(sizesize)| m1(1of(p),2of(p)) }. a:(x:size||filter(j.m1(x,j);upto(0;size))||). (a/x,i. < x,filter(j.m1(x,j);upto(0;size))[i] > ) = b {p:(sizesize)| m1(1of(p),2of(p)) }26 steps

About:
pairspreadproductproductboolassertnatural_numberset
lambdaapplyfunctionequalimpliesallexists

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