Nuprl Lemma : consensus-reachable

`∀[V:Type]`
`  ((∀v1,v2:V.  Dec(v1 = v2 ∈ V))`
`  `` {∃v,v':V. (¬(v = v' ∈ V))}`
`  `` (∀A:Id List. ∀W:{a:Id| (a ∈ A)}  List List.`
`        (three-intersection(A;W)`
`        `` (∀ws∈W.∀x:ts-reachable(consensus-ts4(V;A;W))`
`                    ∃y:ConsensusState`
`                     ((x ((λx,y. CR(in ws)[x, y] )^*) y) ∧ (∃v:V. ∃i:ℤ. in state y, inning i has committed v))))))`

Proof

Definitions occuring in Statement :  three-intersection: `three-intersection(A;W)` cs-inning-committed: `in state s, inning i has committed v` consensus-ts4: `consensus-ts4(V;A;W)` consensus-rel-mod: `CR(in ws)[x, y] ` consensus-state4: `ConsensusState` Id: `Id` l_all: `(∀x∈L.P[x])` l_member: `(x ∈ l)` list: `T List` rel_star: `R^*` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` guard: `{T}` infix_ap: `x f y` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` set: `{x:A| B[x]} ` lambda: `λx.A[x]` int: `ℤ` universe: `Type` equal: `s = t ∈ T` ts-reachable: `ts-reachable(ts)`
Lemmas :  three-intersection-two-intersection two-intersection-one-intersection l_all_iff l_member_wf all_wf ts-reachable_wf consensus-ts4_wf subtype_rel_wf ts-type_wf exists_wf consensus-state4_wf infix_ap_wf subtype_rel_set rel_star_wf consensus-rel-mod_wf subtype_rel_dep_function ts-rel_wf ts-init_wf subtype_rel_self cs-inning-committed_wf set_wf Id_wf list-cases length_of_nil_lemma null_nil_lemma btrue_wf member-implies-null-eq-bfalse nil_wf btrue_neq_bfalse product_subtype_list length_of_cons_lemma length_wf non_neg_length length_wf_nat three-intersection_wf list_wf not_wf equal_wf decidable_wf imax-list_wf map_wf cs-inning_wf map_length equal-wf-T-base int_subtype_base fpf-domain_wf cs-estimate_wf top_wf consensus-state4-subtype imax-list-ub l_exists_iff le_wf member_map le_weakening decidable__lt false_wf condition-implies-le minus-add minus-one-mul add-swap add-commutes add_functionality_wrt_le add-associates le-add-cancel less_than_wf deq-member_wf id-deq_wf subtype_rel-deq sq_stable__l_member decidable__equal_Id bool_wf eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot assert-deq-member fresh-inning-reachable eqtt_to_assert assert_wf bnot_wf bool_cases iff_transitivity iff_weakening_uiff assert_of_bnot consensus-ts4-estimate-domain fpf_wf rel_star_transitivity rel_star_monotonic or_wf cs-precondition_wf fpf-join_wf fpf-single_wf int-deq_wf decidable__l_exists cs-archive-blocked_wf decidable__cs-archive-blocked l_all_wf2 decidable__equal_int not-equal-2 less-iff-le lelt_wf list_subtype_base set_subtype_base atom2_subtype_base select_wf sq_stable__le subtype_rel_list primrec-wf2 nat_wf first0 reduce_nil_lemma rel_star_weakening eta_conv iff_weakening_equal firstn_wf subtract_wf assert_of_band decidable__cand decidable__le not-le-2 zero-add minus-minus add-zero decidable__l_member decidable__not eq_id_wf le-add-cancel-alt assert-eq-id assert_elim and_wf eq_id_self band_wf not_assert_elim deq-member-firstn bor_wf deq_wf bfalse_wf rel_rel_star list-subtype l_member-settype pi1_wf_top squash_wf true_wf subtype_rel_product subtype_top pi2_wf member_wf equal-wf-base-T bnot_thru_band assert_of_bor fpf-dom_wf fpf-ap_wf subtype-fpf2 fpf-join-dom-sq deq_member_cons_lemma intdeq_reduce_lemma deq_member_nil_lemma eq_int_wf assert_of_eq_int less_than_transitivity1 less_than_irreflexivity neg_assert_of_eq_int assert_functionality_wrt_uiff bor_ff_simp fpf-join-ap-sq fpf-join-dom equal-wf-base fpf-single-dom ifthenelse_wf member_firstn le_weakening2 le-add-cancel2 less_than_transitivity2 firstn_all iff_imp_equal_bool iff_wf cs-archived_wf fpf-domain-join cons_member fpf_ap_single_lemma uiff_transitivity member-fpf-domain
\mforall{}[V:Type]
((\mforall{}v1,v2:V.    Dec(v1  =  v2))
{}\mRightarrow{}  \{\mexists{}v,v':V.  (\mneg{}(v  =  v'))\}
{}\mRightarrow{}  (\mforall{}A:Id  List.  \mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List.
(three-intersection(A;W)
{}\mRightarrow{}  (\mforall{}ws\mmember{}W.\mforall{}x:ts-reachable(consensus-ts4(V;A;W))
\mexists{}y:ConsensusState
((x  rel\_star(ConsensusState;  \mlambda{}x,y.  CR(in  ws)[x,  y]  )  y)
\mwedge{}  (\mexists{}v:V.  \mexists{}i:\mBbbZ{}.  in  state  y,  inning  i  has  committed  v))))))

Date html generated: 2015_07_17-AM-11_39_52
Last ObjectModification: 2015_07_16-AM-10_24_50

Home Index