Proof of Nuprl Lemma : new_23_sig_decided

Step * 2 2 2 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. new_23_sig_message-constraint{i:l}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;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. e2 : {e1:E| e1 ≤loc e' }
34. z6 : ℤ
35. z7 : Cmd
36. new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e1;e2) < z6
37. ((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)))
38. (no new_23_sig_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, z6> between e2 and e')
39. header(e') = ``new_23_sig vote`` ∈ Name
40. has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
41. z1 = (fst(fst(fst(msgval(e'))))) ∈ ℤ
42. z6 = (snd(fst(fst(msgval(e'))))) ∈ ℤ
43. ¬(snd(msgval(e')) ∈ snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))
44. ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| = (coeff * flrs) ∈ ℤ
45. delay = 0 ∈ ℤ

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

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

50. c = (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

51. (∀z∈[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))].z = c ∈ Cmd)

52. no_repeats(Id;[snd(msgval(e')) / (snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))])

53. ||[snd(msgval(e')) / (snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))]|| = ((coeff * flrs) +\000C 1) ∈ ℤ

54. msgval(e') ∈ ℤ × ℤ × Cmd × Id
55. no_repeats(Id;snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))

56. ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| = ||fst(new_23_sig_QuorumStateFun(Cmd;not\000Cify;propose;f;<z1, z6>;es.e2;e'))|| ∈ ℤ

57. vtr : Id@i
58. (vtr ∈ snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))

⊢ ↓∃e'@0:E. mk-msg-interface(loc(e');make-Msg(``new_23_sig vote``;<<<n, z6>, c>, vtr>)) ∈ new_23_sig_main()(e'@0)

{ ((InstLemma `new_23_sig_quorum_inv_vote_fun` [⌈Cmd⌉;⌈notify⌉;⌈propose⌉;⌈f⌉;⌈es.e2⌉;⌈e'⌉;⌈<z1, z6>⌉]⋅ THENA Auto)

   THEN D (-2)
   THEN (InstHyp [⌈i⌉] (-1)⋅ THENA Auto)
   THEN SquashExRepD
   THEN (RevHypSubst (-5) (-1) THENA Auto)
   THEN OnSomeHyp(\h.((RWO "l_all_iff" h THENA Auto)

                      THEN (InstHyp [⌈fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))[i]⌉] (h)⋅

                            THENA (Try (((RW ListC 0 THENA Auto) THEN (At ⌈Type⌉ OrRight⋅ THENA Auto) THEN GenListD 0))

                                   THEN Complete (Auto)
                                   )
                            )
                      ))⋅
   THEN (HypSubst (-1) (-2) THENA Auto)
   THEN (RW (SweepUpC EoForwardBaseC) (-2) THENA Auto)
   THEN (UseMessageConstraint' (-2) THENA Auto)
   THEN D 0
   THEN (InstConcl [⌈e3⌉]⋅ THENA Auto)
   THEN All(\i.RW (SweepUpC EoForwardC) i THENA Auto)
   THEN (Subst ⌈loc(e'@0) = loc(e') ∈ Id⌉ (-1)⋅ THENA Auto)
   THEN Unfold `mk-msg-interface` 0

   THEN (Subst' ⌈d1 = 0 ∈ ℤ⌉ (-1)⋅ THENA ((RewriteWithILF (-1) THENA Auto) THEN SquashExRepD THEN Auto))

   THEN (Subst' ⌈msg-authentic(info(e'@0)) = ff⌉ (-1)⋅
         THENA ((RewriteWithILF (-1) THENA Auto) THEN SquashExRepD THEN Auto)
         )
   THEN All (RepUR  ``make-Msg mk-msg``)
   THEN Auto) }

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. new\_23\_sig\_message-constraint\{i:l\}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;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. e2 : \{e1:E| e1 \mleq{}loc e' \} 34. z6 : \mBbbZ{} 35. z7 : Cmd 36. new\_23\_sig\_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e1;e2) < z6 37. ((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))))) 38. (no new\_23\_sig\_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, z6> between e2 and e') 39. header(e') = ``new\_23\_sig vote`` 40. has-es-info-type(es;e';f;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id) 41. z1 = (fst(fst(fst(msgval(e'))))) 42. z6 = (snd(fst(fst(msgval(e'))))) 43. \mneg{}(snd(msgval(e')) \mmember{} snd(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e2;e'))) 44. ||fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e2;e'))|| = (coeff * flrs) 45. delay = 0 46. (fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e2;e')))];snd(\000Cfst(msgval(e')))))) = ((coeff * flrs) + 1) 47. loc(e) \mdownarrow{}\mmember{} reps 48. msg-authentic(info(e)) = ff 49. n = (fst(fst(fst(msgval(e'))))) 50. c = (snd(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e2;e')))];snd(fs\000Ct(msgval(e')))))) 51. (\mforall{}z\mmember{}[snd(fst(msgval(e'))) / (fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e2;e\000C')))].z = c) 52. no\_repeats(Id;[snd(msgval(e')) / (snd(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es\000C.e2;e')))]) 53. ||[snd(msgval(e')) / (snd(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e2;e')))]||\000C = ((coeff * flrs) + 1) 54. msgval(e') \mmember{} \mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id 55. no\_repeats(Id;snd(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e2;e'))) 56. ||snd(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e2;e'))|| = ||fst(new\_23\_sig\_Qu\000CorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e2;e'))|| 57. vtr : Id@i 58. (vtr \mmember{} snd(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e2;e'))) \mvdash{} \mdownarrow{}\mexists{}e'@0:E. mk-msg-interface(loc(e');make-Msg(``new\_23\_sig vote``;<<<n, z6>, c>, vtr>)) \mmember{} new\_23\_sig\000C\_main()(e'@0) By Latex: ((InstLemma `new\_23\_sig\_quorum\_inv\_vote\_fun` [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}notify\mkleeneclose{};\mkleeneopen{}propose\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es.e2\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{};\mkleeneopen{}<z1, z6>\mkleeneclose{}]\mcdot{} THENA Auto ) THEN D (-2) THEN (InstHyp [\mkleeneopen{}i\mkleeneclose{}] (-1)\mcdot{} THENA Auto) THEN SquashExRepD THEN (RevHypSubst (-5) (-1) THENA Auto) THEN OnSomeHyp(\mbackslash{}h.((RWO "l\_all\_iff" h THENA Auto) THEN (InstHyp [\mkleeneopen{}fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e\000C2;e'))[i]\mkleeneclose{}] (h)\mcdot{} THENA (Try (((RW ListC 0 THENA Auto) THEN (At \mkleeneopen{}Type\mkleeneclose{} OrRight\mcdot{} THENA Auto) THEN GenListD 0)) THEN Complete (Auto) ) ) ))\mcdot{} THEN (HypSubst (-1) (-2) THENA Auto) THEN (RW (SweepUpC EoForwardBaseC) (-2) THENA Auto) THEN (UseMessageConstraint' (-2) THENA Auto) THEN D 0 THEN (InstConcl [\mkleeneopen{}e3\mkleeneclose{}]\mcdot{} THENA Auto) THEN All(\mbackslash{}i.RW (SweepUpC EoForwardC) i THENA Auto) THEN (Subst \mkleeneopen{}loc(e'@0) = loc(e')\mkleeneclose{} (-1)\mcdot{} THENA Auto) THEN Unfold `mk-msg-interface` 0 THEN (Subst' \mkleeneopen{}d1 = 0\mkleeneclose{} (-1)\mcdot{} THENA ((RewriteWithILF (-1) THENA Auto) THEN SquashExRepD THEN Auto)) THEN (Subst' \mkleeneopen{}msg-authentic(info(e'@0)) = ff\mkleeneclose{} (-1)\mcdot{} THENA ((RewriteWithILF (-1) THENA Auto) THEN SquashExRepD THEN Auto) ) THEN All (RepUR ``make-Msg mk-msg``) THEN Auto) Home Index