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

At: adjm to adjl graph 1 2 2 1
1. size:
2. m1: sizesize
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 = a2
By: RepeatFor 2 ((Analyze 0) THEN (Analyze -1) THEN (Reduce 0))
Generated subgoal:

13. 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))||		27 steps

About:
pairspreadproductproductboolassertnatural_number
setlambdaapplyfunctionequalimplies
all

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