---

Step * 1 1 1 of Lemma fresh-inning-reachable


1. V : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. ws : {a:Id| (a ∈ A)}  List@i
5. x : ConsensusState@i
6. i : ℤ@i
7. (ws ∈ W)@i
8. (∀a∈ws.Inning(x;a) < i)
⊢ x = (λa.<Inning(x;a), Estimate(x;a)>) ∈ ({a:Id| (a ∈ A)}  ⟶ (ℤ × j:ℤ fp-> V))
BY
{ (All (RepUR ``ts-type ts-rel ts-init consensus-ts4 consensus-state4``)
   THEN Ext
   THEN Reduce 0
   THEN Auto
   THEN All (Unfolds ``cs-inning cs-estimate``)
   THEN Auto
   THEN GenConclAtAddr [2]
   THEN D -2
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  V  :  Type
2.  A  :  Id  List@i
3.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
4.  ws  :  \{a:Id|  (a  \mmember{}  A)\}    List@i
5.  x  :  ConsensusState@i
6.  i  :  \mBbbZ{}@i
7.  (ws  \mmember{}  W)@i
8.  (\mforall{}a\mmember{}ws.Inning(x;a)  <  i)
\mvdash{}  x  =  (\mlambda{}a.<Inning(x;a),  Estimate(x;a)>)


By

---

Latex:
(All  (RepUR  ``ts-type  ts-rel  ts-init  consensus-ts4  consensus-state4``)
  THEN  Ext
  THEN  Reduce  0
  THEN  Auto
  THEN  All  (Unfolds  ``cs-inning  cs-estimate``)
  THEN  Auto
  THEN  GenConclAtAddr  [2]
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto)

---

Home Index