Nuprl Lemma : remove-repeats-length-no-repeats-iff
[T:Type]. [eq:EqDecider(T)]. [L:T List]. uiff(no_repeats(T;L);||remove-repeats(eq;L)|| = ||L||)
Proof not projected
Definitions occuring in Statement :
length: ||as||,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
list: type List,
int: 
,
universe: Type,
equal: s = t,
no_repeats: no_repeats(T;l),
remove-repeats: remove-repeats(eq;L),
deq: EqDecider(T)
Lemmas :
false_wf,
remove-repeats-length-leq,
member-remove-repeats,
l_member_wf,
set-equal_wf,
remove-repeats-set-equal,
int_subtype_base,
subtype_base_sq,
remove-repeats-append-one-member,
remove-repeats-append,
rev_implies_wf,
iff_wf,
no_repeats_cons,
no_repeats_nil,
not_wf,
nat_wf,
uall_wf,
remove-repeats-length-no-repeats,
length_wf_nat,
no_repeats_wf,
uiff_wf,
deq_wf,
length_wf,
remove-repeats_wf,
no_repeats_witness
\mforall{}[T:Type]. \mforall{}[eq:EqDecider(T)]. \mforall{}[L:T List]. uiff(no\_repeats(T;L);||remove-repeats(eq;L)|| = ||L||)
Date html generated:
2012_02_20-PM-05_57_54
Last ObjectModification:
2012_02_02-PM-02_30_02
Home
Index