---

Step * of Lemma cs-inning-committed-single

∀[V:Type]. ∀[A:Id List]. ∀[W:{a:Id| (a ∈ A)}  List List]. ∀[s:ConsensusState]. ∀[i:ℤ]. ∀[v,v2:V].
  (v = v2 ∈ V) supposing 
     (in state s, inning i has committed v2 and 
     in state s, inning i could commit v  and 
     two-intersection(A;W))
BY
{ (Auto THEN D -2 THEN D -1 THEN ExRepD) }

1
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

---

Latex:

---

Latex:
\mforall{}[V:Type].  \mforall{}[A:Id  List].  \mforall{}[W:\{a:Id|  (a  \mmember{}  A)\}    List  List].  \mforall{}[s:ConsensusState].  \mforall{}[i:\mBbbZ{}].  \mforall{}[v,v2:V].
    (v  =  v2)  supposing 
          (in  state  s,  inning  i  has  committed  v2  and 
          in  state  s,  inning  i  could  commit  v    and 
          two-intersection(A;W))


By

---

Latex:
(Auto  THEN  D  -2  THEN  D  -1  THEN  ExRepD)

---

Home Index