(70steps total)
PrintForm
Definitions
Lemmas
graph
1
3
Sections
Graphs
Doc
At:
adjm
to
adjl
graph
1
2
2
1
1
1
1.
size:
2.
m1:
size
size
3.
x:
size
4.
a2:
||filter(
j.m1(x,j);upto(0;size))||
5.
x1:
size
6.
a3:
||filter(
j.m1(x1,j);upto(0;size))||
7.
< x,filter(
j.m1(x,j);upto(0;size))[a2] > = < x1,filter(
j.m1(x1,j);upto(0;size))[a3] >
{p:(
size
size)| m1(1of(p),2of(p)) }
< x,a2 > = < x1,a3 >
x:
size
||filter(
j.m1(x,j);upto(0;size))||
By:
Analyze -1
THEN
Reduce -1
Generated subgoal:
1
7.
< x,filter(
j.m1(x,j);upto(0;size))[a2] > = < x1,filter(
j.m1(x1,j);upto(0;size))[a3] >
8.
m1(x,filter(
j.m1(x,j);upto(0;size))[a2])
< x,a2 > = < x1,a3 >
x:
size
||filter(
j.m1(x,j);upto(0;size))||
13
steps
About:
(70steps total)
PrintForm
Definitions
Lemmas
graph
1
3
Sections
Graphs
Doc