(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 1 2 1 1

1. size:
2. m1: sizesize
3. b1: size
4. b2: size
5. m1(b1,b2)
6. i:
7. i < ||filter(j.m1(b1,j);upto(0;size))||
8. b2 = filter(j.m1(b1,j);upto(0;size))[i]
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:
boolassertnatural_numberless_thanlambdaapplyfunctionequalall

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