---

Step * 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)))
⊢ 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)))))
BY
{ Assert ⌈(∃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))))\000C⌉
⋅ }

1
.....assertion..... 
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)))
⊢ (∃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))))

2
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. (∃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))))
⊢ 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:



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)))
\mvdash{}  Dec(\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

Assert  \mkleeneopen{}(\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))))\mkleeneclose{}\mcdot{}

---

Home Index