Step
*
1
2
1
2
2
of Lemma
consensus-ts4-ref-map
1. [V] : Type
2. ∃v,v':V. (¬(v = v' ∈ V))@i
3. ∀v,v':V. Dec(v = v' ∈ V)@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)} List List@i
6. two-intersection(A;W)@i
7. F : s:ConsensusState ⟶ i:ℤ ⟶ consensus-state3(V)
8. ∀s:ConsensusState. ∀i:ℤ.
(((F s i) = INITIAL ∈ consensus-state3(V)
⇐⇒ ∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v ∧ in state s, inning i could commit v' ))
∧ ((F s i) = WITHDRAWN ∈ consensus-state3(V) ⇐⇒ ¬(∃v:V. in state s, inning i could commit v ))
∧ (∀v:V
(((F s i) = COMMITED[v] ∈ consensus-state3(V) ⇐⇒ in state s, inning i has committed v)
∧ ((F s i) = CONSIDERING[v] ∈ consensus-state3(V)
⇐⇒ in state s, inning i could commit v
∧ (¬in state s, inning i has committed v)
∧ (∀v':V. (in state s, inning i could commit v' ⇒ (v' = v ∈ V)))))))
9. N : s:ConsensusState ⟶ ℕ
10. ∀s:ConsensusState. ∀i:ℕ. (i < N s ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
11. s : ConsensusState@i
12. ∀i:ℕ. (i < N s ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
13. i : ℕ@i
14. i < N s ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a))
⊢ (i < N s ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
∧ (i < N s
⇒ ((map(λi.(F s i);upto(N s))[i] = INITIAL ∈ consensus-state3(V)
⇐⇒ ∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v ∧ in state s, inning i could commit v' ))
∧ (map(λi.(F s i);upto(N s))[i] = WITHDRAWN ∈ consensus-state3(V)
⇐⇒ ¬(∃v:V. in state s, inning i could commit v ))
∧ (∀v:V
((map(λi.(F s i);upto(N s))[i] = COMMITED[v] ∈ consensus-state3(V) ⇐⇒ in state s, inning i has committed v)
∧ (map(λi.(F s i);upto(N s))[i] = CONSIDERING[v] ∈ consensus-state3(V)
⇐⇒ in state s, inning i could commit v
∧ (¬in state s, inning i has committed v)
∧ (∀v':V. (in state s, inning i could commit v' ⇒ (v' = v ∈ V))))))))
BY
{ ((D 0 THEN Try (Trivial)) THEN (GenConcl ⌜(N s) = n ∈ ℕ⌝⋅ THENA Auto) THEN (D 0 THENA Auto)) }
1
1. [V] : Type
2. ∃v,v':V. (¬(v = v' ∈ V))@i
3. ∀v,v':V. Dec(v = v' ∈ V)@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)} List List@i
6. two-intersection(A;W)@i
7. F : s:ConsensusState ⟶ i:ℤ ⟶ consensus-state3(V)
8. ∀s:ConsensusState. ∀i:ℤ.
(((F s i) = INITIAL ∈ consensus-state3(V)
⇐⇒ ∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v ∧ in state s, inning i could commit v' ))
∧ ((F s i) = WITHDRAWN ∈ consensus-state3(V) ⇐⇒ ¬(∃v:V. in state s, inning i could commit v ))
∧ (∀v:V
(((F s i) = COMMITED[v] ∈ consensus-state3(V) ⇐⇒ in state s, inning i has committed v)
∧ ((F s i) = CONSIDERING[v] ∈ consensus-state3(V)
⇐⇒ in state s, inning i could commit v
∧ (¬in state s, inning i has committed v)
∧ (∀v':V. (in state s, inning i could commit v' ⇒ (v' = v ∈ V)))))))
9. N : s:ConsensusState ⟶ ℕ
10. ∀s:ConsensusState. ∀i:ℕ. (i < N s ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
11. s : ConsensusState@i
12. ∀i:ℕ. (i < N s ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
13. i : ℕ@i
14. i < N s ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a))
15. n : ℕ@i
16. (N s) = n ∈ ℕ@i
17. i < n@i
⊢ (map(λi.(F s i);upto(n))[i] = INITIAL ∈ consensus-state3(V)
⇐⇒ ∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v ∧ in state s, inning i could commit v' ))
∧ (map(λi.(F s i);upto(n))[i] = WITHDRAWN ∈ consensus-state3(V) ⇐⇒ ¬(∃v:V. in state s, inning i could commit v ))
∧ (∀v:V
((map(λi.(F s i);upto(n))[i] = COMMITED[v] ∈ consensus-state3(V) ⇐⇒ in state s, inning i has committed v)
∧ (map(λi.(F s i);upto(n))[i] = CONSIDERING[v] ∈ consensus-state3(V)
⇐⇒ in state s, inning i could commit v
∧ (¬in state s, inning i has committed v)
∧ (∀v':V. (in state s, inning i could commit v' ⇒ (v' = v ∈ V))))))
Latex:
Latex:
1. [V] : Type
2. \mexists{}v,v':V. (\mneg{}(v = v'))@i
3. \mforall{}v,v':V. Dec(v = v')@i
4. A : Id List@i
5. W : \{a:Id| (a \mmember{} A)\} List List@i
6. two-intersection(A;W)@i
7. F : s:ConsensusState {}\mrightarrow{} i:\mBbbZ{} {}\mrightarrow{} consensus-state3(V)
8. \mforall{}s:ConsensusState. \mforall{}i:\mBbbZ{}.
(((F s i) = INITIAL
\mLeftarrow{}{}\mRightarrow{} \mexists{}v,v':V
((\mneg{}(v = v'))
\mwedge{} in state s, inning i could commit v
\mwedge{} in state s, inning i could commit v' ))
\mwedge{} ((F s i) = WITHDRAWN \mLeftarrow{}{}\mRightarrow{} \mneg{}(\mexists{}v:V. in state s, inning i could commit v ))
\mwedge{} (\mforall{}v:V
(((F s i) = COMMITED[v] \mLeftarrow{}{}\mRightarrow{} in state s, inning i has committed v)
\mwedge{} ((F s i) = CONSIDERING[v]
\mLeftarrow{}{}\mRightarrow{} in state s, inning i could commit v
\mwedge{} (\mneg{}in state s, inning i has committed v)
\mwedge{} (\mforall{}v':V. (in state s, inning i could commit v' {}\mRightarrow{} (v' = v)))))))
9. N : s:ConsensusState {}\mrightarrow{} \mBbbN{}
10. \mforall{}s:ConsensusState. \mforall{}i:\mBbbN{}. (i < N s \mLeftarrow{}{}\mRightarrow{} \mexists{}a:\{a:Id| (a \mmember{} A)\} . (i \mleq{} Inning(s;a)))
11. s : ConsensusState@i
12. \mforall{}i:\mBbbN{}. (i < N s \mLeftarrow{}{}\mRightarrow{} \mexists{}a:\{a:Id| (a \mmember{} A)\} . (i \mleq{} Inning(s;a)))
13. i : \mBbbN{}@i
14. i < N s \mLeftarrow{}{}\mRightarrow{} \mexists{}a:\{a:Id| (a \mmember{} A)\} . (i \mleq{} Inning(s;a))
\mvdash{} (i < N s \mLeftarrow{}{}\mRightarrow{} \mexists{}a:\{a:Id| (a \mmember{} A)\} . (i \mleq{} Inning(s;a)))
\mwedge{} (i < N s
{}\mRightarrow{} ((map(\mlambda{}i.(F s i);upto(N s))[i] = INITIAL
\mLeftarrow{}{}\mRightarrow{} \mexists{}v,v':V
((\mneg{}(v = v'))
\mwedge{} in state s, inning i could commit v
\mwedge{} in state s, inning i could commit v' ))
\mwedge{} (map(\mlambda{}i.(F s i);upto(N s))[i] = WITHDRAWN \mLeftarrow{}{}\mRightarrow{} \mneg{}(\mexists{}v:V. in state s, inning i could commit v ))
\mwedge{} (\mforall{}v:V
((map(\mlambda{}i.(F s i);upto(N s))[i] = COMMITED[v] \mLeftarrow{}{}\mRightarrow{} in state s, inning i has committed v)
\mwedge{} (map(\mlambda{}i.(F s i);upto(N s))[i] = CONSIDERING[v]
\mLeftarrow{}{}\mRightarrow{} in state s, inning i could commit v
\mwedge{} (\mneg{}in state s, inning i has committed v)
\mwedge{} (\mforall{}v':V. (in state s, inning i could commit v' {}\mRightarrow{} (v' = v))))))))
By
Latex:
((D 0 THEN Try (Trivial)) THEN (GenConcl \mkleeneopen{}(N s) = n\mkleeneclose{}\mcdot{} THENA Auto) THEN (D 0 THENA Auto))
Home
Index