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

At: adjm to adjl graph 1 1 1 1 1 1

1. size:
2. m1: sizesize
3. x: size
4. i: ||filter(j.m1(x,j);upto(0;size))||
(filter(j.m1(x,j);upto(0;size))[i] filter(j.m1(x,j);upto(0;size)))

By:
Unfold `l_member` 0
THEN
InstConcl [i]


Generated subgoals:

None

About:
boolnatural_numberlambdaapplyfunction

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