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

At: adjm to adjl graph 1 1 1 1 1 2
1. size:
2. m1: sizesize
3. x: size
4. i: ||filter(j.m1(x,j);upto(0;size))||
5. (filter(j.m1(x,j);upto(0;size))[i] filter(j.m1(x,j);upto(0;size)))
m1(x,filter(j.m1(x,j);upto(0;size))[i])
By:
RWO Thm* P:(T), L:T List, x:T. (x filter(P;L)) (x L) & P(x) -1
THEN
Reduce -1
Generated subgoals:

None

About:
listboolassertnatural_numberlambdaapplyfunctionuniverseandall

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