---

Step * 1 1 1 of Lemma decidable__cs-precondition


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)))
10. ∀L:{a:Id| (a ∈ A)}  List List
      ∀[P:{x:{a:Id| (a ∈ A)}  List| (x ∈ L)}  ─→ ℙ]. ((∃x∈L. P[x]) ⇐⇒ ∃x:{a:Id| (a ∈ A)}  List. ((x ∈ L) ∧ P[x]))
⊢ (∃ws∈W. (∀b∈ws.i ≤ Inning(s;b)) ∧ (∀ws'∈W.¬in state s, ws' blocks ws from archiving v in inning i))
⇐⇒ ∃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))))
BY
{ (RWO "l_all_iff<" 0 THEN Auto)⋅ }

---

Latex:



1.  [V]  :  Type
2.  \mforall{}v1,v2:V.    Dec(v1  =  v2)@i
3.  \mexists{}v,v':V.  (\mneg{}(v  =  v'))@i
4.  A  :  Id  List@i
5.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
6.  s  :  ConsensusState@i
7.  i  :  \mBbbZ{}@i
8.  v  :  V@i
9.  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)))
10.  \mforall{}L:\{a:Id|  (a  \mmember{}  A)\}    List  List
            \mforall{}[P:\{x:\{a:Id|  (a  \mmember{}  A)\}    List|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbP{}]
                ((\mexists{}x\mmember{}L.  P[x])  \mLeftarrow{}{}\mRightarrow{}  \mexists{}x:\{a:Id|  (a  \mmember{}  A)\}    List.  ((x  \mmember{}  L)  \mwedge{}  P[x]))
\mvdash{}  (\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))
\mLeftarrow{}{}\mRightarrow{}  \mexists{}ws:\{a:Id|  (a  \mmember{}  A)\}    List
          ((ws  \mmember{}  W)
          \mwedge{}  (\mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  ((b  \mmember{}  ws)  {}\mRightarrow{}  (i  \mleq{}  Inning(s;b))))
          \mwedge{}  (\mforall{}ws':\{a:Id|  (a  \mmember{}  A)\}    List
                    ((ws'  \mmember{}  W)  {}\mRightarrow{}  (\mneg{}in  state  s,  ws'  blocks  ws  from  archiving  v  in  inning  i))))


By

(RWO  "l\_all\_iff<"  0  THEN  Auto)\mcdot{}

---

Home Index