(70steps total)
PrintForm
Definitions
Lemmas
graph
1
3
Sections
Graphs
Doc
At:
adjm
to
adjl
graph
1
2
2
2
1
1
2
1
1
1
2
1
1
1.
size:
2.
m1:
size
size
3.
b1:
size
4.
b2:
size
5.
m1(b1,b2)
6.
i:
7.
i < ||filter(
j.m1(b1,j);upto(0;size))||
8.
b2 = filter(
j.m1(b1,j);upto(0;size))[i]
x:
size, i:
||filter(
j.m1(x,j);upto(0;size))||. m1(x,filter(
j.m1(x,j);upto(0;size))[i])
By:
All Thin
Generated subgoal:
1
3.
x:
size
4.
i:
||filter(
j.m1(x,j);upto(0;size))||
m1(x,filter(
j.m1(x,j);upto(0;size))[i])
3
steps
About:
(70steps total)
PrintForm
Definitions
Lemmas
graph
1
3
Sections
Graphs
Doc