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

At: adjm to adjl graph 1 2 2 2 1 1 2 1
1. size:
2. m1: sizesize
3. b: sizesize
4. m1(1of(b),2of(b))
5. i:
6. i < ||filter(j.m1(1of(b),j);upto(0;size))||
7. 2of(b) = filter(j.m1(1of(b),j);upto(0;size))[i]
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)) }
By:
InstConcl [ < 1of(b),i > ]
THEN
Reduce 0
Generated subgoals:

1 < 1of(b),filter(j.m1(1of(b),j);upto(0;size))[i] > = b {p:(sizesize)| m1(1of(p),2of(p)) }10 steps
 
28. a: x:size||filter(j.m1(x,j);upto(0;size))||
9. x: size
10. i1: ||filter(j.m1(x,j);upto(0;size))||
11. a = < x,i1 > x:size||filter(j.m1(x,j);upto(0;size))||
< x,filter(j.m1(x,j);upto(0;size))[i1] > {p:(sizesize)| m1(1of(p),2of(p)) }		7 steps

About:
pairspreadproductproductboolassertnatural_numberless_than
setlambdaapplyfunctionequalmember
exists

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