Nuprl Lemma : consensus-ts4-ref-map
∀[V:Type]
((∃v,v':V. (¬(v = v' ∈ V)))
⇒ (∀v,v':V. Dec(v = v' ∈ V))
⇒ (∀A:Id List. ∀W:{a:Id| (a ∈ A)} List List.
(two-intersection(A;W) ⇒ (∃f:ConsensusState ─→ (consensus-state3(V) List). cs-ref-map-constraints(V;A;W;f)))))
Proof
Definitions occuring in Statement :
cs-ref-map-constraints: cs-ref-map-constraints(V;A;W;f),
two-intersection: two-intersection(A;W),
consensus-state4: ConsensusState,
consensus-state3: consensus-state3(T),
Id: Id,
l_member: (x ∈ l),
list: T List,
decidable: Dec(P),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
set: {x:A| B[x]} ,
function: x:A ─→ B[x],
universe: Type,
equal: s = t ∈ T
Lemmas :
consensus-ts4-ref-map1,
two-intersection_wf,
list_wf,
Id_wf,
l_member_wf,
all_wf,
decidable_wf,
equal_wf,
exists_wf,
not_wf,
consensus-state4_wf,
consensus-state3_wf,
iff_wf,
equal-wf-T-base,
cs-inning-committable_wf,
cs-commited_wf,
cs-inning-committed_wf,
cs-considering_wf,
decidable__assert,
null_wf3,
subtype_rel_list,
top_wf,
false_wf,
le_wf,
less_than_transitivity1,
less_than_irreflexivity,
less_than_wf,
list-cases,
null_nil_lemma,
btrue_wf,
member-implies-null-eq-bfalse,
nil_wf,
btrue_neq_bfalse,
product_subtype_list,
null_cons_lemma,
cs-inning_wf,
nat_wf,
map_wf,
list-subtype,
map_nil_lemma,
length_of_nil_lemma,
map_cons_lemma,
length_of_cons_lemma,
length-map,
length_wf,
non_neg_length,
length_wf_nat,
imax-list_wf,
imax-list-lb,
imax-list-ub,
l_all_iff,
member-less_than,
l_exists_iff,
isect_wf,
l_exists_wf,
uall_wf,
uiff_wf,
l_all_wf2,
member_map,
equal-wf-base-T,
int_subtype_base,
decidable__lt,
decidable__le,
not-le-2,
less-iff-le,
condition-implies-le,
minus-zero,
add-zero,
minus-add,
minus-minus,
add-swap,
add-commutes,
add-associates,
zero-add,
add_functionality_wrt_le,
le-add-cancel,
l_member-set,
sq_stable__l_member,
decidable__equal_Id,
sq_stable__le,
le-add-cancel-alt,
minus-one-mul,
le_transitivity,
le_weakening,
int_seg_wf,
upto_wf,
length_upto,
select-map,
lelt_wf,
select_upto,
subtype_base_sq,
select_wf
\mforall{}[V:Type]
((\mexists{}v,v':V. (\mneg{}(v = v')))
{}\mRightarrow{} (\mforall{}v,v':V. Dec(v = v'))
{}\mRightarrow{} (\mforall{}A:Id List. \mforall{}W:\{a:Id| (a \mmember{} A)\} List List.
(two-intersection(A;W)
{}\mRightarrow{} (\mexists{}f:ConsensusState {}\mrightarrow{} (consensus-state3(V) List). cs-ref-map-constraints(V;A;W;f)))))
Date html generated:
2015_07_17-AM-11_32_31
Last ObjectModification:
2015_07_16-AM-10_15_03
Home
Index