Nuprl Lemma : ma-ring-all-in-remove-repeats-steps1
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:
. ((y = (s^n x)) (
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
},
nat: ,
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 :
atom2_subtype_base,
subtype_base_sq,
intensional-universe_wf,
decidable__ex_int_seg,
select_member,
member-remove-repeats,
l_member_subtype,
int_seg_properties,
select_wf,
decidable__connection,
sq_stable_from_decidable,
surject_wf,
int_seg_wf,
cardinality-le_wf,
subtype_rel_list,
nat_properties,
strong-subtype_wf,
strong-subtype-deq-subtype,
non_neg_length,
false_wf,
not_wf,
length_wf,
le_wf,
connection-bound,
decidable_wf,
decidable__equal_set,
decidable__equal_Id,
assert_wf,
iff_wf,
bool_wf,
subtype_rel_wf,
length_wf_nat,
remove-repeats_wf,
id-deq_wf,
deq_wf,
top_wf,
member_wf,
Id_wf,
l_member_wf,
ma-ring_wf,
nat_wf,
fun_exp_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)\} . \mforall{}n:\mBbbN{}.
((y = (s\^{}n x)) {}\mRightarrow{} (\mexists{}n:\mBbbN{}||remove-repeats(IdDeq;R)||. (y = (s\^{}n x))))))
Date html generated:
2012_02_20-PM-05_55_56
Last ObjectModification:
2012_02_02-PM-02_29_47
Home
Index