---

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

.....wf..... 
1. V : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. v1 : V@i
4. v2 : V@i
5. ¬(v1 = v2 ∈ V)@i
6. A : Id List@i
7. W : {a:Id| (a ∈ A)}  List List@i
8. ws : {a:Id| (a ∈ A)}  List@i
9. ws' : {a:Id| (a ∈ A)}  List@i
10. s : ConsensusState@i
11. i : ℤ@i
12. v : V@i
13. L : V List
14. ∀b:{a:Id| (a ∈ A)} . ∀v:V. ∀j:ℤ.  ((v ∈ L)) supposing ((Estimate(s;b)(j) = v ∈ V) and (↑j ∈ dom(Estimate(s;b))))
15. b : Id
16. (b ∈ ws)
17. (b ∈ ws')
18. j : ℤ@i
19. 0 ≤ j@i
20. j < i@i
21. v' : V@i
22. ¬(v' = v ∈ V)@i
23. ∀b:{a:Id| (a ∈ A)} 
      (((b ∈ ws) ∧ (b ∈ ws'))
      ⇒ ((↑j ∈ dom(Estimate(s;b)))
         ∧ (Estimate(s;b)(j) = v' ∈ V)
         ∧ (∀k:ℤ. (((j < k ∧ k < i) ∧ (↑k ∈ dom(Estimate(s;b)))) ⇒ (Estimate(s;b)(k) = v' ∈ V)))))@i
24. ↑j ∈ dom(Estimate(s;b))
25. Estimate(s;b)(j) = v' ∈ V
26. ∀k:ℤ. (((j < k ∧ k < i) ∧ (↑k ∈ dom(Estimate(s;b)))) ⇒ (Estimate(s;b)(k) = v' ∈ V))
27. i1 : ℕ
28. i1 < ||L|| c∧ (v' = L[i1] ∈ V)
29. j1 : ℕi
⊢ (∃v'∈L. (¬(v' = v ∈ V))
  ∧ (∀b∈ws.(b ∈ ws')
       ⇒ ((↑j1 ∈ dom(Estimate(s;b)))
          ∧ (Estimate(s;b)(j1) = v' ∈ V)
          ∧ (∀k:{j1 + 1..i-}. ((↑k ∈ dom(Estimate(s;b))) ⇒ (Estimate(s;b)(k) = v' ∈ V)))))) ∈ ℙ
BY
{ RepeatFor 3 ((MemCD THEN Try (QuickAuto))) }

1
.....subterm..... T:t
2:n
1. V : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. v1 : V@i
4. v2 : V@i
5. ¬(v1 = v2 ∈ V)@i
6. A : Id List@i
7. W : {a:Id| (a ∈ A)}  List List@i
8. ws : {a:Id| (a ∈ A)}  List@i
9. ws' : {a:Id| (a ∈ A)}  List@i
10. s : ConsensusState@i
11. i : ℤ@i
12. v : V@i
13. L : V List
14. ∀b:{a:Id| (a ∈ A)} . ∀v:V. ∀j:ℤ.  ((v ∈ L)) supposing ((Estimate(s;b)(j) = v ∈ V) and (↑j ∈ dom(Estimate(s;b))))
15. b : Id
16. (b ∈ ws)
17. (b ∈ ws')
18. j : ℤ@i
19. 0 ≤ j@i
20. j < i@i
21. v' : V@i
22. ¬(v' = v ∈ V)@i
23. ∀b:{a:Id| (a ∈ A)} 
      (((b ∈ ws) ∧ (b ∈ ws'))
      ⇒ ((↑j ∈ dom(Estimate(s;b)))
         ∧ (Estimate(s;b)(j) = v' ∈ V)
         ∧ (∀k:ℤ. (((j < k ∧ k < i) ∧ (↑k ∈ dom(Estimate(s;b)))) ⇒ (Estimate(s;b)(k) = v' ∈ V)))))@i
24. ↑j ∈ dom(Estimate(s;b))
25. Estimate(s;b)(j) = v' ∈ V
26. ∀k:ℤ. (((j < k ∧ k < i) ∧ (↑k ∈ dom(Estimate(s;b)))) ⇒ (Estimate(s;b)(k) = v' ∈ V))
27. i1 : ℕ
28. i1 < ||L|| c∧ (v' = L[i1] ∈ V)
29. j1 : ℕi
30. v3 : {x:V| (x ∈ L)} @i
31. b1 : {x:Id| (x ∈ ws)} @i
⊢ (b1 ∈ ws')
  ⇒ ((↑j1 ∈ dom(Estimate(s;b1)))
     ∧ (Estimate(s;b1)(j1) = v3 ∈ V)
     ∧ (∀k:{j1 + 1..i-}. ((↑k ∈ dom(Estimate(s;b1))) ⇒ (Estimate(s;b1)(k) = v3 ∈ V)))) ∈ ℙ

---

Latex:


.....wf..... 
1.  V  :  Type
2.  \mforall{}v1,v2:V.    Dec(v1  =  v2)@i
3.  v1  :  V@i
4.  v2  :  V@i
5.  \mneg{}(v1  =  v2)@i
6.  A  :  Id  List@i
7.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
8.  ws  :  \{a:Id|  (a  \mmember{}  A)\}    List@i
9.  ws'  :  \{a:Id|  (a  \mmember{}  A)\}    List@i
10.  s  :  ConsensusState@i
11.  i  :  \mBbbZ{}@i
12.  v  :  V@i
13.  L  :  V  List
14.  \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))))
15.  b  :  Id
16.  (b  \mmember{}  ws)
17.  (b  \mmember{}  ws')
18.  j  :  \mBbbZ{}@i
19.  0  \mleq{}  j@i
20.  j  <  i@i
21.  v'  :  V@i
22.  \mneg{}(v'  =  v)@i
23.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\} 
            (((b  \mmember{}  ws)  \mwedge{}  (b  \mmember{}  ws'))
            {}\mRightarrow{}  ((\muparrow{}j  \mmember{}  dom(Estimate(s;b)))
                  \mwedge{}  (Estimate(s;b)(j)  =  v')
                  \mwedge{}  (\mforall{}k:\mBbbZ{}.  (((j  <  k  \mwedge{}  k  <  i)  \mwedge{}  (\muparrow{}k  \mmember{}  dom(Estimate(s;b))))  {}\mRightarrow{}  (Estimate(s;b)(k)  =  v')))))@i
24.  \muparrow{}j  \mmember{}  dom(Estimate(s;b))
25.  Estimate(s;b)(j)  =  v'
26.  \mforall{}k:\mBbbZ{}.  (((j  <  k  \mwedge{}  k  <  i)  \mwedge{}  (\muparrow{}k  \mmember{}  dom(Estimate(s;b))))  {}\mRightarrow{}  (Estimate(s;b)(k)  =  v'))
27.  i1  :  \mBbbN{}
28.  i1  <  ||L||  c\mwedge{}  (v'  =  L[i1])
29.  j1  :  \mBbbN{}i
\mvdash{}  (\mexists{}v'\mmember{}L.  (\mneg{}(v'  =  v))
    \mwedge{}  (\mforall{}b\mmember{}ws.(b  \mmember{}  ws')
              {}\mRightarrow{}  ((\muparrow{}j1  \mmember{}  dom(Estimate(s;b)))
                    \mwedge{}  (Estimate(s;b)(j1)  =  v')
                    \mwedge{}  (\mforall{}k:\{j1  +  1..i\msupminus{}\}.  ((\muparrow{}k  \mmember{}  dom(Estimate(s;b)))  {}\mRightarrow{}  (Estimate(s;b)(k)  =  v'))))))  \mmember{}  \mBbbP{}


By

RepeatFor  3  ((MemCD  THEN  Try  (QuickAuto)))

---

Home Index