---

Step * of Lemma decidable__cs-archive-blocked

∀[V:Type]
  ((∀v1,v2:V.  Dec(v1 = v2 ∈ V))
  ⇒ (∃v,v':V. (¬(v = v' ∈ V)))
  ⇒ (∀A:Id List. ∀W:{a:Id| (a ∈ A)}  List List. ∀ws,ws':{a:Id| (a ∈ A)}  List. ∀s:ConsensusState. ∀i:ℤ. ∀v:V.
        Dec(in state s, ws' blocks ws from archiving v in inning i)))
BY
{ (Auto THEN (InstLemma `cs-archived-listable` [⌈V⌉;⌈A⌉;⌈s⌉]⋅ THENA Auto) THEN D -1) }

1
1. [V] : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. ∃v,v':V. (¬(v = v' ∈ V))@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)}  List List@i
6. ws : {a:Id| (a ∈ A)}  List@i
7. ws' : {a:Id| (a ∈ A)}  List@i
8. s : ConsensusState@i
9. i : ℤ@i
10. v : V@i
11. L : V List
12. ∀b:{a:Id| (a ∈ A)} . ∀v:V. ∀j:ℤ.  ((v ∈ L)) supposing ((Estimate(s;b)(j) = v ∈ V) and (↑j ∈ dom(Estimate(s;b))))
⊢ Dec(in state s, ws' blocks ws from archiving v in inning i)

---

Latex:


\mforall{}[V:Type]
    ((\mforall{}v1,v2:V.    Dec(v1  =  v2))
    {}\mRightarrow{}  (\mexists{}v,v':V.  (\mneg{}(v  =  v')))
    {}\mRightarrow{}  (\mforall{}A:Id  List.  \mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List.  \mforall{}ws,ws':\{a:Id|  (a  \mmember{}  A)\}    List.  \mforall{}s:ConsensusState.
            \mforall{}i:\mBbbZ{}.  \mforall{}v:V.
                Dec(in  state  s,  ws'  blocks  ws  from  archiving  v  in  inning  i)))


By

(Auto  THEN  (InstLemma  `cs-archived-listable`  [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1)

---

Home Index