Step
*
1
of Lemma
cs-ref-map-changed
1. [V] : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(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 : ConsensusState ─→ (consensus-state3(V) List)@i
8. cs-ref-map-constraints(V;A;W;f)@i
9. x : ts-reachable(consensus-ts4(V;A;W))@i
10. y : ts-reachable(consensus-ts4(V;A;W))@i
11. x ∈ ConsensusState
12. y ∈ ConsensusState
13. x ts-rel(consensus-ts4(V;A;W)) y@i
14. i : ℕ@i
15. i < ||f x||
16. i < ||f y||
17. v : V@i
18. in state x, inning i could commit v @i
19. ¬in state y, inning i could commit v @i
⊢ (f y[i] = WITHDRAWN ∈ consensus-state3(V))
∨ ((f x[i] = INITIAL ∈ consensus-state3(V))
∧ ((f y[i] = INITIAL ∈ consensus-state3(V))
∨ (∃v':V
((∀j:ℕi. (¬(f x[j] = INITIAL ∈ consensus-state3(V))))
∧ ((f y[i] = CONSIDERING[v'] ∈ consensus-state3(V)) ∨ (f y[i] = COMMITED[v'] ∈ consensus-state3(V)))
∧ (∀j:ℕi. ∀v'':V.
(((f x[j] = CONSIDERING[v''] ∈ consensus-state3(V)) ∨ (f x[j] = COMMITED[v''] ∈ consensus-state3(V)))
⇒ (v'' = v' ∈ V)))))))
BY
{ ((InstLemma `consensus-state3-cases` [⌈V⌉;⌈f x[i]⌉]⋅ THENA Auto)
THEN SplitOrHyps
THEN ExRepD
THEN SplitOrHyps
THEN OnMaybeHyp 8 (\h. ((Unfold `cs-ref-map-constraints` h
THEN (InstHyp [⌈x⌉;⌈i⌉] h⋅ THENA Auto)
THEN D -1
THEN Thin (-2)
THEN (D -1 THENA Auto))
THEN Auto
THEN Try ((SimpleInstHyp ⌈v1⌉ (-1)⋅ THENA Auto))
THEN Auto
THEN ThinTrivial))⋅)⋅ }
1
1. [V] : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(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 : ConsensusState ─→ (consensus-state3(V) List)@i
8. ∀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
9. x : ts-reachable(consensus-ts4(V;A;W))@i
10. y : ts-reachable(consensus-ts4(V;A;W))@i
11. x ∈ ConsensusState
12. y ∈ ConsensusState
13. x ts-rel(consensus-ts4(V;A;W)) y@i
14. i : ℕ@i
15. i < ||f x||
16. i < ||f y||
17. v : V@i
18. in state x, inning i could commit v @i
19. ¬in state y, inning i could commit v @i
20. f x[i] = INITIAL ∈ consensus-state3(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. ∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state x, inning i could commit v ∧ in state x, inning i could commit v' )
25. f x[i] = INITIAL ∈ consensus-state3(V)
⊢ (f y[i] = WITHDRAWN ∈ consensus-state3(V))
∨ ((f x[i] = INITIAL ∈ consensus-state3(V))
∧ ((f y[i] = INITIAL ∈ consensus-state3(V))
∨ (∃v':V
((∀j:ℕi. (¬(f x[j] = INITIAL ∈ consensus-state3(V))))
∧ ((f y[i] = CONSIDERING[v'] ∈ consensus-state3(V)) ∨ (f y[i] = COMMITED[v'] ∈ consensus-state3(V)))
∧ (∀j:ℕi. ∀v'':V.
(((f x[j] = CONSIDERING[v''] ∈ consensus-state3(V)) ∨ (f x[j] = COMMITED[v''] ∈ consensus-state3(V)))
⇒ (v'' = v' ∈ V)))))))
2
1. [V] : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(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 : ConsensusState ─→ (consensus-state3(V) List)@i
8. ∀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
9. x : ts-reachable(consensus-ts4(V;A;W))@i
10. y : ts-reachable(consensus-ts4(V;A;W))@i
11. x ∈ ConsensusState
12. y ∈ ConsensusState
13. x ts-rel(consensus-ts4(V;A;W)) y@i
14. i : ℕ@i
15. i < ||f x||
16. i < ||f y||
17. v : V@i
18. in state x, inning i could commit v @i
19. ¬in state y, inning i could commit v @i
20. f x[i] = WITHDRAWN ∈ consensus-state3(V)
21. (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' ))
22. (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' )
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. ¬(∃v:V. in state x, inning i could commit v )
25. f x[i] = WITHDRAWN ∈ consensus-state3(V)
⊢ (f y[i] = WITHDRAWN ∈ consensus-state3(V))
∨ ((f x[i] = INITIAL ∈ consensus-state3(V))
∧ ((f y[i] = INITIAL ∈ consensus-state3(V))
∨ (∃v':V
((∀j:ℕi. (¬(f x[j] = INITIAL ∈ consensus-state3(V))))
∧ ((f y[i] = CONSIDERING[v'] ∈ consensus-state3(V)) ∨ (f y[i] = COMMITED[v'] ∈ consensus-state3(V)))
∧ (∀j:ℕi. ∀v'':V.
(((f x[j] = CONSIDERING[v''] ∈ consensus-state3(V)) ∨ (f x[j] = COMMITED[v''] ∈ consensus-state3(V)))
⇒ (v'' = v' ∈ V)))))))
3
1. [V] : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(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 : ConsensusState ─→ (consensus-state3(V) List)@i
8. ∀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
9. x : ts-reachable(consensus-ts4(V;A;W))@i
10. y : ts-reachable(consensus-ts4(V;A;W))@i
11. x ∈ ConsensusState
12. y ∈ ConsensusState
13. x ts-rel(consensus-ts4(V;A;W)) y@i
14. i : ℕ@i
15. i < ||f x||
16. i < ||f y||
17. v : V@i
18. in state x, inning i could commit v @i
19. ¬in state y, inning i could commit v @i
20. v1 : V
21. f x[i] = CONSIDERING[v1] ∈ consensus-state3(V)
22. (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' ))
23. (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' )
24. (f x[i] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state x, inning i could commit v ))
25. (f x[i] = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state x, inning i could commit v )
26. ∀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)))))
27. (f x[i] = COMMITED[v1] ∈ consensus-state3(V)) ⇒ in state x, inning i has committed v1
28. (f x[i] = CONSIDERING[v1] ∈ consensus-state3(V)) ⇐ in state x, inning i could commit v1
∧ (¬in state x, inning i has committed v1)
∧ (∀v':V. (in state x, inning i could commit v' ⇒ (v' = v1 ∈ V)))
29. in state x, inning i could commit v1
30. ¬in state x, inning i has committed v1
31. ∀v':V. (in state x, inning i could commit v' ⇒ (v' = v1 ∈ V))
⊢ (f y[i] = WITHDRAWN ∈ consensus-state3(V))
∨ ((f x[i] = INITIAL ∈ consensus-state3(V))
∧ ((f y[i] = INITIAL ∈ consensus-state3(V))
∨ (∃v':V
((∀j:ℕi. (¬(f x[j] = INITIAL ∈ consensus-state3(V))))
∧ ((f y[i] = CONSIDERING[v'] ∈ consensus-state3(V)) ∨ (f y[i] = COMMITED[v'] ∈ consensus-state3(V)))
∧ (∀j:ℕi. ∀v'':V.
(((f x[j] = CONSIDERING[v''] ∈ consensus-state3(V)) ∨ (f x[j] = COMMITED[v''] ∈ consensus-state3(V)))
⇒ (v'' = v' ∈ V)))))))
4
1. [V] : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(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 : ConsensusState ─→ (consensus-state3(V) List)@i
8. ∀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
9. x : ts-reachable(consensus-ts4(V;A;W))@i
10. y : ts-reachable(consensus-ts4(V;A;W))@i
11. x ∈ ConsensusState
12. y ∈ ConsensusState
13. x ts-rel(consensus-ts4(V;A;W)) y@i
14. i : ℕ@i
15. i < ||f x||
16. i < ||f y||
17. v : V@i
18. in state x, inning i could commit v @i
19. ¬in state y, inning i could commit v @i
20. v1 : V
21. f x[i] = COMMITED[v1] ∈ consensus-state3(V)
22. (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' ))
23. (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' )
24. (f x[i] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state x, inning i could commit v ))
25. (f x[i] = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state x, inning i could commit v )
26. ∀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)))))
27. (f x[i] = CONSIDERING[v1] ∈ consensus-state3(V))
⇒ (in state x, inning i could commit v1
∧ (¬in state x, inning i has committed v1)
∧ (∀v':V. (in state x, inning i could commit v' ⇒ (v' = v1 ∈ V))))
28. (f x[i] = CONSIDERING[v1] ∈ consensus-state3(V)) ⇐ in state x, inning i could commit v1
∧ (¬in state x, inning i has committed v1)
∧ (∀v':V. (in state x, inning i could commit v' ⇒ (v' = v1 ∈ V)))
29. in state x, inning i has committed v1
30. f x[i] = COMMITED[v1] ∈ consensus-state3(V)
⊢ (f y[i] = WITHDRAWN ∈ consensus-state3(V))
∨ ((f x[i] = INITIAL ∈ consensus-state3(V))
∧ ((f y[i] = INITIAL ∈ consensus-state3(V))
∨ (∃v':V
((∀j:ℕi. (¬(f x[j] = INITIAL ∈ consensus-state3(V))))
∧ ((f y[i] = CONSIDERING[v'] ∈ consensus-state3(V)) ∨ (f y[i] = COMMITED[v'] ∈ consensus-state3(V)))
∧ (∀j:ℕi. ∀v'':V.
(((f x[j] = CONSIDERING[v''] ∈ consensus-state3(V)) ∨ (f x[j] = COMMITED[v''] ∈ consensus-state3(V)))
⇒ (v'' = v' ∈ V)))))))
Latex:
1. [V] : Type
2. \mforall{}v1,v2:V. Dec(v1 = v2)@i
3. \{\mexists{}v,v':V. (\mneg{}(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 : ConsensusState {}\mrightarrow{} (consensus-state3(V) List)@i
8. cs-ref-map-constraints(V;A;W;f)@i
9. x : ts-reachable(consensus-ts4(V;A;W))@i
10. y : ts-reachable(consensus-ts4(V;A;W))@i
11. x \mmember{} ConsensusState
12. y \mmember{} ConsensusState
13. x ts-rel(consensus-ts4(V;A;W)) y@i
14. i : \mBbbN{}@i
15. i < ||f x||
16. i < ||f y||
17. v : V@i
18. in state x, inning i could commit v @i
19. \mneg{}in state y, inning i could commit v @i
\mvdash{} (f y[i] = WITHDRAWN)
\mvee{} ((f x[i] = INITIAL)
\mwedge{} ((f y[i] = INITIAL)
\mvee{} (\mexists{}v':V
((\mforall{}j:\mBbbN{}i. (\mneg{}(f x[j] = INITIAL)))
\mwedge{} ((f y[i] = CONSIDERING[v']) \mvee{} (f y[i] = COMMITED[v']))
\mwedge{} (\mforall{}j:\mBbbN{}i. \mforall{}v'':V.
(((f x[j] = CONSIDERING[v'']) \mvee{} (f x[j] = COMMITED[v''])) {}\mRightarrow{} (v'' = v')))))))
By
((InstLemma `consensus-state3-cases` [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}f x[i]\mkleeneclose{}]\mcdot{} THENA Auto)
THEN SplitOrHyps
THEN ExRepD
THEN SplitOrHyps
THEN OnMaybeHyp 8 (\mbackslash{}h. ((Unfold `cs-ref-map-constraints` h
THEN (InstHyp [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}] h\mcdot{} THENA Auto)
THEN D -1
THEN Thin (-2)
THEN (D -1 THENA Auto))
THEN Auto
THEN Try ((SimpleInstHyp \mkleeneopen{}v1\mkleeneclose{} (-1)\mcdot{} THENA Auto))
THEN Auto
THEN ThinTrivial))\mcdot{})\mcdot{}
Home
Index