---

Step * of Lemma consensus-ts5-true-knowledge

∀[V:Type]
  ∀A:Id List. ∀W:{a:Id| (a ∈ A)}  List List. ∀x: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))
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN (BLemma `ts-reachable-induction`  THENA (RepeatFor 2 (Auto) THEN RepUR ``ts-type consensus-ts5`` -2 THEN Auto))
   ) }

1
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)))

2
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))

3
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)))

---

Latex:


\mforall{}[V:Type]
    \mforall{}A:Id  List.  \mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List.  \mforall{}x: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))


By

(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  (BLemma  `ts-reachable-induction` 
              THENA  (RepeatFor  2  (Auto)  THEN  RepUR  ``ts-type  consensus-ts5``  -2  THEN  Auto)
              )
  )

---

Home Index