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

At: adjm to adjl graph 1 2 2 1 1 3

1. size:
2. m1: sizesize
3. 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))||
m1(x1,filter(j.m1(x1,j);upto(0;size))[a3])

By: Assert (x:size, i:||filter(j.m1(x,j);upto(0;size))||. m1(x,filter(j.m1(x,j);upto(0;size))[i]))

Generated subgoals:

1 x:size, i:||filter(j.m1(x,j);upto(0;size))||. m1(x,filter(j.m1(x,j);upto(0;size))[i])4 steps
 
27. x:size, i:||filter(j.m1(x,j);upto(0;size))||. m1(x,filter(j.m1(x,j);upto(0;size))[i])
m1(x1,filter(j.m1(x1,j);upto(0;size))[a3])
1 step

About:
boolassertnatural_numberlambdaapplyfunctionall

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