Nuprl Lemma : ma-ring-property2
R:Id List. s:{i:Id| (i 
R)} 
{i:Id| (i R)} . i:Id.
(ma-ring(R;s)
(i R)
(
R':Id List
(l_eqset(Id;R';R)
ma-ring(R';s)
(i = hd(R'))
(j:
||R'|| - 1. ((s R'[j]) = R'[j + 1]))
((s R'[||R'|| - 1]) = R'[0])
no_repeats(Id;R'))))
Proof not projected
Definitions occuring in Statement :
ma-ring: ma-ring(R;s),
l_eqset: l_eqset(T;L1;L2),
Id: Id,
select: l[i],
hd: hd(l),
length: ||as||,
int_seg: {i..j
},
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
and: P Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
list: type List,
subtract: n - m,
add: n + m,
natural_number: $n,
equal: s = t,
no_repeats: no_repeats(T;l),
listp: A List,
l_member: (x l)
Lemmas :
listp_properties,
intensional-universe_wf,
l_member_subtype,
select_member,
ma-ring-no-repeats-listify,
ma-ring-remove-repeats-id,
fun_exp_add1-sq,
squash_wf,
fun_exp_add1,
select-as-hd,
pos-length,
equal-nil-sq-nil,
l_member_length,
ma-ring-remove-repeats-eq-set-listify,
subtype_rel_wf,
deq_wf,
top_wf,
bool_wf,
select_listify_id,
non_neg_length,
strong-subtype-deq-subtype,
strong-subtype_wf,
nat_properties,
subtype_rel_list,
rev_implies_wf,
subtype_base_sq,
atom2_subtype_base,
int_subtype_base,
fun_exp_set_l_member,
iff_wf,
nat_wf,
inject_wf,
hd_wf,
length_wf_nat,
select_wf,
not_wf,
uall_wf,
ge_wf,
pos_length3,
int_seg_properties,
member_wf,
no_repeats-settype,
assert_wf,
listify_length,
member_null,
pos_length2,
listify_wf,
fun_exp_wf,
le_wf,
length_wf,
assert_of_lt_int,
non_nil_length,
l_member_non_nil,
member-remove-repeats,
true_wf,
lt_int_wf,
ifthenelse_wf,
false_wf,
id-deq_wf,
remove-repeats_wf,
no_repeats_wf,
int_seg_wf,
l_eqset_wf,
ma-ring_wf,
l_member_wf,
Id_wf
\mforall{}R:Id List. \mforall{}s:\{i:Id| (i \mmember{} R)\} {}\mrightarrow{} \{i:Id| (i \mmember{} R)\} . \mforall{}i:Id.
(ma-ring(R;s)
{}\mRightarrow{} (i \mmember{} R)
{}\mRightarrow{} (\mexists{}R':Id List\msupplus{}
(l\_eqset(Id;R';R)
\mwedge{} ma-ring(R';s)
\mwedge{} (i = hd(R'))
\mwedge{} (\mforall{}j:\mBbbN{}||R'|| - 1. ((s R'[j]) = R'[j + 1]))
\mwedge{} ((s R'[||R'|| - 1]) = R'[0])
\mwedge{} no\_repeats(Id;R'))))
Date html generated:
2012_02_20-PM-05_58_49
Last ObjectModification:
2012_02_02-PM-02_30_28
Home
Index