Nuprl Lemma : consensus-ts6-reachability1

∀[V:Type]
  ∀A:Id List. ∀W:{a:Id| (a ∈ A)}  List List. ∀L:consensus-event(V;A) List.
  ∀x,y:{a:Id| (a ∈ A)}  ─→ (consensus-event(V;A) List). ∀a:{a:Id| (a ∈ A)} .
    ((∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀z:ℕi × V?.
        ((consensus-message(b;i;z) ∈ L)
        ⇒ let i',est,knw = consensus-accum-state(A;x b) in 
           (i ≤ i')
           ∧ case z
              of inl(p) =>
              let j,v = p 
              in (↑j ∈ dom(est)) ∧ (∀k:ℤ. (¬↑k ∈ dom(est)) supposing (k < i and j < k)) ∧ (v = est(j) ∈ V)
              | inr(a) =>
              ∀j:ℤ. ¬↑j ∈ dom(est) supposing j < i))
       ⇒ (∀v:V. ∀j:ℕ||L||.
             let i,est,knw = consensus-accum-state(A;(x a) @ firstn(j;L)) in 
             (¬(i ∈ fpf-domain(est))) ∧ may consider v in inning i based on knowledge (knw) 
             supposing L[j] = Archive(v) ∈ consensus-event(V;A))
       ⇒ (x (ts-rel(consensus-ts6(V;A;W))^*) y)) supposing 
       (((y a) = ((x a) @ L) ∈ (consensus-event(V;A) List)) and 
       (∀b:{a:Id| (a ∈ A)} . (y b) = (x b) ∈ (consensus-event(V;A) List) supposing ¬(b = a ∈ Id)))


Proof



Definitions occuring in Statement :  consensus-ts6: consensus-ts6(V;A;W),  consensus-accum-state: consensus-accum-state(A;L),  consensus-message: consensus-message(b;i;z),  archive-event: Archive(v),  consensus-event: consensus-event(V;A),  cs-knowledge-precondition: may consider v in inning i based on knowledge (s),  fpf-ap: f(x),  fpf-domain: fpf-domain(f),  fpf-dom: x ∈ dom(f),  Id: Id,  int-deq: IntDeq,  l_member: (x ∈ l),  select: L[n],  firstn: firstn(n;as),  length: ||as||,  append: as @ bs,  list: T List,  rel_star: R^*,  int_seg: {i..j-},  nat: ℕ,  assert: ↑b,  less_than: a < b,  spreadn: spread3,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  infix_ap: x f y,  le: A ≤ B,  all: ∀x:A. B[x],  not: ¬A,  implies: P ⇒ Q,  and: P ∧ Q,  unit: Unit,  set: {x:A| B[x]} ,  apply: f a,  function: x:A ─→ B[x],  spread: spread def,  product: x:A × B[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  union: left + right,  natural_number: $n,  int: ℤ,  universe: Type,  equal: s = t ∈ T,  ts-rel: ts-rel(ts),  ts-type: ts-type(ts)
Lemmas :  consensus-event_wf,  subtype_rel_self,  subtype_rel_dep_function,  ts-rel_wf,  consensus-ts6_wf,  ts-type_wf,  rel_star_wf,  infix_ap_wf,  cs-knowledge-precondition_wf,  fpf-domain_wf,  fpf_wf,  firstn_wf,  consensus-accum-state_wf,  archive-event_wf,  sq_stable__le,  select_wf,  length_wf,  fpf-ap_wf,  less_than_wf,  top_wf,  subtype-fpf2,  int-deq_wf,  fpf-dom_wf,  assert_wf,  le_wf,  int_seg_properties,  consensus-message_wf,  unit_wf2,  int_seg_wf,  nat_wf,  append_wf,  equal_wf,  not_wf,  isect_wf,  list_wf,  l_member_wf,  Id_wf,  all_wf,  nil_wf,  set_wf,  length_of_nil_lemma,  stuck-spread,  base_wf,  list_ind_nil_lemma,  append-nil,  subtype_rel_list,  rel_star_weakening,  decidable__equal_Id,  member_wf,  iff_weakening_equal,  btrue_neq_bfalse,  member-implies-null-eq-bfalse,  btrue_wf,  null_nil_lemma,  subtype-fpf3,  cons_wf,  rel_star_transitivity,  assert-bnot,  bool_subtype_base,  subtype_base_sq,  bool_cases_sqequal,  eqff_to_assert,  assert-eq-id,  eqtt_to_assert,  bool_wf,  eq_id_wf,  member_append,  select_append_front,  lelt_wf,  length_append,  length_wf_nat,  length_cons,  length_wf_nil,  non_neg_length,  length_nil,  le-add-cancel,  add-associates,  add_functionality_wrt_le,  add-commutes,  add-swap,  minus-one-mul,  minus-add,  condition-implies-le,  less-iff-le,  false_wf,  decidable__lt,  firstn_append,  rel_rel_star,  assert_of_bnot,  iff_weakening_uiff,  iff_transitivity,  uiff_transitivity,  bnot_wf,  equal-wf-T-base,  zero-le-nat,  add-zero,  zero-mul,  add-mul-special,  le_weakening,  length_of_cons_lemma,  select_append_back,  firstn_all,  cons_member,  list_accum_append,  atom2_subtype_base,  list_accum_nil_lemma,  list_accum_cons_lemma,  assert_witness,  consensus-accum_wf,  list_accum_wf,  equal-wf-base,  last_induction,  fpf-join_wf,  or_wf,  fpf-single-dom,  int_subtype_base,  fpf-single_wf,  fpf-join-dom,  not-le-2,  decidable__le,  less_than_irreflexivity,  less_than_transitivity1,  fpf-join-ap,  append_assoc,  one-consensus-event_wf,  consensus-event-constraint_wf,  and_wf,  exists_wf
\mforall{}[V:Type]
    \mforall{}A:Id  List.  \mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List.  \mforall{}L:consensus-event(V;A)  List.
    \mforall{}x,y:\{a:Id|  (a  \mmember{}  A)\}    {}\mrightarrow{}  (consensus-event(V;A)  List).  \mforall{}a:\{a:Id|  (a  \mmember{}  A)\}  .
        ((\mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}i:\mBbbN{}.  \mforall{}z:\mBbbN{}i  \mtimes{}  V?.
                ((consensus-message(b;i;z)  \mmember{}  L)
                {}\mRightarrow{}  let  i',est,knw  =  consensus-accum-state(A;x  b)  in 
                      (i  \mleq{}  i')
                      \mwedge{}  case  z
                            of  inl(p)  =>
                            let  j,v  =  p 
                            in  (\muparrow{}j  \mmember{}  dom(est))  \mwedge{}  (\mforall{}k:\mBbbZ{}.  (\mneg{}\muparrow{}k  \mmember{}  dom(est))  supposing  (k  <  i  and  j  <  k))  \mwedge{}  (v  =  est(j\000C))
                            |  inr(a)  =>
                            \mforall{}j:\mBbbZ{}.  \mneg{}\muparrow{}j  \mmember{}  dom(est)  supposing  j  <  i))
              {}\mRightarrow{}  (\mforall{}v:V.  \mforall{}j:\mBbbN{}||L||.
                          let  i,est,knw  =  consensus-accum-state(A;(x  a)  @  firstn(j;L))  in 
                          (\mneg{}(i  \mmember{}  fpf-domain(est)))  \mwedge{}  may  consider  v  in  inning  i  based  on  knowledge  (knw) 
                          supposing  L[j]  =  Archive(v))
              {}\mRightarrow{}  (x  rel\_star(ts-type(consensus-ts6(V;A;W));  ts-rel(consensus-ts6(V;A;W)))  y))  supposing 
              (((y  a)  =  ((x  a)  @  L))  and 
              (\mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  (y  b)  =  (x  b)  supposing  \mneg{}(b  =  a)))


Date html generated: 2015_07_17-AM-11_46_31
Last ObjectModification: 2015_07_16-AM-09_46_03

Home Index