Step
*
4
of Lemma
cs-ref-map-unchanged
1. [V] : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. A : Id List@i
4. W : {a:Id| (a ∈ A)} List List@i
5. two-intersection(A;W)@i
6. f : ConsensusState ─→ (consensus-state3(V) List)@i
7. ∀s:ConsensusState. ∀i:ℕ.
((i < ||f s|| ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
∧ (i < ||f s||
⇒ ((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)))))))))@i
8. x : ts-reachable(consensus-ts4(V;A;W))@i
9. y : ts-reachable(consensus-ts4(V;A;W))@i
10. x ∈ ConsensusState
11. y ∈ ConsensusState
12. x ts-rel(consensus-ts4(V;A;W)) y@i
13. i : ℕ@i
14. i < ||f x||
15. i < ||f y||
16. ∀v:V. (in state x, inning i could commit v ⇒ in state y, inning i could commit v )@i
17. v : V
18. f x[i] = COMMITED[v] ∈ consensus-state3(V)
19. (f x[i] = INITIAL ∈ consensus-state3(V))
⇒ (∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state x, inning i could commit v ∧ in state x, inning i could commit v' ))
20. (f x[i] = INITIAL ∈ consensus-state3(V)) ⇐ ∃v,v':V
((¬(v = v' ∈ V))
∧ in state x, inning i could commit v
∧ in state x, inning i could commit v' )
21. (f x[i] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state x, inning i could commit v ))
22. (f x[i] = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state x, inning i could commit v )
23. ∀v:V
((f x[i] = COMMITED[v] ∈ consensus-state3(V) ⇐⇒ in state x, inning i has committed v)
∧ (f x[i] = CONSIDERING[v] ∈ consensus-state3(V)
⇐⇒ in state x, inning i could commit v
∧ (¬in state x, inning i has committed v)
∧ (∀v':V. (in state x, inning i could commit v' ⇒ (v' = v ∈ V)))))
24. (f x[i] = CONSIDERING[v] ∈ consensus-state3(V))
⇒ (in state x, inning i could commit v
∧ (¬in state x, inning i has committed v)
∧ (∀v':V. (in state x, inning i could commit v' ⇒ (v' = v ∈ V))))
25. (f x[i] = CONSIDERING[v] ∈ consensus-state3(V)) ⇐ in state x, inning i could commit v
∧ (¬in state x, inning i has committed v)
∧ (∀v':V. (in state x, inning i could commit v' ⇒ (v' = v ∈ V)))
26. in state x, inning i has committed v
27. f x[i] = COMMITED[v] ∈ consensus-state3(V)
⊢ (f y[i] = f x[i] ∈ consensus-state3(V))
∨ (∃v:V. ((f y[i] = COMMITED[v] ∈ consensus-state3(V)) ∧ (f x[i] = CONSIDERING[v] ∈ consensus-state3(V))))
BY
{ (Assert in state y, inning i has committed v BY
(InstLemma `consensus-ts4-inning-committed-stable` [⌈V⌉;⌈A⌉;⌈W⌉;⌈v⌉;⌈i⌉]⋅ THEN Auto)) }
1
1. [V] : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. A : Id List@i
4. W : {a:Id| (a ∈ A)} List List@i
5. two-intersection(A;W)@i
6. f : ConsensusState ─→ (consensus-state3(V) List)@i
7. ∀s:ConsensusState. ∀i:ℕ.
((i < ||f s|| ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
∧ (i < ||f s||
⇒ ((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)))))))))@i
8. x : ts-reachable(consensus-ts4(V;A;W))@i
9. y : ts-reachable(consensus-ts4(V;A;W))@i
10. x ∈ ConsensusState
11. y ∈ ConsensusState
12. x ts-rel(consensus-ts4(V;A;W)) y@i
13. i : ℕ@i
14. i < ||f x||
15. i < ||f y||
16. ∀v:V. (in state x, inning i could commit v ⇒ in state y, inning i could commit v )@i
17. v : V
18. f x[i] = COMMITED[v] ∈ consensus-state3(V)
19. (f x[i] = INITIAL ∈ consensus-state3(V))
⇒ (∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state x, inning i could commit v ∧ in state x, inning i could commit v' ))
20. (f x[i] = INITIAL ∈ consensus-state3(V)) ⇐ ∃v,v':V
((¬(v = v' ∈ V))
∧ in state x, inning i could commit v
∧ in state x, inning i could commit v' )
21. (f x[i] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state x, inning i could commit v ))
22. (f x[i] = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state x, inning i could commit v )
23. ∀v:V
((f x[i] = COMMITED[v] ∈ consensus-state3(V) ⇐⇒ in state x, inning i has committed v)
∧ (f x[i] = CONSIDERING[v] ∈ consensus-state3(V)
⇐⇒ in state x, inning i could commit v
∧ (¬in state x, inning i has committed v)
∧ (∀v':V. (in state x, inning i could commit v' ⇒ (v' = v ∈ V)))))
24. (f x[i] = CONSIDERING[v] ∈ consensus-state3(V))
⇒ (in state x, inning i could commit v
∧ (¬in state x, inning i has committed v)
∧ (∀v':V. (in state x, inning i could commit v' ⇒ (v' = v ∈ V))))
25. (f x[i] = CONSIDERING[v] ∈ consensus-state3(V)) ⇐ in state x, inning i could commit v
∧ (¬in state x, inning i has committed v)
∧ (∀v':V. (in state x, inning i could commit v' ⇒ (v' = v ∈ V)))
26. in state x, inning i has committed v
27. f x[i] = COMMITED[v] ∈ consensus-state3(V)
28. in state y, inning i has committed v
⊢ (f y[i] = f x[i] ∈ consensus-state3(V))
∨ (∃v:V. ((f y[i] = COMMITED[v] ∈ consensus-state3(V)) ∧ (f x[i] = CONSIDERING[v] ∈ consensus-state3(V))))
Latex:
1. [V] : Type
2. \mforall{}v1,v2:V. Dec(v1 = v2)@i
3. A : Id List@i
4. W : \{a:Id| (a \mmember{} A)\} List List@i
5. two-intersection(A;W)@i
6. f : ConsensusState {}\mrightarrow{} (consensus-state3(V) List)@i
7. \mforall{}s:ConsensusState. \mforall{}i:\mBbbN{}.
((i < ||f s|| \mLeftarrow{}{}\mRightarrow{} \mexists{}a:\{a:Id| (a \mmember{} A)\} . (i \mleq{} Inning(s;a)))
\mwedge{} (i < ||f s||
{}\mRightarrow{} ((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)))))))))@i
8. x : ts-reachable(consensus-ts4(V;A;W))@i
9. y : ts-reachable(consensus-ts4(V;A;W))@i
10. x \mmember{} ConsensusState
11. y \mmember{} ConsensusState
12. x ts-rel(consensus-ts4(V;A;W)) y@i
13. i : \mBbbN{}@i
14. i < ||f x||
15. i < ||f y||
16. \mforall{}v:V. (in state x, inning i could commit v {}\mRightarrow{} in state y, inning i could commit v )@i
17. v : V
18. f x[i] = COMMITED[v]
19. (f x[i] = INITIAL)
{}\mRightarrow{} (\mexists{}v,v':V
((\mneg{}(v = v')) \mwedge{} in state x, inning i could commit v \mwedge{} in state x, inning i could commit v' ))
20. (f x[i] = INITIAL) \mLeftarrow{}{} \mexists{}v,v':V
((\mneg{}(v = v'))
\mwedge{} in state x, inning i could commit v
\mwedge{} in state x, inning i could commit v' )
21. (f x[i] = WITHDRAWN) {}\mRightarrow{} (\mneg{}(\mexists{}v:V. in state x, inning i could commit v ))
22. (f x[i] = WITHDRAWN) \mLeftarrow{}{} \mneg{}(\mexists{}v:V. in state x, inning i could commit v )
23. \mforall{}v:V
((f x[i] = COMMITED[v] \mLeftarrow{}{}\mRightarrow{} in state x, inning i has committed v)
\mwedge{} (f x[i] = CONSIDERING[v]
\mLeftarrow{}{}\mRightarrow{} in state x, inning i could commit v
\mwedge{} (\mneg{}in state x, inning i has committed v)
\mwedge{} (\mforall{}v':V. (in state x, inning i could commit v' {}\mRightarrow{} (v' = v)))))
24. (f x[i] = CONSIDERING[v])
{}\mRightarrow{} (in state x, inning i could commit v
\mwedge{} (\mneg{}in state x, inning i has committed v)
\mwedge{} (\mforall{}v':V. (in state x, inning i could commit v' {}\mRightarrow{} (v' = v))))
25. (f x[i] = CONSIDERING[v]) \mLeftarrow{}{} in state x, inning i could commit v
\mwedge{} (\mneg{}in state x, inning i has committed v)
\mwedge{} (\mforall{}v':V. (in state x, inning i could commit v' {}\mRightarrow{} (v' = v)))
26. in state x, inning i has committed v
27. f x[i] = COMMITED[v]
\mvdash{} (f y[i] = f x[i]) \mvee{} (\mexists{}v:V. ((f y[i] = COMMITED[v]) \mwedge{} (f x[i] = CONSIDERING[v])))
By
(Assert in state y, inning i has committed v BY
(InstLemma `consensus-ts4-inning-committed-stable` [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}W\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{} THEN Auto))
Home
Index