(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
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]
no_repeats(
size;upto(0;size))
By:
Assert no_repeats(
;upto(0;size))
Generated subgoals:
1
no_repeats(
;upto(0;size))
1
step
 
2
10.
no_repeats(
;upto(0;size))
no_repeats(
size;upto(0;size))
1
step
About:
(70steps total)
PrintForm
Definitions
Lemmas
graph
1
3
Sections
Graphs
Doc