Nuprl Lemma : consensus-refinement3
∀[V:Type]
((∀v1,v2:V. Dec(v1 = v2 ∈ V))
⇒ {∃v,v':V. (¬(v = v' ∈ V))}
⇒ (∀L:V List. Dec(∃v:V. (¬(v ∈ L))))
⇒ (∀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) ⇒ ts-refinement(consensus-ts3(V);consensus-ts4(V;A;W);f)))
supposing ||W|| ≥ 1 ))
Proof
Definitions occuring in Statement :
cs-ref-map-constraints: cs-ref-map-constraints(V;A;W;f),
two-intersection: two-intersection(A;W),
consensus-ts4: consensus-ts4(V;A;W),
consensus-state4: ConsensusState,
consensus-ts3: consensus-ts3(T),
consensus-state3: consensus-state3(T),
Id: Id,
l_member: (x ∈ l),
length: ||as||,
list: T List,
decidable: Dec(P),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
guard: {T},
ge: i ≥ j ,
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],
natural_number: $n,
universe: Type,
equal: s = t ∈ T,
ts-refinement: ts-refinement(ts1;ts2;f)
Lemmas :
less_than_wf,
length_wf,
list_wf,
Id_wf,
l_member_wf,
list-cases,
length_of_nil_lemma,
product_subtype_list,
length_of_cons_lemma,
l_all_iff,
cons_wf,
l_all_wf2,
exists_wf,
all_wf,
cs-ref-map-constraints_wf,
consensus-state4_wf,
consensus-state3_wf,
two-intersection_wf,
ge_wf,
decidable_wf,
not_wf,
equal_wf,
cons_member,
sq_stable__l_member,
decidable__equal_Id,
infix_ap_wf,
ts-reachable_wf,
consensus-ts4_wf,
subtype_rel_set,
subtype_rel_wf,
ts-type_wf,
ts-rel_wf,
subtype_rel_dep_function,
subtype_rel_self,
ts-final_wf,
consensus-ts3_wf,
ts-init_wf,
rel_star_weakening,
colist_wf,
has-value_wf-partial,
nat_wf,
set-value-type,
le_wf,
int-value-type,
colength_wf,
decidable__lt,
false_wf,
non_neg_length,
length_wf_nat,
length_cons,
cs-ref-map-unchanged,
cs-ref-map-changed,
cs-ref-map-step,
decidable__le,
decidable__cs-committed-change,
two-intersection-one-intersection,
less_than_transitivity1,
rel_star_wf,
rel_star_transitivity,
firstn_wf,
consensus-state3-cases,
select_wf,
rel_rel_star,
length_firstn,
less_than_transitivity2,
le_weakening2,
lelt_wf,
select_firstn,
sq_stable__le,
iff_weakening_equal,
equal-wf-T-base,
int_subtype_base,
int_seg_wf,
le_weakening,
or_wf,
cs-considering_wf,
cs-commited_wf,
append_wf,
nil_wf,
or_functionality_wrt_iff,
squash_wf,
true_wf,
list_extensionality,
decidable__equal_int,
le_transitivity,
length_firstn_eq,
member_wf,
cs-inning-committable_wf,
cs-inning-committed-committable,
consensus-ts4-inning-committed-stable,
cs-withdrawn_wf,
decidable__equal_cs-withdrawn,
mklist_wf,
eq_int_wf,
bool_wf,
eqtt_to_assert,
assert_of_eq_int,
eqff_to_assert,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_int,
mklist_length,
mklist_select,
subtype_rel_list,
top_wf,
select-firstn,
less_than_irreflexivity,
set_subtype_base,
add-associates,
add-swap,
add-commutes,
zero-add,
last-lemma-sq,
assert_of_null,
assert_wf,
null_wf3,
less-iff-le,
le_antisymmetry_iff,
condition-implies-le,
minus-add,
minus-one-mul,
add_functionality_wrt_le,
add-zero,
le-add-cancel,
not-equal-2,
cs-initial_wf,
decidable__cs-inning-committable,
length-append,
length-singleton,
select_append_back,
subtract_wf,
select_append_front,
le-add-cancel2,
not-le-2,
committed-inning0-reachable,
fpf-single_wf,
set_wf,
equal-wf-base,
fpf_wf,
minus-zero,
fpf_ap_single_lemma,
hd_wf,
hd_member,
null_nil_lemma,
null_cons_lemma
\mforall{}[V:Type]
((\mforall{}v1,v2:V. Dec(v1 = v2))
{}\mRightarrow{} \{\mexists{}v,v':V. (\mneg{}(v = v'))\}
{}\mRightarrow{} (\mforall{}L:V List. Dec(\mexists{}v:V. (\mneg{}(v \mmember{} L))))
{}\mRightarrow{} (\mforall{}A:Id List. \mforall{}W:\{a:Id| (a \mmember{} A)\} List List.
two-intersection(A;W)
{}\mRightarrow{} (\mforall{}f:ConsensusState {}\mrightarrow{} (consensus-state3(V) List)
(cs-ref-map-constraints(V;A;W;f)
{}\mRightarrow{} ts-refinement(consensus-ts3(V);consensus-ts4(V;A;W);f)))
supposing ||W|| \mgeq{} 1 ))
Date html generated:
2015_07_17-AM-11_37_11
Last ObjectModification:
2015_07_16-AM-10_32_48
Home
Index