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

At: adjm to adjl graph
m:AdjMatrix. adjl-graph(adjm_to_adjl(m)) adjm-graph(m)
By:
(Auto THEN (Analyze 1) THEN (Unfolds [`adjl-graph`;`adjm-graph`;`adjm_to_adjl`;`graph-isomorphic`] 0) THEN (Reduce 0) THEN (InstConcl [Id])) THENA (Auto THEN (Analyze -1) THEN (Reduce 0))
THEN
Unfold `compose2` 0
THEN
Reduce 0
Generated subgoal:

11. 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		69 steps

About:
pairproductproductassertnatural_numbersetlambda
applyfunctionequalandallexists

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