---

Step * 1 2 1 1 1 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. 0 < i
15. 0 ≤ 0
16. 0 < i
⊢ ∃v':V
   ((¬(v' = v ∈ V))
   ∧ (∀b:{a:Id| (a ∈ A)} 
        (((b ∈ ws) ∧ (b ∈ ws'))
        ⇒ ((↑0 ∈ dom(Estimate(s;b)))
           ∧ (Estimate(s;b)(0) = v' ∈ V)
           ∧ (∀k:ℤ. (((0 < k ∧ k < i) ∧ (↑k ∈ dom(Estimate(s;b)))) ⇒ (Estimate(s;b)(k) = v' ∈ V)))))))
BY
{ (Assert ∃v':V. (¬(v' = v ∈ V)) BY
         (ExRepD
          THEN ((Decide v1 = v ∈ V THENA Auto) THENL [InstConcl [⌈v'⌉]⋅; InstConcl [⌈v1⌉]⋅])
          THEN Auto
          THEN D 0
          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. 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. 0 < i
15. 0 ≤ 0
16. 0 < i
17. ∃v':V. (¬(v' = v ∈ V))
⊢ ∃v':V
   ((¬(v' = v ∈ V))
   ∧ (∀b:{a:Id| (a ∈ A)} 
        (((b ∈ ws) ∧ (b ∈ ws'))
        ⇒ ((↑0 ∈ dom(Estimate(s;b)))
           ∧ (Estimate(s;b)(0) = v' ∈ V)
           ∧ (∀k:ℤ. (((0 < k ∧ k < i) ∧ (↑k ∈ dom(Estimate(s;b)))) ⇒ (Estimate(s;b)(k) = v' ∈ V)))))))

---

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.  \mneg{}(\mexists{}b\mmember{}ws.  (b  \mmember{}  ws'))
14.  0  <  i
15.  0  \mleq{}  0
16.  0  <  i
\mvdash{}  \mexists{}v':V
      ((\mneg{}(v'  =  v))
      \mwedge{}  (\mforall{}b:\{a:Id|  (a  \mmember{}  A)\} 
                (((b  \mmember{}  ws)  \mwedge{}  (b  \mmember{}  ws'))
                {}\mRightarrow{}  ((\muparrow{}0  \mmember{}  dom(Estimate(s;b)))
                      \mwedge{}  (Estimate(s;b)(0)  =  v')
                      \mwedge{}  (\mforall{}k:\mBbbZ{}.  (((0  <  k  \mwedge{}  k  <  i)  \mwedge{}  (\muparrow{}k  \mmember{}  dom(Estimate(s;b))))  {}\mRightarrow{}  (Estimate(s;b)(k)  =  v')))))))


By

(Assert  \mexists{}v':V.  (\mneg{}(v'  =  v))  BY
              (ExRepD
                THEN  ((Decide  v1  =  v  THENA  Auto)  THENL  [InstConcl  [\mkleeneopen{}v'\mkleeneclose{}]\mcdot{};  InstConcl  [\mkleeneopen{}v1\mkleeneclose{}]\mcdot{}])
                THEN  Auto
                THEN  D  0
                THEN  Auto))

---

Home Index