---

Step * 1 1 1 1 of Lemma consensus-ts4-archived-invariant

.....antecedent..... 
1. V : Type@i'
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. A : Id List@i
4. W : {a:Id| (a ∈ A)}  List List@i
5. x : ConsensusState@i
6. (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) x@i
7. y : ConsensusState@i
8. (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) y@i
9. ∀i:ℤ. ∀v:V. ∀a:{a:Id| (a ∈ A)} .
     (by state x, a archived v in inning i
     ⇒ (∀j:ℕi. ∀v':V.  (in state x, inning j could commit v'  ⇒ (v' = v ∈ V))))@i
10. CR[x,y]@i
11. i : ℤ@i
12. v : V@i
13. a : {a:Id| (a ∈ A)} @i
14. by state y, a archived v in inning i@i
15. j : ℕi@i
16. v' : V@i
17. in state y, inning j could commit v' @i
18. by state x, a archived v in inning i
⊢ in state x, inning j could commit v' 
BY
{ (InstLemma `cs-inning-committable-step` [⌈V⌉;⌈A⌉;⌈W⌉;⌈x⌉;⌈y⌉;⌈j⌉;⌈v'⌉]⋅
   THEN Auto
   THEN All
    (RepUR ``ts-type ts-init ts-rel consensus-ts4 ts-reachable``)⋅
   THEN Auto) }

---

Latex:


.....antecedent..... 
1.  V  :  Type@i'
2.  \mforall{}v1,v2:V.    Dec(v1  =  v2)@i
3.  A  :  Id  List@i
4.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
5.  x  :  ConsensusState@i
6.  (\mlambda{}a.<-1,  \motimes{}>)  rel\_star(ConsensusState;  \mlambda{}x,y.  CR[x,y])  x@i
7.  y  :  ConsensusState@i
8.  (\mlambda{}a.<-1,  \motimes{}>)  rel\_star(ConsensusState;  \mlambda{}x,y.  CR[x,y])  y@i
9.  \mforall{}i:\mBbbZ{}.  \mforall{}v:V.  \mforall{}a:\{a:Id|  (a  \mmember{}  A)\}  .
          (by  state  x,  a  archived  v  in  inning  i
          {}\mRightarrow{}  (\mforall{}j:\mBbbN{}i.  \mforall{}v':V.    (in  state  x,  inning  j  could  commit  v'    {}\mRightarrow{}  (v'  =  v))))@i
10.  CR[x,y]@i
11.  i  :  \mBbbZ{}@i
12.  v  :  V@i
13.  a  :  \{a:Id|  (a  \mmember{}  A)\}  @i
14.  by  state  y,  a  archived  v  in  inning  i@i
15.  j  :  \mBbbN{}i@i
16.  v'  :  V@i
17.  in  state  y,  inning  j  could  commit  v'  @i
18.  by  state  x,  a  archived  v  in  inning  i
\mvdash{}  in  state  x,  inning  j  could  commit  v' 


By

(InstLemma  `cs-inning-committable-step`  [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}W\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}v'\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  All
    (RepUR  ``ts-type  ts-init  ts-rel  consensus-ts4  ts-reachable``)\mcdot{}
  THEN  Auto)

---

Home Index