---

Step * 1 of Lemma decidable__cs-archived


1. [V] : Type
2. A : Id List@i
3. s : ConsensusState@i
4. a : {a:Id| (a ∈ A)} @i
5. i : ℤ@i
6. v : V@i
7. ∀v,v':V.  Dec(v = v' ∈ V)@i
⊢ Dec((i ∈ fpf-domain(Estimate(s;a))) ∧ (Estimate(s;a)(i) = v ∈ V))
BY
{ ((Unfold `and` 0 THEN Fold `cand` 0)
   THEN (InstLemma `decidable__cand` [⌈(i ∈ fpf-domain(Estimate(s;a)))⌉]⋅ THENA Auto)
   THEN BHyp -1 
   THEN Auto) }

---

Latex:



1.  [V]  :  Type
2.  A  :  Id  List@i
3.  s  :  ConsensusState@i
4.  a  :  \{a:Id|  (a  \mmember{}  A)\}  @i
5.  i  :  \mBbbZ{}@i
6.  v  :  V@i
7.  \mforall{}v,v':V.    Dec(v  =  v')@i
\mvdash{}  Dec((i  \mmember{}  fpf-domain(Estimate(s;a)))  \mwedge{}  (Estimate(s;a)(i)  =  v))


By

((Unfold  `and`  0  THEN  Fold  `cand`  0)
  THEN  (InstLemma  `decidable\_\_cand`  [\mkleeneopen{}(i  \mmember{}  fpf-domain(Estimate(s;a)))\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BHyp  -1 
  THEN  Auto)

---

Home Index