### 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