Step
*
1
1
1
1
3
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. v' : V@i
5. ¬(v1 = v' ∈ 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@i
19. i@0 : ℕ||L||@i
20. ¬(L[i@0] = v ∈ V)@i
21. (∀b∈ws.(b ∈ ws')
⇒ ((↑j ∈ dom(Estimate(s;b)))
∧ (Estimate(s;b)(j) = L[i@0] ∈ V)
∧ (∀k:{j + 1..i-}. ((↑k ∈ dom(Estimate(s;b))) ⇒ (Estimate(s;b)(k) = L[i@0] ∈ V)))))@i
22. 0 ≤ j
23. j < i
⊢ ∃v':V
((¬(v' = v ∈ V))
∧ (∀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)))))))
BY
{ (RWO "l_all_iff" (-3) THENA Try (Complete (Auto))) }
1
.....wf.....
1. V : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. v1 : V@i
4. v' : V@i
5. ¬(v1 = v' ∈ 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@i
19. i@0 : ℕ||L||@i
20. ¬(L[i@0] = v ∈ V)@i
21. (∀b∈ws.(b ∈ ws')
⇒ ((↑j ∈ dom(Estimate(s;b)))
∧ (Estimate(s;b)(j) = L[i@0] ∈ V)
∧ (∀k:{j + 1..i-}. ((↑k ∈ dom(Estimate(s;b))) ⇒ (Estimate(s;b)(k) = L[i@0] ∈ V)))))@i
22. 0 ≤ j
23. j < i
⊢ λb.((b ∈ ws')
⇒ ((↑j ∈ dom(Estimate(s;b)))
∧ (Estimate(s;b)(j) = L[i@0] ∈ V)
∧ (∀k:{j + 1..i-}. ((↑k ∈ dom(Estimate(s;b))) ⇒ (Estimate(s;b)(k) = L[i@0] ∈ V))))) ∈ {x:Id| (x ∈ ws)} ⟶ ℙ
2
1. [V] : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. v1 : V@i
4. v' : V@i
5. ¬(v1 = v' ∈ 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@i
19. i@0 : ℕ||L||@i
20. ¬(L[i@0] = v ∈ V)@i
21. ∀b:Id
((b ∈ ws)
⇒ (b ∈ ws')
⇒ ((↑j ∈ dom(Estimate(s;b)))
∧ (Estimate(s;b)(j) = L[i@0] ∈ V)
∧ (∀k:{j + 1..i-}. ((↑k ∈ dom(Estimate(s;b))) ⇒ (Estimate(s;b)(k) = L[i@0] ∈ V)))))
22. 0 ≤ j
23. j < i
⊢ ∃v':V
((¬(v' = v ∈ V))
∧ (∀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)))))))
Latex:
Latex:
1. [V] : Type
2. \mforall{}v1,v2:V. Dec(v1 = v2)@i
3. v1 : V@i
4. v' : V@i
5. \mneg{}(v1 = v')@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 : \mBbbN{}i@i
19. i@0 : \mBbbN{}||L||@i
20. \mneg{}(L[i@0] = v)@i
21. (\mforall{}b\mmember{}ws.(b \mmember{} ws')
{}\mRightarrow{} ((\muparrow{}j \mmember{} dom(Estimate(s;b)))
\mwedge{} (Estimate(s;b)(j) = L[i@0])
\mwedge{} (\mforall{}k:\{j + 1..i\msupminus{}\}. ((\muparrow{}k \mmember{} dom(Estimate(s;b))) {}\mRightarrow{} (Estimate(s;b)(k) = L[i@0])))))@i
22. 0 \mleq{} j
23. j < 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{}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')))))))
By
Latex:
(RWO "l\_all\_iff" (-3) THENA Try (Complete (Auto)))
Home
Index