Nuprl Lemma : three-cs-safety

∀[V:Type]
  ∀eq:EqDecider(V). ∀A:Id List. ∀t:ℕ+. ∀f:(V List) ─→ V.
    ((∀vs:V List. (f vs ∈ vs) supposing ||vs|| ≥ 1 )
       ⇒ (∀v:V. ∀s:ts-reachable(three-consensus-ts(V;A;t;f)).
             (three-cs-decided(V;A;t;f;s;v)
             ⇒ ((∃a∈A. (||s a|| ≥ 1 ) ∧ (hd(s a) = Init[v] ∈ consensus-rcv(V;A)))
                ∧ (∀w:V. ∀s':ts-reachable(three-consensus-ts(V;A;t;f)).
                     ((s (ts-rel(three-consensus-ts(V;A;t;f))^*) s')
                     ⇒ three-cs-decided(V;A;t;f;s';w)
                     ⇒ (v = w ∈ V))))))) supposing 
       ((∀vs:V List. ∀v:V.
           ((f vs) = v ∈ V) supposing (((t + 1) ≤ ||filter(λx.(eqof(eq) x v);vs)||) and (||vs|| = ((2 * t) + 1) ∈ ℤ))) a\000Cnd 
       (||A|| = ((3 * t) + 1) ∈ ℤ) and 
       no_repeats(Id;A))


Proof



Definitions occuring in Statement :  three-cs-decided: three-cs-decided(V;A;t;f;s;v),  three-consensus-ts: three-consensus-ts(V;A;t;f),  cs-initial-rcv: Init[v],  consensus-rcv: consensus-rcv(V;A),  Id: Id,  eqof: eqof(d),  deq: EqDecider(T),  l_exists: (∃x∈L. P[x]),  no_repeats: no_repeats(T;l),  l_member: (x ∈ l),  filter: filter(P;l),  hd: hd(l),  length: ||as||,  list: T List,  rel_star: R^*,  nat_plus: ℕ+,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  infix_ap: x f y,  ge: i ≥ j ,  le: A ≤ B,  all: ∀x:A. B[x],  implies: P ⇒ Q,  and: P ∧ Q,  apply: f a,  lambda: λx.A[x],  function: x:A ─→ B[x],  multiply: n * m,  add: n + m,  natural_number: $n,  int: ℤ,  universe: Type,  equal: s = t ∈ T,  ts-reachable: ts-reachable(ts),  ts-rel: ts-rel(ts),  ts-type: ts-type(ts)
Lemmas :  three-cs-safety1,  no_repeats_witness,  Id_wf,  le_wf,  length_wf,  filter_wf5,  l_member_wf,  eqof_wf,  equal_wf,  list_wf,  three-cs-safety2,  three-cs-decided_wf,  subtype_rel_set,  ts-type_wf,  three-consensus-ts_wf,  nat_plus_subtype_nat,  consensus-rcv_wf,  infix_ap_wf,  rel_star_wf,  ts-rel_wf,  ts-init_wf,  subtype_rel_self,  ts-reachable_wf,  subtype_rel_wf,  subtype_rel_dep_function,  all_wf,  isect_wf,  ge_wf,  no_repeats_wf,  nat_plus_wf,  deq_wf
\mforall{}[V:Type]
    \mforall{}eq:EqDecider(V).  \mforall{}A:Id  List.  \mforall{}t:\mBbbN{}\msupplus{}.  \mforall{}f:(V  List)  {}\mrightarrow{}  V.
        ((\mforall{}vs:V  List.  (f  vs  \mmember{}  vs)  supposing  ||vs||  \mgeq{}  1  )
              {}\mRightarrow{}  (\mforall{}v:V.  \mforall{}s:ts-reachable(three-consensus-ts(V;A;t;f)).
                          (three-cs-decided(V;A;t;f;s;v)
                          {}\mRightarrow{}  ((\mexists{}a\mmember{}A.  (||s  a||  \mgeq{}  1  )  \mwedge{}  (hd(s  a)  =  Init[v]))
                                \mwedge{}  (\mforall{}w:V.  \mforall{}s':ts-reachable(three-consensus-ts(V;A;t;f)).
                                          ((s 
                                              (ts-rel(three-consensus-ts(V;A;t;f))\^{}*) 
                                              s')
                                          {}\mRightarrow{}  three-cs-decided(V;A;t;f;s';w)
                                          {}\mRightarrow{}  (v  =  w)))))))  supposing 
              ((\mforall{}vs:V  List.  \mforall{}v:V.
                      ((f  vs)  =  v)  supposing 
                            (((t  +  1)  \mleq{}  ||filter(\mlambda{}x.(eqof(eq)  x  v);vs)||)  and 
                            (||vs||  =  ((2  *  t)  +  1))))  and 
              (||A||  =  ((3  *  t)  +  1))  and 
              no\_repeats(Id;A))


Date html generated: 2015_07_17-AM-11_54_13
Last ObjectModification: 2015_01_28-AM-00_43_15

Home Index