Nuprl Lemma : ma-ring-id-or-diff2
R:Id List. s:{i:Id| (i 
R)} 
{i:Id| (i R)} . x:{x:Id| (x R)} .
(ma-ring(R;s) 
no_repeats(Id;R) (x = (s^||R|| x)))
Proof not projected
Definitions occuring in Statement :
ma-ring: ma-ring(R;s),
Id: Id,
length: ||as||,
all: x:A. B[x],
implies: P Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
list: type List,
equal: s = t,
no_repeats: no_repeats(T;l),
l_member: (x l),
fun_exp: f^n
Definitions :
all: x:A. B[x],
implies: P Q,
member: t T,
top: Top,
subtype: S 
T,
squash: 
T,
true: True,
iff: P 
Q,
uall: [x:A]. B[x],
sq_stable: SqStable(P),
prop: 
,
and: P 
Q,
uiff: uiff(P;Q),
uimplies: b supposing a,
sq_type: SQType(T),
guard: {T}
Lemmas :
ma-ring-id-or-diff,
length_wf_nat,
top_wf,
Id_wf,
sq_stable_from_decidable,
l_member_wf,
decidable__l_member,
decidable__equal_Id,
remove-repeats-length-no-repeats-iff,
id-deq_wf,
subtype_base_sq,
int_subtype_base,
divides_reflexivity,
no_repeats_wf,
ma-ring_wf
\mforall{}R:Id List. \mforall{}s:\{i:Id| (i \mmember{} R)\} {}\mrightarrow{} \{i:Id| (i \mmember{} R)\} . \mforall{}x:\{x:Id| (x \mmember{} R)\} .
(ma-ring(R;s) {}\mRightarrow{} no\_repeats(Id;R) {}\mRightarrow{} (x = (s\^{}||R|| x)))
Date html generated:
2012_02_20-PM-05_58_41
Last ObjectModification:
2012_02_02-PM-02_30_25
Home
Index