---

Step * of Lemma consensus-reachable

∀[V:Type]
  ((∀v1,v2:V.  Dec(v1 = v2 ∈ V))
  ⇒ {∃v,v':V. (¬(v = v' ∈ V))}
  ⇒ (∀A:Id List. ∀W:{a:Id| (a ∈ A)}  List List.
        (three-intersection(A;W)
        ⇒ (∀ws∈W.∀x:ts-reachable(consensus-ts4(V;A;W))
                    ∃y:ConsensusState
                     ((x ((λx,y. CR(in ws)[x, y] )^*) y) ∧ (∃v:V. ∃i:ℤ. in state y, inning i has committed v))))))
BY
{ (Auto
   THEN (FLemma `three-intersection-two-intersection` [-1] THENA Auto)
   THEN (FLemma `two-intersection-one-intersection` [-1] THENA Auto)
   THEN (BLemma `l_all_iff` THEN Auto)
   THEN (Assert ∃a:{a:Id| (a ∈ A)} . (a ∈ ws) BY
               OnMaybeHyp 8 (\h. ((RepUR ``one-intersection`` h THEN (RWO "l_all_iff" h THENA Auto))
                                  THEN InstHyp [⌈ws⌉] h⋅
                                  THEN Complete (Auto))))⋅
   THEN (Assert 0 < ||ws|| BY
               (ExRepD THEN DVar `ws' THEN Reduce 0 THEN Auto' THEN AutoSimpHyp Auto (-1)))⋅) }

1
1. [V] : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(v = v' ∈ V))}@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)}  List List@i
6. three-intersection(A;W)@i
7. two-intersection(A;W)
8. one-intersection(A;W)
9. ws : {a:Id| (a ∈ A)}  List@i
10. (ws ∈ W)@i
11. x@0 : ts-reachable(consensus-ts4(V;A;W))@i
12. ∃a:{a:Id| (a ∈ A)} . (a ∈ ws)
13. 0 < ||ws||
⊢ ∃y:ConsensusState. ((x@0 ((λx@0,y. CR(in ws)[x@0, y] )^*) y) ∧ (∃v:V. ∃i:ℤ. in state y, inning i has committed v))

---

Latex:


\mforall{}[V:Type]
    ((\mforall{}v1,v2:V.    Dec(v1  =  v2))
    {}\mRightarrow{}  \{\mexists{}v,v':V.  (\mneg{}(v  =  v'))\}
    {}\mRightarrow{}  (\mforall{}A:Id  List.  \mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List.
                (three-intersection(A;W)
                {}\mRightarrow{}  (\mforall{}ws\mmember{}W.\mforall{}x:ts-reachable(consensus-ts4(V;A;W))
                                        \mexists{}y:ConsensusState
                                          ((x  rel\_star(ConsensusState;  \mlambda{}x,y.  CR(in  ws)[x,  y]  )  y)
                                          \mwedge{}  (\mexists{}v:V.  \mexists{}i:\mBbbZ{}.  in  state  y,  inning  i  has  committed  v))))))


By

(Auto
  THEN  (FLemma  `three-intersection-two-intersection`  [-1]  THENA  Auto)
  THEN  (FLemma  `two-intersection-one-intersection`  [-1]  THENA  Auto)
  THEN  (BLemma  `l\_all\_iff`  THEN  Auto)
  THEN  (Assert  \mexists{}a:\{a:Id|  (a  \mmember{}  A)\}  .  (a  \mmember{}  ws)  BY
                          OnMaybeHyp  8  (\mbackslash{}h.  ((RepUR  ``one-intersection``  h  THEN  (RWO  "l\_all\_iff"  h  THENA  Auto))
                                                                THEN  InstHyp  [\mkleeneopen{}ws\mkleeneclose{}]  h\mcdot{}
                                                                THEN  Complete  (Auto))))\mcdot{}
  THEN  (Assert  0  <  ||ws||  BY
                          (ExRepD  THEN  DVar  `ws'  THEN  Reduce  0  THEN  Auto'  THEN  AutoSimpHyp  Auto  (-1)))\mcdot{})

---

Home Index