---

Step * of Lemma decidable__cs-precondition

∀[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. ∀s:ConsensusState. ∀i:ℤ. ∀v:V.
        Dec(state s may consider v in inning i)))
BY
{ (Auto
   THEN Unfold `cs-precondition` 0
   THEN (Assert Dec((∃ws∈W. (∀b∈ws.i ≤ Inning(s;b))
               ∧ (∀ws'∈W.¬in state s, ws' blocks ws from archiving v in inning i))) BY
               ((ProveDecidable1 THENA Auto)
                THEN DoSubsume
                THEN Auto
                THEN Unfold `consensus-state4` 0
                THEN SubtypeReasoning
                THEN Auto
                THEN RepeatFor 2 (D -1)
                THEN HypSubst' -1 0
                THEN GenConclAtAddr [1]
                THEN Auto))) }

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. s : ConsensusState@i
7. i : ℤ@i
8. v : V@i
9. Dec((∃ws∈W. (∀b∈ws.i ≤ Inning(s;b)) ∧ (∀ws'∈W.¬in state s, ws' blocks ws from archiving v in inning i)))
⊢ Dec(∃ws:{a:Id| (a ∈ A)}  List
       ((ws ∈ W)
       ∧ (∀b:{a:Id| (a ∈ A)} . ((b ∈ ws) ⇒ (i ≤ Inning(s;b))))
       ∧ (∀ws':{a:Id| (a ∈ A)}  List. ((ws' ∈ W) ⇒ (¬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{}s:ConsensusState.  \mforall{}i:\mBbbZ{}.  \mforall{}v:V.
                Dec(state  s  may  consider  v  in  inning  i)))


By

(Auto
  THEN  Unfold  `cs-precondition`  0
  THEN  (Assert  Dec((\mexists{}ws\mmember{}W.  (\mforall{}b\mmember{}ws.i  \mleq{}  Inning(s;b))
                          \mwedge{}  (\mforall{}ws'\mmember{}W.\mneg{}in  state  s,  ws'  blocks  ws  from  archiving  v  in  inning  i)))  BY
                          ((ProveDecidable1  THENA  Auto)
                            THEN  DoSubsume
                            THEN  Auto
                            THEN  Unfold  `consensus-state4`  0
                            THEN  SubtypeReasoning
                            THEN  Auto
                            THEN  RepeatFor  2  (D  -1)
                            THEN  HypSubst'  -1  0
                            THEN  GenConclAtAddr  [1]
                            THEN  Auto)))

---

Home Index