Nuprl Lemma : ma-ring-no-repeats-listify
R:Id List. s:{i:Id| (i 
R)} 
{i:Id| (i R)} . x:Id.
(ma-ring(R;s) 
(x R) no_repeats(Id;(
n.(s^n x))[
||remove-repeats(IdDeq;R)||]))
Proof not projected
Definitions occuring in Statement :
ma-ring: ma-ring(R;s),
id-deq: IdDeq,
Id: Id,
listify: listify(f;m;n),
length: ||as||,
all: x:A. B[x],
implies: P Q,
set: {x:A| B[x]} ,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
list: type List,
natural_number: $n,
no_repeats: no_repeats(T;l),
l_member: (x l),
fun_exp: f^n,
remove-repeats: remove-repeats(eq;L)
Lemmas :
ma-ring-remove-repeats-eq-set-listify,
remove-repeats_property,
non_neg_length,
listify_length,
iff_wf,
l_eqset_wf,
ma-ring_wf,
l_contains-eq_set-no_repeats,
listify_wf,
length_wf,
remove-repeats_wf,
id-deq_wf,
fun_exp_wf,
le_wf,
l_member_wf,
int_seg_wf,
length_wf_nat,
no_repeats_wf,
uall_wf,
Id_wf,
nat_wf,
not_wf
\mforall{}R:Id List. \mforall{}s:\{i:Id| (i \mmember{} R)\} {}\mrightarrow{} \{i:Id| (i \mmember{} R)\} . \mforall{}x:Id.
(ma-ring(R;s) {}\mRightarrow{} (x \mmember{} R) {}\mRightarrow{} no\_repeats(Id;(\mlambda{}n.(s\^{}n x))[\mBbbN{}||remove-repeats(IdDeq;R)||]))
Date html generated:
2012_02_20-PM-05_58_04
Last ObjectModification:
2012_02_02-PM-02_30_08
Home
Index