---

Step * 1 1 2 4 1 of Lemma new_23_sig_votes_consistent

.....assertion..... 
1. Cmd : Type
2. valueall-type(Cmd)
3. cmdeq : EqDecider(Cmd)
4. reps : bag(Id)
5. clients : bag(Id)
6. coeff : ℤ
7. flrs : ℤ
8. notify : Atom List
9. propose : Atom List
10. slots : set-sig{i:l}(ℤ)
11. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
12. (f propose) = (ℤ × Cmd) ∈ Type
13. (f notify) = (ℤ × Cmd) ∈ Type
14. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
15. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
16. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
17. f ∈ Name ─→ Type
18. es : EO+(Message(f))
19. new_23_sig_message-constraint{i:l}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f)@i'
20. e1 : E@i
21. e2 : E@i
22. n : ℤ@i
23. r : ℤ@i
24. sender : Id@i
25. l1 : Id@i
26. l2 : Id@i
27. c1 : Cmd@i
28. c2 : Cmd@i
29. d1 : ℤ@i
30. d2 : ℤ@i
31. loc(e1) ↓∈ reps
32. e3 : E
33. e3 ≤loc e1 
34. z3 : Cmd
35. ((header(e3) = propose ∈ Name) ∧ has-es-info-type(es;e3;f;ℤ × Cmd) ∧ (<n, z3> = msgval(e3) ∈ (ℤ × Cmd)))
∨ ((header(e3) = ``new_23_sig vote`` ∈ Name)
  ∧ has-es-info-type(es;e3;f;ℤ × ℤ × Cmd × Id)
  ∧ (n = (fst(fst(fst(msgval(e3))))) ∈ ℤ)
  ∧ (z3 = (snd(fst(msgval(e3)))) ∈ Cmd))
36. ¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e3))
37. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) n between e3 and e1)
38. l1 ↓∈ reps
39. d1 = 0 ∈ ℤ
40. ff = ff
41. sender = loc(e1) ∈ Id
42. new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e3;e1) < r
43. ((header(e1) = ``new_23_sig retry`` ∈ Name)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd)
∧ (<<n, r>, c1> = msgval(e1) ∈ (ℤ × ℤ × Cmd)))
∨ ((header(e1) = ``new_23_sig vote`` ∈ Name)
  ∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
  ∧ (<<n, r>, c1> = (fst(msgval(e1))) ∈ (ℤ × ℤ × Cmd)))
