Nuprl Lemma : remove-repeats-length-no-repeats
[T:Type]. [eq:EqDecider(T)]. [L:T List]. ||remove-repeats(eq;L)|| = ||L|| supposing no_repeats(T;L)
Proof not projected
Definitions occuring in Statement :
length: ||as||,
uimplies: b supposing a,
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 :
append_wf,
remove-repeats_wf,
length_wf,
remove-repeats-append-one-member,
remove-repeats-append,
rev_implies_wf,
iff_wf,
no_repeats_cons,
length_wf_nat,
list_subtype_base,
subtype_base_sq,
subtype_rel_wf,
deq_wf,
no_repeats_wf
\mforall{}[T:Type]. \mforall{}[eq:EqDecider(T)]. \mforall{}[L:T List].
||remove-repeats(eq;L)|| = ||L|| supposing no\_repeats(T;L)
Date html generated:
2012_02_20-PM-05_57_44
Last ObjectModification:
2012_02_02-PM-02_29_56
Home
Index