---

Step * 3 1 of Lemma consensus-ts6-reachability1


1. [V] : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. x : {a:Id| (a ∈ A)}  ─→ (consensus-event(V;A) List)@i
5. y : {a:Id| (a ∈ A)}  ─→ (consensus-event(V;A) List)@i
6. a : {a:Id| (a ∈ A)} @i
7. ∀b:{a:Id| (a ∈ A)} . (y b) = (x b) ∈ (consensus-event(V;A) List) supposing ¬(b = a ∈ Id)
8. (y a) = ((x a) @ []) ∈ (consensus-event(V;A) List)
9. ∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀z:ℕi × V?.
     ((consensus-message(b;i;z) ∈ [])
     ⇒ let i',est,knw = consensus-accum-state(A;x b) in 
        (i ≤ i')
        ∧ case z
           of inl(p) =>
           let j,v = p 
           in (↑j ∈ dom(est)) ∧ (∀k:ℤ. (¬↑k ∈ dom(est)) supposing (k < i and j < k)) ∧ (v = est(j) ∈ V)
           | inr(a) =>
           ∀j:ℤ. ¬↑j ∈ dom(est) supposing j < i)@i
10. ∀v:V. ∀j:ℕ||[]||.
      let i,est,knw = consensus-accum-state(A;(x a) @ firstn(j;[])) in 
      (¬(i ∈ fpf-domain(est))) ∧ may consider v in inning i based on knowledge (knw) 
      supposing [][j] = Archive(v) ∈ consensus-event(V;A)@i
⊢ x (ts-rel(consensus-ts6(V;A;W))^*) y
BY
{ (Thin (-2) THEN Reduce (-1)) }

1
1. [V] : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. x : {a:Id| (a ∈ A)}  ─→ (consensus-event(V;A) List)@i
5. y : {a:Id| (a ∈ A)}  ─→ (consensus-event(V;A) List)@i
6. a : {a:Id| (a ∈ A)} @i
7. ∀b:{a:Id| (a ∈ A)} . (y b) = (x b) ∈ (consensus-event(V;A) List) supposing ¬(b = a ∈ Id)
8. (y a) = ((x a) @ []) ∈ (consensus-event(V;A) List)
9. ∀v:V. ∀j:ℕ0.
     let i,est,knw = consensus-accum-state(A;(x a) @ []) in 
     (¬(i ∈ fpf-domain(est))) ∧ may consider v in inning i based on knowledge (knw) 
     supposing ⊥ = Archive(v) ∈ consensus-event(V;A)@i
⊢ x (ts-rel(consensus-ts6(V;A;W))^*) y

---

Latex:



1.  [V]  :  Type
2.  A  :  Id  List@i
3.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
4.  x  :  \{a:Id|  (a  \mmember{}  A)\}    {}\mrightarrow{}  (consensus-event(V;A)  List)@i
5.  y  :  \{a:Id|  (a  \mmember{}  A)\}    {}\mrightarrow{}  (consensus-event(V;A)  List)@i
6.  a  :  \{a:Id|  (a  \mmember{}  A)\}  @i
7.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  (y  b)  =  (x  b)  supposing  \mneg{}(b  =  a)
8.  (y  a)  =  ((x  a)  @  [])
9.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}i:\mBbbN{}.  \mforall{}z:\mBbbN{}i  \mtimes{}  V?.
          ((consensus-message(b;i;z)  \mmember{}  [])
          {}\mRightarrow{}  let  i',est,knw  =  consensus-accum-state(A;x  b)  in 
                (i  \mleq{}  i')
                \mwedge{}  case  z
                      of  inl(p)  =>
                      let  j,v  =  p 
                      in  (\muparrow{}j  \mmember{}  dom(est))  \mwedge{}  (\mforall{}k:\mBbbZ{}.  (\mneg{}\muparrow{}k  \mmember{}  dom(est))  supposing  (k  <  i  and  j  <  k))  \mwedge{}  (v  =  est(j))
                      |  inr(a)  =>
                      \mforall{}j:\mBbbZ{}.  \mneg{}\muparrow{}j  \mmember{}  dom(est)  supposing  j  <  i)@i
10.  \mforall{}v:V.  \mforall{}j:\mBbbN{}||[]||.
            let  i,est,knw  =  consensus-accum-state(A;(x  a)  @  firstn(j;[]))  in 
            (\mneg{}(i  \mmember{}  fpf-domain(est)))  \mwedge{}  may  consider  v  in  inning  i  based  on  knowledge  (knw) 
            supposing  [][j]  =  Archive(v)@i
\mvdash{}  x  rel\_star(ts-type(consensus-ts6(V;A;W));  ts-rel(consensus-ts6(V;A;W)))  y


By

(Thin  (-2)  THEN  Reduce  (-1))

---

Home Index