44. loc(e2) ↓∈ reps
45. e' : E
46. e' ≤loc e2 
47. z2 : Cmd
48. ((header(e') = propose ∈ Name) ∧ has-es-info-type(es;e';f;ℤ × Cmd) ∧ (<n, z2> = msgval(e') ∈ (ℤ × Cmd)))
∨ ((header(e') = ``new_23_sig vote`` ∈ Name)
  ∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
  ∧ (n = (fst(fst(fst(msgval(e'))))) ∈ ℤ)
  ∧ (z2 = (snd(fst(msgval(e')))) ∈ Cmd))
49. ¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))
50. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) n between e' and e2)
51. l2 ↓∈ reps
52. d2 = 0 ∈ ℤ
53. ff = ff
54. sender = loc(e2) ∈ Id
55. new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e';e2) < r
56. ((header(e2) = ``new_23_sig retry`` ∈ Name)
∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd)
∧ (<<n, r>, c2> = msgval(e2) ∈ (ℤ × ℤ × Cmd)))
∨ ((header(e2) = ``new_23_sig vote`` ∈ Name)
  ∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd × Id)
  ∧ (<<n, r>, c2> = (fst(msgval(e2))) ∈ (ℤ × ℤ × Cmd)))
57. e' = e3 ∈ E
⊢ e2 = e1 ∈ E
BY
{ (UseLoclTri ⌈es⌉⌈e1⌉⌈e2⌉⋅ THEN Assert ⌈False⌉⋅ THEN Auto) }

1
.....assertion..... 
1. Cmd : Type
2. valueall-type(Cmd)
3. cmdeq : EqDecider(Cmd)
4. reps : bag(Id)
5. clients : bag(Id)
6. coeff : ℤ
7. flrs : ℤ
8. notify : Atom List
9. propose : Atom List
10. slots : set-sig{i:l}(ℤ)
11. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
12. (f propose) = (ℤ × Cmd) ∈ Type
13. (f notify) = (ℤ × Cmd) ∈ Type
14. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
15. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
16. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
17. f ∈ Name ─→ Type
18. es : EO+(Message(f))
19. new_23_sig_message-constraint{i:l}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f)@i'
20. e1 : E@i
21. e2 : E@i
22. n : ℤ@i
23. r : ℤ@i
24. sender : Id@i
25. l1 : Id@i
26. l2 : Id@i
27. c1 : Cmd@i
28. c2 : Cmd@i
29. d1 : ℤ@i
30. d2 : ℤ@i
31. loc(e1) ↓∈ reps
32. e3 : E
33. e3 ≤loc e1 
34. z3 : Cmd
35. ((header(e3) = propose ∈ Name) ∧ has-es-info-type(es;e3;f;ℤ × Cmd) ∧ (<n, z3> = msgval(e3) ∈ (ℤ × Cmd)))
∨ ((header(e3) = ``new_23_sig vote`` ∈ Name)
  ∧ has-es-info-type(es;e3;f;ℤ × ℤ × Cmd × Id)
  ∧ (n = (fst(fst(fst(msgval(e3))))) ∈ ℤ)
  ∧ (z3 = (snd(fst(msgval(e3)))) ∈ Cmd))
36. ¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e3))
37. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) n between e3 and e1)
38. l1 ↓∈ reps
39. d1 = 0 ∈ ℤ
40. ff = ff
41. sender = loc(e1) ∈ Id
42. new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e3;e1) < r
43. ((header(e1) = ``new_23_sig retry`` ∈ Name)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd)
∧ (<<n, r>, c1> = msgval(e1) ∈ (ℤ × ℤ × Cmd)))
∨ ((header(e1) = ``new_23_sig vote`` ∈ Name)
  ∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
  ∧ (<<n, r>, c1> = (fst(msgval(e1))) ∈ (ℤ × ℤ × Cmd)))
44. loc(e2) ↓∈ reps
45. e' : E
46. e' ≤loc e2 
47. z2 : Cmd
48. ((header(e') = propose ∈ Name) ∧ has-es-info-type(es;e';f;ℤ × Cmd) ∧ (<n, z2> = msgval(e') ∈ (ℤ × Cmd)))
∨ ((header(e') = ``new_23_sig vote`` ∈ Name)
  ∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
  ∧ (n = (fst(fst(fst(msgval(e'))))) ∈ ℤ)
  ∧ (z2 = (snd(fst(msgval(e')))) ∈ Cmd))
49. ¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))
50. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) n between e' and e2)
51. l2 ↓∈ reps
52. d2 = 0 ∈ ℤ
53. ff = ff
54. sender = loc(e2) ∈ Id
55. new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e';e2) < r
56. ((header(e2) = ``new_23_sig retry`` ∈ Name)
∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd)
∧ (<<n, r>, c2> = msgval(e2) ∈ (ℤ × ℤ × Cmd)))
∨ ((header(e2) = ``new_23_sig vote`` ∈ Name)
  ∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd × Id)
  ∧ (<<n, r>, c2> = (fst(msgval(e2))) ∈ (ℤ × ℤ × Cmd)))
57. e' = e3 ∈ E
58. (e1 <loc e2)
⊢ False

2
.....assertion..... 
1. Cmd : Type
2. valueall-type(Cmd)
3. cmdeq : EqDecider(Cmd)
4. reps : bag(Id)
5. clients : bag(Id)
6. coeff : ℤ
7. flrs : ℤ
8. notify : Atom List
9. propose : Atom List
10. slots : set-sig{i:l}(ℤ)
11. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
12. (f propose) = (ℤ × Cmd) ∈ Type
13. (f notify) = (ℤ × Cmd) ∈ Type
14. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
15. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
16. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
17. f ∈ Name ─→ Type
18. es : EO+(Message(f))
19. new_23_sig_message-constraint{i:l}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f)@i'
20. e1 : E@i
21. e2 : E@i
22. n : ℤ@i
23. r : ℤ@i
24. sender : Id@i
25. l1 : Id@i
26. l2 : Id@i
27. c1 : Cmd@i
28. c2 : Cmd@i
29. d1 : ℤ@i
30. d2 : ℤ@i
31. loc(e1) ↓∈ reps
32. e3 : E
33. e3 ≤loc e1 
34. z3 : Cmd
35. ((header(e3) = propose ∈ Name) ∧ has-es-info-type(es;e3;f;ℤ × Cmd) ∧ (<n, z3> = msgval(e3) ∈ (ℤ × Cmd)))
∨ ((header(e3) = ``new_23_sig vote`` ∈ Name)
  ∧ has-es-info-type(es;e3;f;ℤ × ℤ × Cmd × Id)
  ∧ (n = (fst(fst(fst(msgval(e3))))) ∈ ℤ)
  ∧ (z3 = (snd(fst(msgval(e3)))) ∈ Cmd))
36. ¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e3))
37. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) n between e3 and e1)
38. l1 ↓∈ reps
39. d1 = 0 ∈ ℤ
40. ff = ff
41. sender = loc(e1) ∈ Id
42. new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e3;e1) < r
43. ((header(e1) = ``new_23_sig retry`` ∈ Name)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd)
∧ (<<n, r>, c1> = msgval(e1) ∈ (ℤ × ℤ × Cmd)))
∨ ((header(e1) = ``new_23_sig vote`` ∈ Name)
  ∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
  ∧ (<<n, r>, c1> = (fst(msgval(e1))) ∈ (ℤ × ℤ × Cmd)))
44. loc(e2) ↓∈ reps
45. e' : E
46. e' ≤loc e2 
47. z2 : Cmd
48. ((header(e') = propose ∈ Name) ∧ has-es-info-type(es;e';f;ℤ × Cmd) ∧ (<n, z2> = msgval(e') ∈ (ℤ × Cmd)))
∨ ((header(e') = ``new_23_sig vote`` ∈ Name)
  ∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
  ∧ (n = (fst(fst(fst(msgval(e'))))) ∈ ℤ)
  ∧ (z2 = (snd(fst(msgval(e')))) ∈ Cmd))
49. ¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))
50. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) n between e' and e2)
51. l2 ↓∈ reps
52. d2 = 0 ∈ ℤ
53. ff = ff
54. sender = loc(e2) ∈ Id
55. new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e';e2) < r
56. ((header(e2) = ``new_23_sig retry`` ∈ Name)
∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd)
∧ (<<n, r>, c2> = msgval(e2) ∈ (ℤ × ℤ × Cmd)))
∨ ((header(e2) = ``new_23_sig vote`` ∈ Name)
  ∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd × Id)
  ∧ (<<n, r>, c2> = (fst(msgval(e2))) ∈ (ℤ × ℤ × Cmd)))
57. e' = e3 ∈ E
58. (e2 <loc e1)
⊢ False

---

Latex:

---

Latex:
.....assertion..... 
1.  Cmd  :  Type
2.  valueall-type(Cmd)
3.  cmdeq  :  EqDecider(Cmd)
4.  reps  :  bag(Id)
5.  clients  :  bag(Id)
6.  coeff  :  \mBbbZ{}
7.  flrs  :  \mBbbZ{}
8.  notify  :  Atom  List
9.  propose  :  Atom  List
10.  slots  :  set-sig\{i:l\}(\mBbbZ{})
11.  f  :  new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose)
12.  (f  propose)  =  (\mBbbZ{}  \mtimes{}  Cmd)
13.  (f  notify)  =  (\mBbbZ{}  \mtimes{}  Cmd)
14.  (f  ``new\_23\_sig  decided``)  =  (\mBbbZ{}  \mtimes{}  Cmd)
15.  (f  ``new\_23\_sig  retry``)  =  (\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)
16.  (f  ``new\_23\_sig  vote``)  =  (\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)
17.  f  \mmember{}  Name  {}\mrightarrow{}  Type
18.  es  :  EO+(Message(f))
19.  new\_23\_sig\_message-constraint\{i:l\}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f)@i'
20.  e1  :  E@i
21.  e2  :  E@i
22.  n  :  \mBbbZ{}@i
23.  r  :  \mBbbZ{}@i
24.  sender  :  Id@i
25.  l1  :  Id@i
26.  l2  :  Id@i
27.  c1  :  Cmd@i
28.  c2  :  Cmd@i
29.  d1  :  \mBbbZ{}@i
30.  d2  :  \mBbbZ{}@i
31.  loc(e1)  \mdownarrow{}\mmember{}  reps
32.  e3  :  E
33.  e3  \mleq{}loc  e1 
34.  z3  :  Cmd
35.  ((header(e3)  =  propose)  \mwedge{}  has-es-info-type(es;e3;f;\mBbbZ{}  \mtimes{}  Cmd)  \mwedge{}  (<n,  z3>  =  msgval(e3)))
\mvee{}  ((header(e3)  =  ``new\_23\_sig  vote``)
    \mwedge{}  has-es-info-type(es;e3;f;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)
    \mwedge{}  (n  =  (fst(fst(fst(msgval(e3))))))
    \mwedge{}  (z3  =  (snd(fst(msgval(e3))))))
36.  \mneg{}\muparrow{}(set-sig-member(slots)  n  new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e3))
37.  (no  new\_23\_sig\_Notify(Cmd;clients;notify;propose;f)  n  between  e3  and  e1)
38.  l1  \mdownarrow{}\mmember{}  reps
39.  d1  =  0
40.  ff  =  ff
41.  sender  =  loc(e1)
42.  new\_23\_sig\_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e3;e1)  <  r
43.  ((header(e1)  =  ``new\_23\_sig  retry``)
\mwedge{}  has-es-info-type(es;e1;f;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)
\mwedge{}  (<<n,  r>,  c1>  =  msgval(e1)))
\mvee{}  ((header(e1)  =  ``new\_23\_sig  vote``)
    \mwedge{}  has-es-info-type(es;e1;f;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)
    \mwedge{}  (<<n,  r>,  c1>  =  (fst(msgval(e1)))))
44.  loc(e2)  \mdownarrow{}\mmember{}  reps
45.  e'  :  E
46.  e'  \mleq{}loc  e2 
47.  z2  :  Cmd
48.  ((header(e')  =  propose)  \mwedge{}  has-es-info-type(es;e';f;\mBbbZ{}  \mtimes{}  Cmd)  \mwedge{}  (<n,  z2>  =  msgval(e')))
\mvee{}  ((header(e')  =  ``new\_23\_sig  vote``)
    \mwedge{}  has-es-info-type(es;e';f;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)
    \mwedge{}  (n  =  (fst(fst(fst(msgval(e'))))))
    \mwedge{}  (z2  =  (snd(fst(msgval(e'))))))
49.  \mneg{}\muparrow{}(set-sig-member(slots)  n  new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))
50.  (no  new\_23\_sig\_Notify(Cmd;clients;notify;propose;f)  n  between  e'  and  e2)
51.  l2  \mdownarrow{}\mmember{}  reps
52.  d2  =  0
53.  ff  =  ff
54.  sender  =  loc(e2)
55.  new\_23\_sig\_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e';e2)  <  r
56.  ((header(e2)  =  ``new\_23\_sig  retry``)
\mwedge{}  has-es-info-type(es;e2;f;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)
\mwedge{}  (<<n,  r>,  c2>  =  msgval(e2)))
\mvee{}  ((header(e2)  =  ``new\_23\_sig  vote``)
    \mwedge{}  has-es-info-type(es;e2;f;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)
    \mwedge{}  (<<n,  r>,  c2>  =  (fst(msgval(e2)))))
57.  e'  =  e3
\mvdash{}  e2  =  e1


By

---

Latex:
(UseLoclTri  \mkleeneopen{}es\mkleeneclose{}\mkleeneopen{}e1\mkleeneclose{}\mkleeneopen{}e2\mkleeneclose{}\mcdot{}  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index