---

Step * 1 1 1 1 of Lemma new_23_sig_votes_consistent


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. ((r = 0 ∈ ℤ) ∧ (c1 = z3 ∈ Cmd) ∧ (e1 = e3 ∈ E))
∨ (new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e3;e1) < r
  ∧ (((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)))))
43. loc(e2) ↓∈ reps
44. e' : E
45. e' ≤loc e2 
46. z2 : Cmd
47. ((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))
48. ¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))
49. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) n between e' and e2)
50. l2 ↓∈ reps
51. d2 = 0 ∈ ℤ
52. ff = ff
53. sender = loc(e2) ∈ Id
54. ((r = 0 ∈ ℤ) ∧ (c2 = z2 ∈ Cmd) ∧ (e2 = e' ∈ E))
∨ (new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e';e2) < r
  ∧ (((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)))))
⊢ <n, z3> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e3)
∨ <n, z3> ∈ (new_23_sig_vote2prop(Cmd) o new_23_sig_vote'base(Cmd;notify;propose;f))(e3)
BY
{ (D 35
   THEN Try (Complete (((OrLeft THENA Auto) THEN MaUseClassRel'' 0 THEN Auto)))
   THEN (OrRight THENA Auto)
   THEN MaUseClassRel'' 0
   THEN D 0
   THEN InstConcl [⌈msgval(e3)⌉]⋅
   THEN Auto
   THEN Try (Complete ((MaUseClassRel'' 0 THEN Auto)))
   THEN Repeat (BagMemberD 0)
   THEN Auto) }

---

Latex:

---

Latex:

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.  ((r  =  0)  \mwedge{}  (c1  =  z3)  \mwedge{}  (e1  =  e3))
\mvee{}  (new\_23\_sig\_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e3;e1)  <  r
    \mwedge{}  (((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)))))))
43.  loc(e2)  \mdownarrow{}\mmember{}  reps
44.  e'  :  E
45.  e'  \mleq{}loc  e2 
46.  z2  :  Cmd
47.  ((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'))))))
48.  \mneg{}\muparrow{}(set-sig-member(slots)  n  new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))
49.  (no  new\_23\_sig\_Notify(Cmd;clients;notify;propose;f)  n  between  e'  and  e2)
50.  l2  \mdownarrow{}\mmember{}  reps
51.  d2  =  0
52.  ff  =  ff
53.  sender  =  loc(e2)
54.  ((r  =  0)  \mwedge{}  (c2  =  z2)  \mwedge{}  (e2  =  e'))
\mvee{}  (new\_23\_sig\_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e';e2)  <  r
    \mwedge{}  (((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)))))))
\mvdash{}  <n,  z3>  \mmember{}  new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e3)
\mvee{}  <n,  z3>  \mmember{}  (new\_23\_sig\_vote2prop(Cmd)  o  new\_23\_sig\_vote'base(Cmd;notify;propose;f))(e3)


By

---

Latex:
(D  35
  THEN  Try  (Complete  (((OrLeft  THENA  Auto)  THEN  MaUseClassRel''  0  THEN  Auto)))
  THEN  (OrRight  THENA  Auto)
  THEN  MaUseClassRel''  0
  THEN  D  0
  THEN  InstConcl  [\mkleeneopen{}msgval(e3)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  ((MaUseClassRel''  0  THEN  Auto)))
  THEN  Repeat  (BagMemberD  0)
  THEN  Auto)

---

Home Index