---

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


1. [V] : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. x1 : ConsensusState@i
5. x2 : Knowledge(ConsensusState)@i
⊢ ∀a:{a:Id| (a ∈ A)} 
    SqStable(∀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
{ ((D 0 THENA Auto) THEN GenConclAtAddr [1;2;2;1;1]⋅) }

1
1. [V] : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. x1 : ConsensusState@i
5. x2 : Knowledge(ConsensusState)@i
6. a : {a:Id| (a ∈ A)} @i
7. v : b:Id fp-> ℤ × (ℤ × V + Top)@i
8. Knowledge(x2;a) = v ∈ b:Id fp-> ℤ × (ℤ × V + Top)@i
⊢ SqStable(∀b:{a:Id| (a ∈ A)} 
             let I,z = v(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(v))

---

Latex:



1.  [V]  :  Type
2.  A  :  Id  List@i
3.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
4.  x1  :  ConsensusState@i
5.  x2  :  Knowledge(ConsensusState)@i
\mvdash{}  \mforall{}a:\{a:Id|  (a  \mmember{}  A)\} 
        SqStable(\mforall{}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

((D  0  THENA  Auto)  THEN  GenConclAtAddr  [1;2;2;1;1]\mcdot{})

---

Home Index