(70steps total)
PrintForm
Definitions
Lemmas
graph
1
3
Sections
Graphs
Doc
At:
adjm
to
adjl
graph
1
2
2
2
1
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:
Thin -2
Generated subgoal:
1
4.
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)) }
23
steps
About:
(70steps total)
PrintForm
Definitions
Lemmas
graph
1
3
Sections
Graphs
Doc