---

Step * 1 1 2 of Lemma decidable__cs-archive-blocked


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))))
13. (∃b∈ws. (b ∈ ws'))
14. in state s, ws' blocks ws from archiving v in inning i
⇐⇒ ∃j:ℕi
     (∃v'∈L. (¬(v' = v ∈ V))
     ∧ (∀b∈ws.(b ∈ ws')
          ⇒ ((↑j ∈ dom(Estimate(s;b)))
             ∧ (Estimate(s;b)(j) = v' ∈ V)
             ∧ (∀k:{j + 1..i-}. ((↑k ∈ dom(Estimate(s;b))) ⇒ (Estimate(s;b)(k) = v' ∈ V))))))
⊢ Dec(in state s, ws' blocks ws from archiving v in inning i)
BY
{ Subst' ∃j:ℕi
          (∃v'∈L. (¬(v' = v ∈ V))
          ∧ (∀b∈ws.(b ∈ ws')
               ⇒ ((↑j ∈ dom(Estimate(s;b)))
                  ∧ (Estimate(s;b)(j) = v' ∈ V)
                  ∧ (∀k:{j + 1..i-}. ((↑k ∈ dom(Estimate(s;b))) ⇒ (Estimate(s;b)(k) = v' ∈ V)))))) 
~ ∃j:ℕi
   (∃v'∈L. (¬(v' = v ∈ V))
   ∧ (∀b∈ws.(b ∈ ws')
        ⇒ ((λv',b,j. ((↑j ∈ dom(Estimate(s;b)))
                     ∧ (Estimate(s;b)(j) = v' ∈ V)
                     ∧ (∀k:{j + 1..i-}. ((↑k ∈ dom(Estimate(s;b))) ⇒ (Estimate(s;b)(k) = v' ∈ V))))) 
            v' 
            b 
            j))) -1 }

1
.....equality..... 
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))))
13. (∃b∈ws. (b ∈ ws'))
14. in state s, ws' blocks ws from archiving v in inning i
⇐⇒ ∃j:ℕi
     (∃v'∈L. (¬(v' = v ∈ V))
     ∧ (∀b∈ws.(b ∈ ws')
          ⇒ ((↑j ∈ dom(Estimate(s;b)))
             ∧ (Estimate(s;b)(j) = v' ∈ V)
             ∧ (∀k:{j + 1..i-}. ((↑k ∈ dom(Estimate(s;b))) ⇒ (Estimate(s;b)(k) = v' ∈ V))))))
⊢ ∃j:ℕi
   (∃v'∈L. (¬(v' = v ∈ V))
   ∧ (∀b∈ws.(b ∈ ws')
        ⇒ ((↑j ∈ dom(Estimate(s;b)))
           ∧ (Estimate(s;b)(j) = v' ∈ V)
           ∧ (∀k:{j + 1..i-}. ((↑k ∈ dom(Estimate(s;b))) ⇒ (Estimate(s;b)(k) = v' ∈ V)))))) 
~ ∃j:ℕi
   (∃v'∈L. (¬(v' = v ∈ V))
   ∧ (∀b∈ws.(b ∈ ws')
        ⇒ ((λv',b,j. ((↑j ∈ dom(Estimate(s;b)))
                     ∧ (Estimate(s;b)(j) = v' ∈ V)
                     ∧ (∀k:{j + 1..i-}. ((↑k ∈ dom(Estimate(s;b))) ⇒ (Estimate(s;b)(k) = v' ∈ V))))) 
            v' 
            b 
            j)))

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. 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))))
13. (∃b∈ws. (b ∈ ws'))
14. in state s, ws' blocks ws from archiving v in inning i
⇐⇒ ∃j:ℕi
     (∃v'∈L. (¬(v' = v ∈ V))
     ∧ (∀b∈ws.(b ∈ ws')
          ⇒ ((λv',b,j. ((↑j ∈ dom(Estimate(s;b)))
                       ∧ (Estimate(s;b)(j) = v' ∈ V)
                       ∧ (∀k:{j + 1..i-}. ((↑k ∈ dom(Estimate(s;b))) ⇒ (Estimate(s;b)(k) = v' ∈ V))))) 
              v' 
              b 
              j)))
⊢ Dec(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.  ws  :  \{a:Id|  (a  \mmember{}  A)\}    List@i
7.  ws'  :  \{a:Id|  (a  \mmember{}  A)\}    List@i
8.  s  :  ConsensusState@i
9.  i  :  \mBbbZ{}@i
10.  v  :  V@i
11.  L  :  V  List
12.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}v:V.  \mforall{}j:\mBbbZ{}.
            ((v  \mmember{}  L))  supposing  ((Estimate(s;b)(j)  =  v)  and  (\muparrow{}j  \mmember{}  dom(Estimate(s;b))))
13.  (\mexists{}b\mmember{}ws.  (b  \mmember{}  ws'))
14.  in  state  s,  ws'  blocks  ws  from  archiving  v  in  inning  i
\mLeftarrow{}{}\mRightarrow{}  \mexists{}j:\mBbbN{}i
          (\mexists{}v'\mmember{}L.  (\mneg{}(v'  =  v))
          \mwedge{}  (\mforall{}b\mmember{}ws.(b  \mmember{}  ws')
                    {}\mRightarrow{}  ((\muparrow{}j  \mmember{}  dom(Estimate(s;b)))
                          \mwedge{}  (Estimate(s;b)(j)  =  v')
                          \mwedge{}  (\mforall{}k:\{j  +  1..i\msupminus{}\}.  ((\muparrow{}k  \mmember{}  dom(Estimate(s;b)))  {}\mRightarrow{}  (Estimate(s;b)(k)  =  v'))))))
\mvdash{}  Dec(in  state  s,  ws'  blocks  ws  from  archiving  v  in  inning  i)


By

Subst'  \mexists{}j:\mBbbN{}i
                (\mexists{}v'\mmember{}L.  (\mneg{}(v'  =  v))
                \mwedge{}  (\mforall{}b\mmember{}ws.(b  \mmember{}  ws')
                          {}\mRightarrow{}  ((\muparrow{}j  \mmember{}  dom(Estimate(s;b)))
                                \mwedge{}  (Estimate(s;b)(j)  =  v')
                                \mwedge{}  (\mforall{}k:\{j  +  1..i\msupminus{}\}.  ((\muparrow{}k  \mmember{}  dom(Estimate(s;b)))  {}\mRightarrow{}  (Estimate(s;b)(k)  =  v')))))) 
\msim{}  \mexists{}j:\mBbbN{}i
      (\mexists{}v'\mmember{}L.  (\mneg{}(v'  =  v))
      \mwedge{}  (\mforall{}b\mmember{}ws.(b  \mmember{}  ws')
                {}\mRightarrow{}  ((\mlambda{}v',b,j.  ((\muparrow{}j  \mmember{}  dom(Estimate(s;b)))
                                          \mwedge{}  (Estimate(s;b)(j)  =  v')
                                          \mwedge{}  (\mforall{}k:\{j  +  1..i\msupminus{}\}.  ((\muparrow{}k  \mmember{}  dom(Estimate(s;b)))  {}\mRightarrow{}  (Estimate(s;b)(k)  =  v'))))) 
                        v' 
                        b 
                        j)))  -1

---

Home Index