(70steps total)
PrintForm
Definitions
Lemmas
graph
1
3
Sections
Graphs
Doc
At:
adjm
to
adjl
graph
1
2
2
1
1
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.
m1(x,filter(
j.m1(x,j);upto(0;size))[a2])
8.
x = x1
9.
filter(
j.m1(x,j);upto(0;size))[a2] = filter(
j.m1(x1,j);upto(0;size))[a3]
a2 = a3
||filter(
j.m1(x,j);upto(0;size))||
By:
Assert no_repeats(
size;filter(
j.m1(x,j);upto(0;size)))
Generated subgoals:
1
no_repeats(
size;filter(
j.m1(x,j);upto(0;size)))
4
steps
 
2
10.
no_repeats(
size;filter(
j.m1(x,j);upto(0;size)))
a2 = a3
||filter(
j.m1(x,j);upto(0;size))||
7
steps
About:
(70steps total)
PrintForm
Definitions
Lemmas
graph
1
3
Sections
Graphs
Doc