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

At: adjm to adjl graph 1 2 3
1. size:
2. m1: sizesize
(x. < 1of(x),filter(j.m1(1of(x),j);upto(0;size))[2of(x)] > ) = (e.e) o (e.e/x,i. < x,filter(j.m1(x,j);upto(0;size))[i] > ) (x:size||filter(j.m1(x,j);upto(0;size))||)sizesize
By: Ext THENA (Auto THEN (Analyze -1) THEN (Reduce 0))
Generated subgoal:

13. x: x:size||filter(j.m1(x,j);upto(0;size))||
(x. < 1of(x),filter(j.m1(1of(x),j);upto(0;size))[2of(x)] > )(x) = ((e.e) o (e.e/x,i. < x,filter(j.m1(x,j);upto(0;size))[i] > ))(x) sizesize		2 steps

About:
pairspreadproductproductboolnatural_numberlambdaapplyfunctionequal

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