---

Step * 1 of Lemma cs-inning-committed-single


1. V : Type
2. A : Id List
3. W : {a:Id| (a ∈ A)}  List List
4. s : ConsensusState
5. i : ℤ
6. v : V
7. v2 : V
8. two-intersection(A;W)
9. ws : {a:Id| (a ∈ A)}  List
10. (ws ∈ W)
11. ∀a:{a:Id| (a ∈ A)} . ((a ∈ ws) ⇒ (by state s, a archived v in inning i ∨ in state s, a has not completed inning i))
12. w1 : {a:Id| (a ∈ A)}  List
13. (w1 ∈ W)
14. ∀a:{a:Id| (a ∈ A)} . ((a ∈ w1) ⇒ by state s, a archived v2 in inning i)
⊢ v = v2 ∈ V
BY
{ OnMaybeHyp 8 (\h. (Unfold `two-intersection` h
                     THEN (RWW "l_all_iff" h THENA Auto)
                     THEN (InstHyp [⌈ws⌉;⌈w1⌉] h⋅ THENA Auto)
                     THEN ExRepD
                     THEN (Assert by state s, a archived v in inning i ∨ in state s, a has not completed inning i BY
                                 Auto)
                     THEN (Assert by state s, a archived v2 in inning i BY
                                 Auto)
                     THEN (D -2 THEN D -1)
                     THEN Auto
                     THEN D -3
                     THEN Auto)) }

---

Latex:



1.  V  :  Type
2.  A  :  Id  List
3.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List
4.  s  :  ConsensusState
5.  i  :  \mBbbZ{}
6.  v  :  V
7.  v2  :  V
8.  two-intersection(A;W)
9.  ws  :  \{a:Id|  (a  \mmember{}  A)\}    List
10.  (ws  \mmember{}  W)
11.  \mforall{}a:\{a:Id|  (a  \mmember{}  A)\} 
            ((a  \mmember{}  ws)
            {}\mRightarrow{}  (by  state  s,  a  archived  v  in  inning  i  \mvee{}  in  state  s,  a  has  not  completed  inning  i))
12.  w1  :  \{a:Id|  (a  \mmember{}  A)\}    List
13.  (w1  \mmember{}  W)
14.  \mforall{}a:\{a:Id|  (a  \mmember{}  A)\}  .  ((a  \mmember{}  w1)  {}\mRightarrow{}  by  state  s,  a  archived  v2  in  inning  i)
\mvdash{}  v  =  v2


By

OnMaybeHyp  8  (\mbackslash{}h.  (Unfold  `two-intersection`  h
                                      THEN  (RWW  "l\_all\_iff"  h  THENA  Auto)
                                      THEN  (InstHyp  [\mkleeneopen{}ws\mkleeneclose{};\mkleeneopen{}w1\mkleeneclose{}]  h\mcdot{}  THENA  Auto)
                                      THEN  ExRepD
                                      THEN  (Assert  by  state  s,  a  archived  v  in  inning  i
                                                              \mvee{}  in  state  s,  a  has  not  completed  inning  i  BY
                                                              Auto)
                                      THEN  (Assert  by  state  s,  a  archived  v2  in  inning  i  BY
                                                              Auto)
                                      THEN  (D  -2  THEN  D  -1)
                                      THEN  Auto
                                      THEN  D  -3
                                      THEN  Auto))

---

Home Index