---

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

.....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
BY
{ (InstLemma `consensus-ts4-inning-committed-stable` [⌈V⌉;⌈A⌉;⌈W⌉;⌈v2⌉;⌈i⌉]⋅ THENA Auto) }

1
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
17. ts-stable(consensus-ts4(V;A;W);s.in state s, inning i has committed v2)
⊢ in state s2, inning i has committed v2

---

Latex:


.....antecedent..... 
1.  V  :  Type
2.  A  :  Id  List
3.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List
4.  \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))
5.  s  :  ConsensusState
6.  s2  :  ConsensusState
7.  \mforall{}[i:\mBbbZ{}].  \mforall{}[v,v2:V].
          (v  =  v2)  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  :  \mBbbZ{}
10.  \mforall{}[v,v2:V].
            (v  =  v2)  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.  \mforall{}[v2:V]
            (v  =  v2)  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
\mvdash{}  in  state  s2,  inning  i  has  committed  v2


By

(InstLemma  `consensus-ts4-inning-committed-stable`  [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}W\mkleeneclose{};\mkleeneopen{}v2\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index