---

Step * 2 of Lemma consensus-ts5-true-knowledge


1. V : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
⊢ let x1,x2 = ts-init(consensus-ts5(V;A;W)) 
  in ∀a,b:{a:Id| (a ∈ A)} .
       let I,z = Knowledge(x2;a)(b) 
       in (I ≤ Inning(x1;b))
          ∧ case z
             of inl(p) =>
             let k,v = p 
             in k < I
                ∧ (↑k ∈ dom(Estimate(x1;b)))
                ∧ (Estimate(x1;b)(k) = v ∈ V)
                ∧ (∀i:ℤ. ¬↑i ∈ dom(Estimate(x1;b)) supposing k < i ∧ i < I)
             | inr(p) =>
             ∀i:ℤ. ¬↑i ∈ dom(Estimate(x1;b)) supposing i < I 
       supposing ↑b ∈ dom(Knowledge(x2;a))
BY
{ (RepUR ``ts-init consensus-ts5 cs-knowledge cs-inning cs-estimate`` 0 THEN Auto) }

---

Latex:



1.  V  :  Type
2.  A  :  Id  List@i
3.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
\mvdash{}  let  x1,x2  =  ts-init(consensus-ts5(V;A;W)) 
    in  \mforall{}a,b:\{a:Id|  (a  \mmember{}  A)\}  .
              let  I,z  =  Knowledge(x2;a)(b) 
              in  (I  \mleq{}  Inning(x1;b))
                    \mwedge{}  case  z
                          of  inl(p)  =>
                          let  k,v  =  p 
                          in  k  <  I
                                \mwedge{}  (\muparrow{}k  \mmember{}  dom(Estimate(x1;b)))
                                \mwedge{}  (Estimate(x1;b)(k)  =  v)
                                \mwedge{}  (\mforall{}i:\mBbbZ{}.  \mneg{}\muparrow{}i  \mmember{}  dom(Estimate(x1;b))  supposing  k  <  i  \mwedge{}  i  <  I)
                          |  inr(p)  =>
                          \mforall{}i:\mBbbZ{}.  \mneg{}\muparrow{}i  \mmember{}  dom(Estimate(x1;b))  supposing  i  <  I 
              supposing  \muparrow{}b  \mmember{}  dom(Knowledge(x2;a))


By

(RepUR  ``ts-init  consensus-ts5  cs-knowledge  cs-inning  cs-estimate``  0  THEN  Auto)

---

Home Index