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,  l_exists: (∃x∈L. P[x]),  no_repeats: no_repeats(T;l),  l_member: (x ∈ l),  hd: hd(l),  length: ||as||,  filter: filter(P;l),  list: T List,  eqof: eqof(d),  deq: EqDecider(T),  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)
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  all: ∀x:A. B[x],  uimplies: b supposing a,  implies: P ⇒ Q,  prop: ℙ,  nat_plus: ℕ+,  and: P ∧ Q,  cand: A c∧ B,  subtype_rel: A ⊆r B,  ts-reachable: ts-reachable(ts),  so_lambda: λ2x.t[x],  so_apply: x[s],  ts-type: ts-type(ts),  pi1: fst(t),  three-consensus-ts: three-consensus-ts(V;A;t;f),  infix_ap: x f y,  ge: i ≥ j ,  guard: {T}
Latex:
\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: 2016_05_16-PM-00_48_16
Last ObjectModification: 2015_12_29-PM-01_39_04

Theory : event-ordering


Home Index