Nuprl Lemma : ma-ring-all-in-remove-repeats-steps2
R:Id List. s:{i:Id| (i 
R)} 
{i:Id| (i R)} . x:{i:Id| (i R)} .
(ma-ring(R;s) 
(y:{i:Id| (i R)} . 
n:
||remove-repeats(IdDeq;R)||. (y = (s^n x))))
Proof not projected
Definitions occuring in Statement :
ma-ring: ma-ring(R;s),
id-deq: IdDeq,
Id: Id,
length: ||as||,
int_seg: {i..j
},
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
list: type List,
natural_number: $n,
equal: s = t,
l_member: (x l),
fun_exp: f^n,
remove-repeats: remove-repeats(eq;L)
Lemmas :
ma-ring-all-in-remove-repeats-steps1,
Id_wf,
l_member_wf,
ma-ring_wf
\mforall{}R:Id List. \mforall{}s:\{i:Id| (i \mmember{} R)\} {}\mrightarrow{} \{i:Id| (i \mmember{} R)\} . \mforall{}x:\{i:Id| (i \mmember{} R)\} .
(ma-ring(R;s) {}\mRightarrow{} (\mforall{}y:\{i:Id| (i \mmember{} R)\} . \mexists{}n:\mBbbN{}||remove-repeats(IdDeq;R)||. (y = (s\^{}n x))))
Date html generated:
2012_02_20-PM-05_56_01
Last ObjectModification:
2012_02_02-PM-02_29_50
Home
Index