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

At: adjm to adjl graph 1 2 2 2 1 1 1
1. size:
2. m1: sizesize
3. b: sizesize
4. m1(1of(b),2of(b))
(2of(b) filter(j.m1(1of(b),j);upto(0;size)))
By:
RWO Thm* P:(T), L:T List, x:T. (x filter(P;L)) (x L) & P(x) 0
THEN
Reduce 0
Generated subgoal:

1 (2of(b) upto(0;size))2 steps

About:
productlistboolassertnatural_numberlambdaapplyfunctionuniverseandall

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