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

At: adjm to adjl graph 1 1 1 1
1. size:
2. m1: sizesize
3. e: x:size||filter(j.m1(x,j);upto(0;size))||
4. x: size
5. i: ||filter(j.m1(x,j);upto(0;size))||
6. e = < x,i > x:size||filter(j.m1(x,j);upto(0;size))||
x:size, i:||filter(j.m1(x,j);upto(0;size))||. m1(x,filter(j.m1(x,j);upto(0;size))[i])
By: All Thin
Generated subgoal:

13. x: size
4. i: ||filter(j.m1(x,j);upto(0;size))||
m1(x,filter(j.m1(x,j);upto(0;size))[i])		3 steps

About:
pairproductboolassertnatural_numberlambdaapplyfunctionequalall

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