---

Step * 1 of Lemma consensus-ts4-estimate-rel


1. V : Type
2. A : Id List
3. W : {a:Id| (a ∈ A)}  List List
4. a : {a:Id| (a ∈ A)} 
5. a@0 : ConsensusState@i
6. b : ConsensusState@i
7. c : ConsensusState@i
8. Estimate(a@0;a) ⊆ Estimate(b;a)@i
9. Estimate(b;a) ⊆ Estimate(c;a)@i
⊢ Estimate(a@0;a) ⊆ Estimate(c;a)
BY
{ (Using [`g',⌈Estimate(b;a)⌉] (BLemma `fpf-sub_transitivity`)⋅ THEN Auto) }

---

Latex:



1.  V  :  Type
2.  A  :  Id  List
3.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List
4.  a  :  \{a:Id|  (a  \mmember{}  A)\} 
5.  a@0  :  ConsensusState@i
6.  b  :  ConsensusState@i
7.  c  :  ConsensusState@i
8.  Estimate(a@0;a)  \msubseteq{}  Estimate(b;a)@i
9.  Estimate(b;a)  \msubseteq{}  Estimate(c;a)@i
\mvdash{}  Estimate(a@0;a)  \msubseteq{}  Estimate(c;a)


By

(Using  [`g',\mkleeneopen{}Estimate(b;a)\mkleeneclose{}]  (BLemma  `fpf-sub\_transitivity`)\mcdot{}  THEN  Auto)

---

Home Index