---

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

∀[V:Type]. ∀[A:Id List]. ∀[W:{a:Id| (a ∈ A)}  List List]. ∀[s,s2:ConsensusState].
  ∀[i:ℤ]. ∀[v,v2:V].
    (v = v2 ∈ V) supposing 
       (in state s, inning i has committed v2 and 
       in state s2, inning i could commit v  and 
       two-intersection(A;W)) 
  supposing s ts-rel(consensus-ts4(V;A;W)) s2
BY
{ (InstLemma `cs-inning-committed-single` []
   THEN RepeatFor 3 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN ParallelOp -2
   THEN (D 0 THENA (Auto THEN Auto THEN RepUR ``ts-type consensus-ts4`` 0 THEN Auto))
   THEN ParallelOp -2
   THEN RepeatFor 5 (ParallelLast)) }

1
.....antecedent..... 
1. V : Type
2. A : Id List
3. W : {a:Id| (a ∈ A)}  List List
4. ∀[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))
5. s : ConsensusState
6. s2 : ConsensusState
7. ∀[i:ℤ]. ∀[v,v2:V].
     (v = v2 ∈ V) supposing 
        (in state s2, inning i has committed v2 and 
        in state s2, inning i could commit v  and 
        two-intersection(A;W))
8. s ts-rel(consensus-ts4(V;A;W)) s2
9. i : ℤ
10. ∀[v,v2:V].
      (v = v2 ∈ V) supposing 
         (in state s2, inning i has committed v2 and 
         in state s2, inning i could commit v  and 
         two-intersection(A;W))
11. v : V
12. ∀[v2:V]
      (v = v2 ∈ V) supposing 
         (in state s2, inning i has committed v2 and 
         in state s2, inning i could commit v  and 
         two-intersection(A;W))
13. v2 : V
14. two-intersection(A;W)
15. in state s2, inning i could commit v 
16. in state s, inning i has committed v2
⊢ in state s2, inning i has committed v2

---

Latex:


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


By

(InstLemma  `cs-inning-committed-single`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  ParallelOp  -2
  THEN  (D  0  THENA  (Auto  THEN  Auto  THEN  RepUR  ``ts-type  consensus-ts4``  0  THEN  Auto))
  THEN  ParallelOp  -2
  THEN  RepeatFor  5  (ParallelLast))

---

Home Index