Nuprl Lemma : ma-ring-id-or-diff
R:Id List. s:{i:Id| (i 
R)} 
{i:Id| (i R)} . x:Id. n:
.
(ma-ring(R;s) 
(x R) (||remove-repeats(IdDeq;R)|| | n 
x = (s^n x)))
Proof not projected
Definitions occuring in Statement :
ma-ring: ma-ring(R;s),
id-deq: IdDeq,
Id: Id,
divides: b | a,
length: ||as||,
nat: ,
all: x:A. B[x],
iff: P Q,
implies: P Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
list: type List,
equal: s = t,
l_member: (x l),
fun_exp: f^n,
remove-repeats: remove-repeats(eq;L)
Definitions :
prop: 
,
member: t T,
rev_implies: P Q,
and: P 
Q,
iff: P Q,
implies: P Q,
all: x:A. B[x],
true: True,
squash: 
T,
false: False,
not: 
A,
le: A 
B,
nat_plus: 
,
nat: ,
uall: [x:A]. B[x],
uimplies: b supposing a,
exists: 
x:A. B[x],
divides: b | a
Lemmas :
nat_wf,
ma-ring_wf,
Id_wf,
l_member_wf,
fun_exp_wf,
equal_wf,
id-deq_wf,
remove-repeats_wf,
length_wf,
divides_wf,
length_wf_nat,
le_wf,
fun_exp-rem,
ma-ring-remove-repeats-id
\mforall{}R:Id List. \mforall{}s:\{i:Id| (i \mmember{} R)\} {}\mrightarrow{} \{i:Id| (i \mmember{} R)\} . \mforall{}x:Id. \mforall{}n:\mBbbN{}.
(ma-ring(R;s) {}\mRightarrow{} (x \mmember{} R) {}\mRightarrow{} (||remove-repeats(IdDeq;R)|| | n \mLeftarrow{}{}\mRightarrow{} x = (s\^{}n x)))
Date html generated:
2012_02_20-PM-05_58_35
Last ObjectModification:
2012_02_02-PM-02_30_22
Home
Index