---

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


1. [V] : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
⊢ ∀x:ts-reachable(consensus-ts5(V;A;W))
    SqStable(let x1,x2 = x 
             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
{ ((D 0 THENA Auto) THEN D -1 THEN Thin (-1) THEN RepUR ``ts-type consensus-ts5`` -1 THEN D -1 THEN Reduce 0) }

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
⊢ SqStable(∀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)))

---

Latex:



1.  [V]  :  Type
2.  A  :  Id  List@i
3.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
\mvdash{}  \mforall{}x:ts-reachable(consensus-ts5(V;A;W))
        SqStable(let  x1,x2  =  x 
                          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

((D  0  THENA  Auto)
  THEN  D  -1
  THEN  Thin  (-1)
  THEN  RepUR  ``ts-type  consensus-ts5``  -1
  THEN  D  -1
  THEN  Reduce  0)

---

Home Index