(70steps total)
PrintForm
Definitions
Lemmas
graph
1
3
Sections
Graphs
Doc
At:
adjm
to
adjl
graph
1
2
2
2
2
1.
size:
2.
m1:
size
size
3.
b:
size
size
4.
m1(1of(b),2of(b))
5.
m1(1of(b),2of(b))
a:(x:
size
||filter(
j.m1(x,j);upto(0;size))||). (a/x,i. < x,filter(
j.m1(x,j);upto(0;size))[i] > ) = b
{p:(
size
size)| m1(1of(p),2of(p)) }
By:
Analyze -1
THEN
Unhide
Generated subgoals:
None
About:
(70steps total)
PrintForm
Definitions
Lemmas
graph
1
3
Sections
Graphs
Doc
size
size
size
size
m1(1of(b),2of(b))
a:(x:size||filter(
j.m1(x,j);upto(0;size))||). (a/x,i. < x,filter(j.m1(x,j);upto(0;size))[i] > ) = b 
{p:(sizesize)| m1(1of(p),2of(p)) }
