Step
*
1
of Lemma
new_23_sig_decided_property
1. Cmd : {T:Type| valueall-type(T)}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : ℤ
6. flrs : ℤ
7. propose : Atom List
8. notify : Atom List
9. slots : set-sig{i:l}(ℤ)
10. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
11. es : EO+(Message(f))
12. eo-msg-interface-constraint(es;new_23_sig_main();new_23_sig_headers_internal();f)@i
13. e : E@i
14. c : Cmd@i
15. n : ℤ@i
16. <n, c> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e)@i
17. (f propose) = (ℤ × Cmd) ∈ Type
18. (f notify) = (ℤ × Cmd) ∈ Type
19. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
20. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
21. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
22. f ∈ Name ⟶ Type
23. e' : E
24. delay : ℤ
25. (e' < e)
26. loc(e') ↓∈ reps
27. e1 : {e1:E| e1 ≤loc e' }
28. z1 : ℤ
29. z2 : Cmd
30. ((header(e1) = propose ∈ Name) ∧ has-es-info-type(es;e1;f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e1) ∈ (ℤ × Cmd)))
∨ ((header(e1) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
∧ (z1 = (fst(fst(fst(msgval(e1))))) ∈ ℤ)
∧ (z2 = (snd(fst(msgval(e1)))) ∈ Cmd))
31. ¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1))
32. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e1 and e')
33. (no new_23_sig_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, 0> between e1 and e')
34. header(e') = ``new_23_sig vote`` ∈ Name
35. has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
36. ↑(new_23_sig_newvote(Cmd) <z1, 0> msgval(e') new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))
37. ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))|| = (coeff * flrs) ∈ ℤ
38. delay = 0 ∈ ℤ
39. (fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))];sn\000Cd(fst(msgval(e')))))) = ((coeff * flrs) + 1) ∈ ℤ
40. loc(e) ↓∈ reps
41. msg-authentic(info(e)) = ff
42. n = (fst(fst(fst(msgval(e'))))) ∈ ℤ
43. c = (snd(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))\000C];snd(fst(msgval(e')))))) ∈ Cmd
44. (∀z∈[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))].z = c ∈ Cmd)
⊢ ↓∃x:Id
∃rnd:ℕ
∃L:Id List
(no_repeats(Id;L)
∧ (||L|| = ((coeff * flrs) + 1) ∈ ℤ)
∧ (∀vtr∈L.↓∃e':E. mk-msg-interface(x;make-Msg(``new_23_sig vote``;<<<n, rnd>, c>, vtr>)) ∈ new_23_sig_main()(e')))
BY
{ (D 0
THEN InstConcl [⌜loc(e')⌝;⌜0⌝;⌜[snd(msgval(e')) / (snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e\000C')))]⌝]⋅
THEN Auto
THEN InstLemma `new_23_sig_quorum_invariant_fun` [⌜Cmd⌝;⌜notify⌝;⌜propose⌝;⌜f⌝;⌜es.e1⌝;⌜e'⌝;⌜<z1, 0>⌝]⋅
THEN Auto) }
1
1. Cmd : {T:Type| valueall-type(T)}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : ℤ
6. flrs : ℤ
7. propose : Atom List
8. notify : Atom List
9. slots : set-sig{i:l}(ℤ)
10. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
11. es : EO+(Message(f))
12. eo-msg-interface-constraint(es;new_23_sig_main();new_23_sig_headers_internal();f)@i
13. e : E@i
14. c : Cmd@i
15. n : ℤ@i
16. <n, c> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e)@i
17. (f propose) = (ℤ × Cmd) ∈ Type
18. (f notify) = (ℤ × Cmd) ∈ Type
19. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
20. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
21. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
22. f ∈ Name ⟶ Type
23. e' : E
24. delay : ℤ
25. (e' < e)
26. loc(e') ↓∈ reps
27. e1 : {e1:E| e1 ≤loc e' }
28. z1 : ℤ
29. z2 : Cmd
30. ((header(e1) = propose ∈ Name) ∧ has-es-info-type(es;e1;f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e1) ∈ (ℤ × Cmd)))
∨ ((header(e1) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
∧ (z1 = (fst(fst(fst(msgval(e1))))) ∈ ℤ)
∧ (z2 = (snd(fst(msgval(e1)))) ∈ Cmd))
31. ¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1))
32. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e1 and e')
33. (no new_23_sig_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, 0> between e1 and e')
34. header(e') = ``new_23_sig vote`` ∈ Name
35. has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
36. ↑(new_23_sig_newvote(Cmd) <z1, 0> msgval(e') new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))
37. ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))|| = (coeff * flrs) ∈ ℤ
38. delay = 0 ∈ ℤ
39. (fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))];sn\000Cd(fst(msgval(e')))))) = ((coeff * flrs) + 1) ∈ ℤ
40. loc(e) ↓∈ reps
41. msg-authentic(info(e)) = ff
42. n = (fst(fst(fst(msgval(e'))))) ∈ ℤ
43. c = (snd(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))\000C];snd(fst(msgval(e')))))) ∈ Cmd
44. (∀z∈[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))].z = c ∈ Cmd)
45. no_repeats(Id;snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))
46. msgval(e') ∈ ℤ × ℤ × Cmd × Id
47. no_repeats(Id;snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))
48. ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))|| = ||fst(new_23_sig_QuorumStateFun(Cmd;noti\000Cfy;propose;f;<z1, 0>;es.e1;e'))|| ∈ ℤ
⊢ ¬(snd(msgval(e')) ∈ snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))
2
1. Cmd : {T:Type| valueall-type(T)}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : ℤ
6. flrs : ℤ
7. propose : Atom List
8. notify : Atom List
9. slots : set-sig{i:l}(ℤ)
10. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
11. es : EO+(Message(f))
12. eo-msg-interface-constraint(es;new_23_sig_main();new_23_sig_headers_internal();f)@i
13. e : E@i
14. c : Cmd@i
15. n : ℤ@i
16. <n, c> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e)@i
17. (f propose) = (ℤ × Cmd) ∈ Type
18. (f notify) = (ℤ × Cmd) ∈ Type
19. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
20. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
21. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
22. f ∈ Name ⟶ Type
23. e' : E
24. delay : ℤ
25. (e' < e)
26. loc(e') ↓∈ reps
27. e1 : {e1:E| e1 ≤loc e' }
28. z1 : ℤ
29. z2 : Cmd
30. ((header(e1) = propose ∈ Name) ∧ has-es-info-type(es;e1;f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e1) ∈ (ℤ × Cmd)))
∨ ((header(e1) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
∧ (z1 = (fst(fst(fst(msgval(e1))))) ∈ ℤ)
∧ (z2 = (snd(fst(msgval(e1)))) ∈ Cmd))
31. ¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1))
32. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e1 and e')
33. (no new_23_sig_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, 0> between e1 and e')
34. header(e') = ``new_23_sig vote`` ∈ Name
35. has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
36. ↑(new_23_sig_newvote(Cmd) <z1, 0> msgval(e') new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))
37. ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))|| = (coeff * flrs) ∈ ℤ
38. delay = 0 ∈ ℤ
39. (fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))];sn\000Cd(fst(msgval(e')))))) = ((coeff * flrs) + 1) ∈ ℤ
40. loc(e) ↓∈ reps
41. msg-authentic(info(e)) = ff
42. n = (fst(fst(fst(msgval(e'))))) ∈ ℤ
43. c = (snd(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))\000C];snd(fst(msgval(e')))))) ∈ Cmd
44. (∀z∈[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))].z = c ∈ Cmd)
45. no_repeats(Id;[snd(msgval(e')) / (snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))])
46. ||[snd(msgval(e')) / (snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))]|| = ((coeff * flrs) + \000C1) ∈ ℤ
47. msgval(e') ∈ ℤ × ℤ × Cmd × Id
48. no_repeats(Id;snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))
49. ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))|| = ||fst(new_23_sig_QuorumStateFun(Cmd;noti\000Cfy;propose;f;<z1, 0>;es.e1;e'))|| ∈ ℤ
⊢ (∀vtr∈[snd(msgval(e')) / (snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))].↓∃e'@0:E. mk-msg-int\000Cerface(loc(e');make-Msg(``new_23_sig vote``;<<<n, 0>, c>, vtr>)) ∈ new_23_sig_main()(e'@0))
3
1. Cmd : {T:Type| valueall-type(T)}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : ℤ
6. flrs : ℤ
7. propose : Atom List
8. notify : Atom List
9. slots : set-sig{i:l}(ℤ)
10. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
11. es : EO+(Message(f))
12. eo-msg-interface-constraint(es;new_23_sig_main();new_23_sig_headers_internal();f)@i
13. e : E@i
14. c : Cmd@i
15. n : ℤ@i
16. <n, c> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e)@i
17. (f propose) = (ℤ × Cmd) ∈ Type
18. (f notify) = (ℤ × Cmd) ∈ Type
19. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
20. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
21. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
22. f ∈ Name ⟶ Type
23. e' : E
24. delay : ℤ
25. (e' < e)
26. loc(e') ↓∈ reps
27. e1 : {e1:E| e1 ≤loc e' }
28. z1 : ℤ
29. z2 : Cmd
30. ((header(e1) = propose ∈ Name) ∧ has-es-info-type(es;e1;f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e1) ∈ (ℤ × Cmd)))
∨ ((header(e1) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
∧ (z1 = (fst(fst(fst(msgval(e1))))) ∈ ℤ)
∧ (z2 = (snd(fst(msgval(e1)))) ∈ Cmd))
31. ¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1))
32. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e1 and e')
33. (no new_23_sig_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, 0> between e1 and e')
34. header(e') = ``new_23_sig vote`` ∈ Name
35. has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
36. ↑(new_23_sig_newvote(Cmd) <z1, 0> msgval(e') new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))
37. ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))|| = (coeff * flrs) ∈ ℤ
38. delay = 0 ∈ ℤ
39. (fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))];sn\000Cd(fst(msgval(e')))))) = ((coeff * flrs) + 1) ∈ ℤ
40. loc(e) ↓∈ reps
41. msg-authentic(info(e)) = ff
42. n = (fst(fst(fst(msgval(e'))))) ∈ ℤ
43. c = (snd(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))\000C];snd(fst(msgval(e')))))) ∈ Cmd
44. (∀z∈[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))].z = c ∈ Cmd)
45. rnd : ℕ
46. L : Id List@i
47. no_repeats(Id;L)
48. ||L|| = ((coeff * flrs) + 1) ∈ ℤ
49. ∀x:Id. ((x ∈ L) ∈ Type)
50. vtr : Id@i
51. (vtr ∈ L)@i
52. e'@0 : E@i
53. no_repeats(Id;snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))
54. ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))|| = ||fst(new_23_sig_QuorumStateFun(Cmd;noti\000Cfy;propose;f;<z1, 0>;es.e1;e'))|| ∈ ℤ
⊢ <<<n, rnd>, c>, vtr> ∈ f ``new_23_sig vote``
4
1. Cmd : {T:Type| valueall-type(T)}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : ℤ
6. flrs : ℤ
7. propose : Atom List
8. notify : Atom List
9. slots : set-sig{i:l}(ℤ)
10. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
11. es : EO+(Message(f))
12. eo-msg-interface-constraint(es;new_23_sig_main();new_23_sig_headers_internal();f)@i
13. e : E@i
14. c : Cmd@i
15. n : ℤ@i
16. <n, c> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e)@i
17. (f propose) = (ℤ × Cmd) ∈ Type
18. (f notify) = (ℤ × Cmd) ∈ Type
19. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
20. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
21. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
22. f ∈ Name ⟶ Type
23. e' : E
24. delay : ℤ
25. (e' < e)
26. loc(e') ↓∈ reps
27. e1 : {e1:E| e1 ≤loc e' }
28. z1 : ℤ
29. z2 : Cmd
30. ((header(e1) = propose ∈ Name) ∧ has-es-info-type(es;e1;f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e1) ∈ (ℤ × Cmd)))
∨ ((header(e1) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
∧ (z1 = (fst(fst(fst(msgval(e1))))) ∈ ℤ)
∧ (z2 = (snd(fst(msgval(e1)))) ∈ Cmd))
31. ¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1))
32. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e1 and e')
33. (no new_23_sig_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, 0> between e1 and e')
34. header(e') = ``new_23_sig vote`` ∈ Name
35. has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
36. ↑(new_23_sig_newvote(Cmd) <z1, 0> msgval(e') new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))
37. ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))|| = (coeff * flrs) ∈ ℤ
38. delay = 0 ∈ ℤ
39. (fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))];sn\000Cd(fst(msgval(e')))))) = ((coeff * flrs) + 1) ∈ ℤ
40. loc(e) ↓∈ reps
41. msg-authentic(info(e)) = ff
42. n = (fst(fst(fst(msgval(e'))))) ∈ ℤ
43. c = (snd(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))\000C];snd(fst(msgval(e')))))) ∈ Cmd
44. (∀z∈[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))].z = c ∈ Cmd)
45. x : Id
46. rnd : ℕ@i
47. L : Id List@i
48. no_repeats(Id;L)
49. ||L|| = ((coeff * flrs) + 1) ∈ ℤ
50. ∀x:Id. ((x ∈ L) ∈ Type)
51. vtr : Id@i
52. (vtr ∈ L)@i
53. e2 : E@i
54. no_repeats(Id;snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))
55. ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))|| = ||fst(new_23_sig_QuorumStateFun(Cmd;noti\000Cfy;propose;f;<z1, 0>;es.e1;e'))|| ∈ ℤ
⊢ <<<n, rnd>, c>, vtr> ∈ f ``new_23_sig vote``
Latex:
Latex:
1. Cmd : \{T:Type| valueall-type(T)\}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : \mBbbZ{}
6. flrs : \mBbbZ{}
7. propose : Atom List
8. notify : Atom List
9. slots : set-sig\{i:l\}(\mBbbZ{})
10. f : new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose)
11. es : EO+(Message(f))
12. eo-msg-interface-constraint(es;new\_23\_sig\_main();new\_23\_sig\_headers\_internal();f)@i
13. e : E@i
14. c : Cmd@i
15. n : \mBbbZ{}@i
16. <n, c> \mmember{} new\_23\_sig\_decided'base(Cmd;notify;propose;f)(e)@i
17. (f propose) = (\mBbbZ{} \mtimes{} Cmd)
18. (f notify) = (\mBbbZ{} \mtimes{} Cmd)
19. (f ``new\_23\_sig decided``) = (\mBbbZ{} \mtimes{} Cmd)
20. (f ``new\_23\_sig retry``) = (\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)
21. (f ``new\_23\_sig vote``) = (\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)
22. f \mmember{} Name {}\mrightarrow{} Type
23. e' : E
24. delay : \mBbbZ{}
25. (e' < e)
26. loc(e') \mdownarrow{}\mmember{} reps
27. e1 : \{e1:E| e1 \mleq{}loc e' \}
28. z1 : \mBbbZ{}
29. z2 : Cmd
30. ((header(e1) = propose) \mwedge{} has-es-info-type(es;e1;f;\mBbbZ{} \mtimes{} Cmd) \mwedge{} (<z1, z2> = 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{} (z1 = (fst(fst(fst(msgval(e1))))))
\mwedge{} (z2 = (snd(fst(msgval(e1))))))
31. \mneg{}\muparrow{}(set-sig-member(slots) z1 new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1))
32. (no new\_23\_sig\_Notify(Cmd;clients;notify;propose;f) z1 between e1 and e')
33. (no new\_23\_sig\_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, 0> between e1 and e')
34. header(e') = ``new\_23\_sig vote``
35. has-es-info-type(es;e';f;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)
36. \muparrow{}(new\_23\_sig\_newvote(Cmd) <z1, 0> msgval(e') new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1,\000C 0>es.e1;e'))
37. ||fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>es.e1;e'))|| = (coeff * flrs)
38. delay = 0
39. (fst(poss-maj(eq;[snd(fst(msgval(e'))) /
(fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>es.e1;e')))];snd(f\000Cst(msgval(e'))))))
= ((coeff * flrs) + 1)
40. loc(e) \mdownarrow{}\mmember{} reps
41. msg-authentic(info(e)) = ff
42. n = (fst(fst(fst(msgval(e')))))
43. c
= (snd(poss-maj(eq;[snd(fst(msgval(e'))) /
(fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>es.e1;e')))];snd(fst\000C(msgval(e'))))))
44. (\mforall{}z\mmember{}[snd(fst(msgval(e'))) / (fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>es.e1;e'\000C)))].z = c)
\mvdash{} \mdownarrow{}\mexists{}x:Id
\mexists{}rnd:\mBbbN{}
\mexists{}L:Id List
(no\_repeats(Id;L)
\mwedge{} (||L|| = ((coeff * flrs) + 1))
\mwedge{} (\mforall{}vtr\mmember{}L.\mdownarrow{}\mexists{}e':E. mk-msg-interface(x;make-Msg(``new\_23\_sig vote``;<<<n, rnd>, c>, vtr>)) \mmember{} new\000C\_23\_sig\_main()(e')))
By
Latex:
(D 0
THEN InstConcl [\mkleeneopen{}loc(e')\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}[snd(msgval(e')) /
(snd(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>es.e1;e\000C')))]\mkleeneclose{}]\mcdot{}
THEN Auto
THEN InstLemma `new\_23\_sig\_quorum\_invariant\_fun` [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}notify\mkleeneclose{};\mkleeneopen{}propose\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es.e1\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{};\mkleeneopen{}<z1
, 0
>\mkleeneclose{}]\mcdot{}
THEN Auto)
Home
Index