(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.
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;filter(
j.m1(x,j);upto(0;size)))
By:
BackThru
Thm*
P:(T
), l:T List. no_repeats(T;l)
no_repeats(T;filter(P;l))
Generated subgoal:
1
no_repeats(
size;upto(0;size))
3
steps
About:
(70steps total)
PrintForm
Definitions
Lemmas
graph
1
3
Sections
Graphs
Doc