Step
*
1
3
of Lemma
new_23_sig_validity
1. Cmd : {T:Type| valueall-type(T)}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : {2...}
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. (f propose) = (ℤ × Cmd) ∈ Type
12. (f notify) = (ℤ × Cmd) ∈ Type
13. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
14. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
15. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
16. f ∈ Name ─→ Type
17. es : EO+(Message(f))
18. new_23_sig_message-constraint{i:l}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;f)@i'
19. e : E@i
20. ∀e1:E
((e1 < e)
⇒ ((∀v:ℤ × Cmd
(v ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e1)
⇒ (↓∃e':E. ((e' < e1) ∧ v ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))
∧ (∀v:ℤ × ℤ × Cmd × Id
(v ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e1)
⇒ (↓∃e':E
((e' < e1) ∧ <fst(fst(fst(v))), snd(fst(v))> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))
∧ (∀v:ℤ × ℤ × Cmd
(v ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e1)
⇒ (↓∃e':E. ((e' < e1) ∧ <fst(fst(v)), snd(v)> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))
∧ (∀e2:E
(e2 c≤ e1
⇒ (∀n,rnd:ℤ. ∀c:Cmd.
((c ∈ fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>;es.e2;e1)))
⇒ (↓∃e':E. ((e' < e1) ∧ <n, c> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))))))
21. ∀v:ℤ × Cmd
(v ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e)
⇒ (↓∃e':E. ((e' < e) ∧ v ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'))))
22. ∀v:ℤ × ℤ × Cmd × Id
(v ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e)
⇒ (↓∃e':E. ((e' < e) ∧ <fst(fst(fst(v))), snd(fst(v))> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'))))
23. v3 : ℤ@i
24. v4 : ℤ@i
25. v2 : Cmd@i
26. <<v3, v4>, v2> ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e)@i
27. e' : E
28. delay : ℤ
29. (e' < e)
30. loc(e') ↓∈ reps
31. e1 : {e1:E| e1 ≤loc e' }
32. z1 : ℤ
33. z2 : Cmd
34. ((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))
35. ¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1))
36. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e1 and e')
37. ((no new_23_sig_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, 0> between e1 and e')
∧ ((header(e') = ``new_23_sig vote`` ∈ Name) ∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id))
∧ (↑(new_23_sig_newvote(Cmd) <z1, 0> msgval(e') new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))
∧ (||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))|| = (coeff * flrs) ∈ ℤ)
∧ (delay = 0 ∈ ℤ)
∧ (¬((fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))];s\000Cnd(fst(msgval(e')))))) = ((coeff * flrs) + 1) ∈ ℤ))
∧ (loc(e) = loc(e') ∈ Id)
∧ msg-authentic(info(e)) = ff
∧ ((v3 = (fst(fst(fst(msgval(e'))))) ∈ ℤ) ∧ (v4 = ((snd(fst(fst(msgval(e'))))) + 1) ∈ ℤ))
∧ (v2 = (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))
∨ (∃e2:{e1:E| e1 ≤loc e' }
∃z6:ℤ
∃z7:Cmd
(new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e1;e2) < z6
∧ (((header(e2) = ``new_23_sig retry`` ∈ Name)
∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd)
∧ (<<z1, z6>, z7> = msgval(e2) ∈ (ℤ × ℤ × Cmd)))
∨ ((header(e2) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd × Id)
∧ (<<z1, z6>, z7> = (fst(msgval(e2))) ∈ (ℤ × ℤ × Cmd))))
∧ (no new_23_sig_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, z6> between e2 and e')
∧ ((header(e') = ``new_23_sig vote`` ∈ Name) ∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id))
∧ (↑(new_23_sig_newvote(Cmd) <z1, z6> msgval(e') new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')\000C))
∧ (||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| = (coeff * flrs) ∈ ℤ)
∧ (delay = 0 ∈ ℤ)
∧ (¬((fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e\000C')))];snd(fst(msgval(e')))))) = ((coeff * flrs) + 1) ∈ ℤ))
∧ (loc(e) = loc(e') ∈ Id)
∧ msg-authentic(info(e)) = ff
∧ ((v3 = (fst(fst(fst(msgval(e'))))) ∈ ℤ) ∧ (v4 = ((snd(fst(fst(msgval(e'))))) + 1) ∈ ℤ))
∧ (v2 = (snd(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e\000C2;e')))];snd(fst(msgval(e')))))) ∈ Cmd)))
⊢ ↓∃e':E. ((e' < e) ∧ <v3, v2> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'))
BY
{ (D (-1) THEN ExRepD) }
1
1. Cmd : {T:Type| valueall-type(T)}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : {2...}
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. (f propose) = (ℤ × Cmd) ∈ Type
12. (f notify) = (ℤ × Cmd) ∈ Type
13. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
14. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
15. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
16. f ∈ Name ─→ Type
17. es : EO+(Message(f))
18. new_23_sig_message-constraint{i:l}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;f)@i'
19. e : E@i
20. ∀e1:E
((e1 < e)
⇒ ((∀v:ℤ × Cmd
(v ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e1)
⇒ (↓∃e':E. ((e' < e1) ∧ v ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))
∧ (∀v:ℤ × ℤ × Cmd × Id
(v ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e1)
⇒ (↓∃e':E
((e' < e1) ∧ <fst(fst(fst(v))), snd(fst(v))> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))
∧ (∀v:ℤ × ℤ × Cmd
(v ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e1)
⇒ (↓∃e':E. ((e' < e1) ∧ <fst(fst(v)), snd(v)> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))
∧ (∀e2:E
(e2 c≤ e1
⇒ (∀n,rnd:ℤ. ∀c:Cmd.
((c ∈ fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>;es.e2;e1)))
⇒ (↓∃e':E. ((e' < e1) ∧ <n, c> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))))))
21. ∀v:ℤ × Cmd
(v ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e)
⇒ (↓∃e':E. ((e' < e) ∧ v ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'))))
22. ∀v:ℤ × ℤ × Cmd × Id
(v ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e)
⇒ (↓∃e':E. ((e' < e) ∧ <fst(fst(fst(v))), snd(fst(v))> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'))))
23. v3 : ℤ@i
24. v4 : ℤ@i
25. v2 : Cmd@i
26. <<v3, v4>, v2> ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e)@i
27. e' : E
28. delay : ℤ
29. (e' < e)
30. loc(e') ↓∈ reps
31. e1 : {e1:E| e1 ≤loc e' }
32. z1 : ℤ
33. z2 : Cmd
34. ((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))
35. ¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1))
36. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e1 and e')
37. (no new_23_sig_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, 0> between e1 and e')
38. header(e') = ``new_23_sig vote`` ∈ Name
39. has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
40. ↑(new_23_sig_newvote(Cmd) <z1, 0> msgval(e') new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))
41. ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))|| = (coeff * flrs) ∈ ℤ
42. delay = 0 ∈ ℤ
43. ¬((fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e')))];\000Csnd(fst(msgval(e')))))) = ((coeff * flrs) + 1) ∈ ℤ)
44. loc(e) = loc(e') ∈ Id
45. msg-authentic(info(e)) = ff
46. v3 = (fst(fst(fst(msgval(e'))))) ∈ ℤ
47. v4 = ((snd(fst(fst(msgval(e'))))) + 1) ∈ ℤ
48. v2 = (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
⊢ ↓∃e':E. ((e' < e) ∧ <v3, v2> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'))
2
1. Cmd : {T:Type| valueall-type(T)}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : {2...}
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. (f propose) = (ℤ × Cmd) ∈ Type
12. (f notify) = (ℤ × Cmd) ∈ Type
13. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
14. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
15. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
16. f ∈ Name ─→ Type
17. es : EO+(Message(f))
18. new_23_sig_message-constraint{i:l}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;f)@i'
19. e : E@i
20. ∀e1:E
((e1 < e)
⇒ ((∀v:ℤ × Cmd
(v ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e1)
⇒ (↓∃e':E. ((e' < e1) ∧ v ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))
∧ (∀v:ℤ × ℤ × Cmd × Id
(v ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e1)
⇒ (↓∃e':E
((e' < e1) ∧ <fst(fst(fst(v))), snd(fst(v))> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))
∧ (∀v:ℤ × ℤ × Cmd
(v ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e1)
⇒ (↓∃e':E. ((e' < e1) ∧ <fst(fst(v)), snd(v)> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))
∧ (∀e2:E
(e2 c≤ e1
⇒ (∀n,rnd:ℤ. ∀c:Cmd.
((c ∈ fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>;es.e2;e1)))
⇒ (↓∃e':E. ((e' < e1) ∧ <n, c> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))))))
21. ∀v:ℤ × Cmd
(v ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e)
⇒ (↓∃e':E. ((e' < e) ∧ v ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'))))
22. ∀v:ℤ × ℤ × Cmd × Id
(v ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e)
⇒ (↓∃e':E. ((e' < e) ∧ <fst(fst(fst(v))), snd(fst(v))> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'))))
23. v3 : ℤ@i
24. v4 : ℤ@i
25. v2 : Cmd@i
26. <<v3, v4>, v2> ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e)@i
27. e' : E
28. delay : ℤ
29. (e' < e)
30. loc(e') ↓∈ reps
31. e1 : {e1:E| e1 ≤loc e' }
32. z1 : ℤ
33. z2 : Cmd
34. ((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))
35. ¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1))
36. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e1 and e')
37. e2 : {e1:E| e1 ≤loc e' }
38. z6 : ℤ
39. z7 : Cmd
40. new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e1;e2) < z6
41. ((header(e2) = ``new_23_sig retry`` ∈ Name)
∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd)
∧ (<<z1, z6>, z7> = msgval(e2) ∈ (ℤ × ℤ × Cmd)))
∨ ((header(e2) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd × Id)
∧ (<<z1, z6>, z7> = (fst(msgval(e2))) ∈ (ℤ × ℤ × Cmd)))
42. (no new_23_sig_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, z6> between e2 and e')
43. header(e') = ``new_23_sig vote`` ∈ Name
44. has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
45. ↑(new_23_sig_newvote(Cmd) <z1, z6> msgval(e') new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))
46. ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| = (coeff * flrs) ∈ ℤ
47. delay = 0 ∈ ℤ
48. ¬((fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))]\000C;snd(fst(msgval(e')))))) = ((coeff * flrs) + 1) ∈ ℤ)
49. loc(e) = loc(e') ∈ Id
50. msg-authentic(info(e)) = ff
51. v3 = (fst(fst(fst(msgval(e'))))) ∈ ℤ
52. v4 = ((snd(fst(fst(msgval(e'))))) + 1) ∈ ℤ
53. v2 = (snd(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')\000C))];snd(fst(msgval(e')))))) ∈ Cmd
⊢ ↓∃e':E. ((e' < e) ∧ <v3, v2> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'))
Latex:
Latex:
1. Cmd : \{T:Type| valueall-type(T)\}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : \{2...\}
6. flrs : \mBbbN{}
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. (f propose) = (\mBbbZ{} \mtimes{} Cmd)
12. (f notify) = (\mBbbZ{} \mtimes{} Cmd)
13. (f ``new\_23\_sig decided``) = (\mBbbZ{} \mtimes{} Cmd)
14. (f ``new\_23\_sig retry``) = (\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)
15. (f ``new\_23\_sig vote``) = (\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)
16. f \mmember{} Name {}\mrightarrow{} Type
17. es : EO+(Message(f))
18. new\_23\_sig\_message-constraint\{i:l\}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;f)@i'
19. e : E@i
20. \mforall{}e1:E
((e1 < e)
{}\mRightarrow{} ((\mforall{}v:\mBbbZ{} \mtimes{} Cmd
(v \mmember{} new\_23\_sig\_decided'base(Cmd;notify;propose;f)(e1)
{}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e1) \mwedge{} v \mmember{} new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e')))))
\mwedge{} (\mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id
(v \mmember{} new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e1)
{}\mRightarrow{} (\mdownarrow{}\mexists{}e':E
((e' < e1)
\mwedge{} <fst(fst(fst(v))), snd(fst(v))> \mmember{}
new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e')))))
\mwedge{} (\mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd
(v \mmember{} new\_23\_sig\_retry'base(Cmd;notify;propose;f)(e1)
{}\mRightarrow{} (\mdownarrow{}\mexists{}e':E
((e' < e1)
\mwedge{} <fst(fst(v)), snd(v)> \mmember{} new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e')))))
\mwedge{} (\mforall{}e2:E
(e2 c\mleq{} e1
{}\mRightarrow{} (\mforall{}n,rnd:\mBbbZ{}. \mforall{}c:Cmd.
((c \mmember{} fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>es.e2;e1)))
{}\mRightarrow{} (\mdownarrow{}\mexists{}e':E
((e' < e1)
\mwedge{} <n, c> \mmember{} new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e')))))))))
21. \mforall{}v:\mBbbZ{} \mtimes{} Cmd
(v \mmember{} new\_23\_sig\_decided'base(Cmd;notify;propose;f)(e)
{}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e) \mwedge{} v \mmember{} new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e'))))
22. \mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id
(v \mmember{} new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e)
{}\mRightarrow{} (\mdownarrow{}\mexists{}e':E
((e' < e)
\mwedge{} <fst(fst(fst(v))), snd(fst(v))> \mmember{} new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e'))))
23. v3 : \mBbbZ{}@i
24. v4 : \mBbbZ{}@i
25. v2 : Cmd@i
26. <<v3, v4>, v2> \mmember{} new\_23\_sig\_retry'base(Cmd;notify;propose;f)(e)@i
27. e' : E
28. delay : \mBbbZ{}
29. (e' < e)
30. loc(e') \mdownarrow{}\mmember{} reps
31. e1 : \{e1:E| e1 \mleq{}loc e' \}
32. z1 : \mBbbZ{}
33. z2 : Cmd
34. ((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))))))
35. \mneg{}\muparrow{}(set-sig-member(slots) z1 new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1))
36. (no new\_23\_sig\_Notify(Cmd;clients;notify;propose;f) z1 between e1 and e')
37. ((no new\_23\_sig\_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, 0> between e1 and e')
\mwedge{} ((header(e') = ``new\_23\_sig vote``) \mwedge{} has-es-info-type(es;e';f;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id))
\mwedge{} (\muparrow{}(new\_23\_sig\_newvote(Cmd) <z1, 0> msgval(e') new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, \000C0>es.e1;e')))
\mwedge{} (||fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>es.e1;e'))|| = (coeff * flrs))
\mwedge{} (delay = 0)
\mwedge{} (\mneg{}((fst(poss-maj(eq;[snd(fst(msgval(e'))) /
(fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>es.e1;e')))];snd(\000Cfst(msgval(e'))))))
= ((coeff * flrs) + 1)))
\mwedge{} (loc(e) = loc(e'))
\mwedge{} msg-authentic(info(e)) = ff
\mwedge{} ((v3 = (fst(fst(fst(msgval(e')))))) \mwedge{} (v4 = ((snd(fst(fst(msgval(e'))))) + 1)))
\mwedge{} (v2
= (snd(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'))))))))
\mvee{} (\mexists{}e2:\{e1:E| e1 \mleq{}loc e' \}
\mexists{}z6:\mBbbZ{}
\mexists{}z7:Cmd
(new\_23\_sig\_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e1;e2) < z6
\mwedge{} (((header(e2) = ``new\_23\_sig retry``)
\mwedge{} has-es-info-type(es;e2;f;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)
\mwedge{} (<<z1, z6>, z7> = 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{} (<<z1, z6>, z7> = (fst(msgval(e2))))))
\mwedge{} (no new\_23\_sig\_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, z6> between e2 and e')
\mwedge{} ((header(e') = ``new\_23\_sig vote``) \mwedge{} has-es-info-type(es;e';f;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id))
\mwedge{} (\muparrow{}(new\_23\_sig\_newvote(Cmd) <z1, z6> msgval(e') new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;\000Cf;<z1, z6>es.e2;e')))
\mwedge{} (||fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e2;e'))|| = (coeff * flrs)\000C)
\mwedge{} (delay = 0)
\mwedge{} (\mneg{}((fst(poss-maj(eq;[snd(fst(msgval(e'))) /
(fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e2;e'))\000C)];snd(fst(msgval(e'))))))
= ((coeff * flrs) + 1)))
\mwedge{} (loc(e) = loc(e'))
\mwedge{} msg-authentic(info(e)) = ff
\mwedge{} ((v3 = (fst(fst(fst(msgval(e')))))) \mwedge{} (v4 = ((snd(fst(fst(msgval(e'))))) + 1)))
\mwedge{} (v2
= (snd(poss-maj(eq;[snd(fst(msgval(e'))) /
(fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e2;e')))\000C];snd(fst(msgval(e')))))))))
\mvdash{} \mdownarrow{}\mexists{}e':E. ((e' < e) \mwedge{} <v3, v2> \mmember{} new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e'))
By
Latex:
(D (-1) THEN ExRepD)
Home
Index