(11steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: no repeats upto 1 2 1
1. d:
2. 0 < d
3. i,j:. j-i = d-1 no_repeats(;upto(i;j))
4. i:
5. j:
6. j-i = d
7. i < j
no_repeats(;[i / upto(i+1;j)])
By:
RWO Thm* l:T List, x:T. no_repeats(T;[x / l]) no_repeats(T;l) & (x l) 0
THEN
EasyHyp
Generated subgoal:

1 (i upto(i+1;j))1 step

About:
listconsintnatural_numberaddsubtractless_thanuniverseequalimpliesandall

(11steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc