---

Step * 2 2 1 of Lemma consensus-refinement4


1. [V] : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. 1 < ||W||@i
5. two-intersection(A;W)@i
⊢ ∀x:ts-reachable(consensus-ts4(V;A;W))
    ((ts-final(consensus-ts4(V;A;W)) x)
    ⇒ (∃y:ts-reachable(consensus-ts5(V;A;W))
         ((ts-final(consensus-ts5(V;A;W)) y) ∧ (((λs.(fst(s))) y) = x ∈ ts-type(consensus-ts4(V;A;W))))))
BY
{ (Auto
   THEN D -2
   THEN RepUR ``ts-type consensus-ts4`` -3
   THEN RepUR ``ts-final consensus-ts4`` -1
   THEN Reduce 0
   THEN ExRepD) }

1
1. [V] : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. 1 < ||W||@i
5. two-intersection(A;W)@i
6. x : ConsensusState@i
7. \\%6 : ts-init(consensus-ts4(V;A;W)) (ts-rel(consensus-ts4(V;A;W))^*) x@i
8. v : V@i
9. ∀a:{a:Id| (a ∈ A)} . ((Inning(x;a) = 0 ∈ ℤ) ∧ (Estimate(x;a) = 0 : v ∈ i:ℤ fp-> V))@i
⊢ ∃y:ts-reachable(consensus-ts5(V;A;W))
   ((ts-final(consensus-ts5(V;A;W)) y) ∧ ((fst(y)) = x ∈ ts-type(consensus-ts4(V;A;W))))

---

Latex:



1.  [V]  :  Type
2.  A  :  Id  List@i
3.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
4.  1  <  ||W||@i
5.  two-intersection(A;W)@i
\mvdash{}  \mforall{}x:ts-reachable(consensus-ts4(V;A;W))
        ((ts-final(consensus-ts4(V;A;W))  x)
        {}\mRightarrow{}  (\mexists{}y:ts-reachable(consensus-ts5(V;A;W))
                  ((ts-final(consensus-ts5(V;A;W))  y)  \mwedge{}  (((\mlambda{}s.(fst(s)))  y)  =  x))))


By

(Auto
  THEN  D  -2
  THEN  RepUR  ``ts-type  consensus-ts4``  -3
  THEN  RepUR  ``ts-final  consensus-ts4``  -1
  THEN  Reduce  0
  THEN  ExRepD)

---

Home Index