Step
*
1
1
1
1
1
1
of Lemma
decidable__cs-archive-blocked
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. (v' ∈ L)
⊢ ∃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))))))
BY
{ (D -1 THEN With ⌈j⌉ (D 0)⋅) }
1
.....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)
⊢ j ∈ ℕi
2
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)
⊢ (∃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))))))
3
.....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)))))) ∈ ℙ
Latex:
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. (v' \mmember{} L)
\mvdash{} \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'))))))
By
(D -1 THEN With \mkleeneopen{}j\mkleeneclose{} (D 0)\mcdot{})
Home
Index