Proof of Nuprl Lemma : new_23_sig

Step * 1 1 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. v1 : ℤ@i
22. v2 : Cmd@i
23. <v1, v2> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e)@i
24. e' : E
25. delay : ℤ
26. (e' < e)
27. loc(e') ↓∈ reps
28. e1 : {e1:E| e1 ≤loc e' }
29. z1 : ℤ
30. z2 : Cmd

31. ((header(e1) = propose ∈ Name) ∧ has-es-info-type(es;e1;f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e1) ∈ (ℤ × Cmd)))

∧ (↑(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')))];snd\000C(fst(msgval(e')))))) = ((coeff * flrs) + 1) ∈ ℤ)

∧ loc(e) ↓∈ reps
∧ msg-authentic(info(e)) = ff
∧ (v1 = (fst(fst(fst(msgval(e'))))) ∈ ℤ)

∧ (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) ↓∈ reps
      ∧ msg-authentic(info(e)) = ff
      ∧ (v1 = (fst(fst(fst(msgval(e'))))) ∈ ℤ)

      ∧ (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) ∧ <v1, v2> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'))
BY
{ (D (-1)
   THEN ExRepD
   THEN InstHyp [⌈e'⌉] 20⋅
   THEN Auto
   THEN (InstHyp [⌈msgval(e')⌉] (-3)⋅ THENA Auto)
   THEN Try (Complete ((UseClassRel 0 THEN Auto)))
   THEN SquashExRepD
   THEN (SimpleSubstTerm ⌈fst(fst(fst(msgval(e'))))⌉ (-1)⋅ THENA Auto)) }

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')))))

                    ((c ∈ fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>;es.e2;e1)))

31. ((header(e1) = propose ∈ Name) ∧ has-es-info-type(es;e1;f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e1) ∈ (ℤ × Cmd)))

37. ↑(new_23_sig_newvote(Cmd) <z1, 0> msgval(e') new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))

38. ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e1;e'))|| = (coeff * flrs) ∈ ℤ
39. delay = 0 ∈ ℤ

40. (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) ∈ ℤ

41. loc(e) ↓∈ reps
42. msg-authentic(info(e)) = ff
43. v1 = (fst(fst(fst(msgval(e'))))) ∈ ℤ

44. 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

45. ∀v:ℤ × Cmd
      (v ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e')
      ⇒ (↓∃e'@0:E. ((e'@0 < e') ∧ v ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'@0))))
46. ∀v:ℤ × ℤ × Cmd × Id
      (v ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')
      ⇒ (↓∃e'@0:E

            ((e'@0 < e') ∧ <fst(fst(fst(v))), snd(fst(v))> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'@0))))

47. ∀v:ℤ × ℤ × Cmd
(v ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e')
⇒

 (↓∃e'@0:E. ((e'@0 < e') ∧ <fst(fst(v)), snd(v)> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'@0))))

48. ∀e2:E
      (e2 c≤ e'
      ⇒ (∀n,rnd:ℤ. ∀c:Cmd.
            ((c ∈ fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>;es.e2;e')))
            ⇒ (↓∃e'@0:E. ((e'@0 < e') ∧ <n, c> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'@0))))))
49. e'@0 : E
50. (e'@0 < e')
51. <v1, snd(fst(msgval(e')))> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'@0)
⊢ ↓∃e':E. ((e' < e) ∧ <v1, 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')))))

                    ((c ∈ fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>;es.e2;e1)))

31. ((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))
32. ¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1))
33. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e1 and e')
34. e2 : {e1:E| e1 ≤loc e' }
35. z6 : ℤ
36. z7 : Cmd
37. new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e1;e2) < z6
38. ((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)))
39. (no new_23_sig_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, z6> between e2 and e')
40. header(e') = ``new_23_sig vote`` ∈ Name
41. has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)

42. ↑(new_23_sig_newvote(Cmd) <z1, z6> msgval(e') new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))

43. ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| = (coeff * flrs) ∈ ℤ
44. delay = 0 ∈ ℤ

45. (fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))];s\000Cnd(fst(msgval(e')))))) = ((coeff * flrs) + 1) ∈ ℤ

46. loc(e) ↓∈ reps
47. msg-authentic(info(e)) = ff
48. v1 = (fst(fst(fst(msgval(e'))))) ∈ ℤ

49. 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

50. ∀v:ℤ × Cmd
      (v ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e')
      ⇒ (↓∃e'@0:E. ((e'@0 < e') ∧ v ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'@0))))
51. ∀v:ℤ × ℤ × Cmd × Id
      (v ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')
      ⇒ (↓∃e'@0:E

            ((e'@0 < e') ∧ <fst(fst(fst(v))), snd(fst(v))> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'@0))))

52. ∀v:ℤ × ℤ × Cmd
(v ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e')
⇒

 (↓∃e'@0:E. ((e'@0 < e') ∧ <fst(fst(v)), snd(v)> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'@0))))

53. ∀e2:E
      (e2 c≤ e'
      ⇒ (∀n,rnd:ℤ. ∀c:Cmd.
            ((c ∈ fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>;es.e2;e')))
            ⇒ (↓∃e'@0:E. ((e'@0 < e') ∧ <n, c> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'@0))))))
54. e'@0 : E
55. (e'@0 < e')
56. <v1, snd(fst(msgval(e')))> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'@0)
⊢ ↓∃e':E. ((e' < e) ∧ <v1, 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. v1 : \mBbbZ{}@i 22. v2 : Cmd@i 23. <v1, v2> \mmember{} new\_23\_sig\_decided'base(Cmd;notify;propose;f)(e)@i 24. e' : E 25. delay : \mBbbZ{} 26. (e' < e) 27. loc(e') \mdownarrow{}\mmember{} reps 28. e1 : \{e1:E| e1 \mleq{}loc e' \} 29. z1 : \mBbbZ{} 30. z2 : Cmd 31. ((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)))))) 32. \mneg{}\muparrow{}(set-sig-member(slots) z1 new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1)) 33. (no new\_23\_sig\_Notify(Cmd;clients;notify;propose;f) z1 between e1 and e') 34. ((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{} ((fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>es.e1;e')))];snd(fs\000Ct(msgval(e')))))) = ((coeff * flrs) + 1)) \mwedge{} loc(e) \mdownarrow{}\mmember{} reps \mwedge{} msg-authentic(info(e)) = ff \mwedge{} (v1 = (fst(fst(fst(msgval(e')))))) \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{} ((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) \mdownarrow{}\mmember{} reps \mwedge{} msg-authentic(info(e)) = ff \mwedge{} (v1 = (fst(fst(fst(msgval(e')))))) \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{} <v1, v2> \mmember{} new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e')) By Latex: (D (-1) THEN ExRepD THEN InstHyp [\mkleeneopen{}e'\mkleeneclose{}] 20\mcdot{} THEN Auto THEN (InstHyp [\mkleeneopen{}msgval(e')\mkleeneclose{}] (-3)\mcdot{} THENA Auto) THEN Try (Complete ((UseClassRel 0 THEN Auto))) THEN SquashExRepD THEN (SimpleSubstTerm \mkleeneopen{}fst(fst(fst(msgval(e'))))\mkleeneclose{} (-1)\mcdot{} THENA Auto)) Home Index