---

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


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

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. \\%1 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <x1, x2>@i
7. y1 : ConsensusState@i
8. y2 : Knowledge(ConsensusState)@i
9. \\%2 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <y1, y2>@i
10. ∀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))@i
11. <x1, x2> ts-rel(consensus-ts5(V;A;W)) <y1, y2>@i
⊢ ∀a,b:{a:Id| (a ∈ A)} .
    let I,z = Knowledge(y2;a)(b) 
    in (I ≤ Inning(y1;b))
       ∧ case z
          of inl(p) =>
          let k,v = p 
          in k < I
             ∧ (↑k ∈ dom(Estimate(y1;b)))
             ∧ (Estimate(y1;b)(k) = v ∈ V)
             ∧ (∀i:ℤ. ¬↑i ∈ dom(Estimate(y1;b)) supposing k < i ∧ i < I)
          | inr(p) =>
          ∀i:ℤ. ¬↑i ∈ dom(Estimate(y1;b)) supposing i < I 
    supposing ↑b ∈ dom(Knowledge(y2;a))

---

Latex:



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

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

---

Home Index