---

Step * 4 4 of Lemma consensus-ts6-reachability1

.....wf..... 
1. V : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. ys : consensus-event(V;A) List@i
5. y : consensus-event(V;A)@i
⊢ ∀x,y:{a:Id| (a ∈ A)}  ─→ (consensus-event(V;A) List). ∀a:{a:Id| (a ∈ A)} .
    ((∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀z:ℕi × V?.
        ((consensus-message(b;i;z) ∈ ys)
        ⇒ 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))
       ⇒ (∀v:V. ∀j:ℕ||ys||.
             let i,est,knw = consensus-accum-state(A;(x a) @ firstn(j;ys)) in 
             (¬(i ∈ fpf-domain(est))) ∧ may consider v in inning i based on knowledge (knw) 
             supposing ys[j] = Archive(v) ∈ consensus-event(V;A))
       ⇒ (x (ts-rel(consensus-ts6(V;A;W))^*) y)) supposing 
       (((y a) = ((x a) @ ys) ∈ (consensus-event(V;A) List)) and 
       (∀b:{a:Id| (a ∈ A)} . (y b) = (x b) ∈ (consensus-event(V;A) List) supposing ¬(b = a ∈ Id))) ∈ ℙ
BY
{ (Auto
   THEN GenConclAtAddr [2;1]
   THEN RepeatFor 2 (D -2)
   THEN Reduce 0
   THEN DVar `z'
   THEN Reduce 0
   THEN (Try ((DVar `x1' THEN DVar `x2')) THEN Reduce 0)
   THEN Auto)⋅ }

---

Latex:


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


By

(Auto
  THEN  GenConclAtAddr  [2;1]
  THEN  RepeatFor  2  (D  -2)
  THEN  Reduce  0
  THEN  DVar  `z'
  THEN  Reduce  0
  THEN  (Try  ((DVar  `x1'  THEN  DVar  `x2'))  THEN  Reduce  0)
  THEN  Auto)\mcdot{}

---

Home Index