---

Step * 3 1 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. ∀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
BY
{ ((RWO "append-nil" (-2) THENA Auto)
   THEN BLemma `rel_star_weakening`
   THEN Auto
   THEN Symmetry⋅
   THEN RepUR ``ts-type consensus-ts6 consensus-state6`` 0
   THEN (Ext THENA Auto)
   THEN Decide x1 = a ∈ Id
   THEN Auto) }

---

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{}v:V.  \mforall{}j:\mBbbN{}0.
          let  i,est,knw  =  consensus-accum-state(A;(x  a)  @  [])  in 
          (\mneg{}(i  \mmember{}  fpf-domain(est)))  \mwedge{}  may  consider  v  in  inning  i  based  on  knowledge  (knw) 
          supposing  \mbot{}  =  Archive(v)@i
\mvdash{}  x  rel\_star(ts-type(consensus-ts6(V;A;W));  ts-rel(consensus-ts6(V;A;W)))  y


By

((RWO  "append-nil"  (-2)  THENA  Auto)
  THEN  BLemma  `rel\_star\_weakening`
  THEN  Auto
  THEN  Symmetry\mcdot{}
  THEN  RepUR  ``ts-type  consensus-ts6  consensus-state6``  0
  THEN  (Ext  THENA  Auto)
  THEN  Decide  x1  =  a
  THEN  Auto)

---

Home Index