Proof of Nuprl Lemma : new_23_sig

Step * 1 4 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. ∀v:ℤ × ℤ × Cmd
(v ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e)
⇒ (↓∃e':E. ((e' < e) ∧ <fst(fst(v)), snd(v)> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'))))
24. e1 : E@i
25. e1 c≤ e@i
26. n : ℤ@i
27. rnd : ℤ@i
28. c : Cmd@i
29. (c ∈ fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>;es.e1;e)))@i
⊢ ↓∃e':E. ((e' < e) ∧ <n, c> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'))
BY
{ (D (-1)

   THEN (InstLemma `new_23_sig_quorum_invariant_fun` [⌈Cmd⌉;⌈notify⌉;⌈propose⌉;⌈f⌉;⌈es.e1⌉;⌈e⌉;⌈<n, rnd>⌉]⋅ THENA Auto)

   THEN (InstLemma `new_23_sig_quorum_inv_vote_fun` [⌈Cmd⌉;⌈notify⌉;⌈propose⌉;⌈f⌉;⌈es.e1⌉;⌈e⌉;⌈<n, rnd>⌉;⌈i⌉]⋅

         THENA Auto
         )
   THEN SquashExRepD

   THEN (SimpleSubstTerm ⌈fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>;es.e1;e))[i]⌉ (-1)⋅ THENA Auto)

   THEN All(\i.(RW EoForwardC i THENA Auto))⋅
   THEN All(\i.(RW EoForwardBaseC i THENA Auto))⋅
   THEN InstHyp [⌈e'⌉] 20⋅
   THEN Auto

   THEN (InstHyp [⌈<<<n, rnd>, c>, snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>;es.e1;e))[i]>⌉] (-3)⋅ THE\000CNA Auto)

   THEN AllReduce
   THEN SquashExRepD
   THEN D 0
   THEN InstConcl [⌈e'@0⌉]⋅
   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 : \{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. \mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd (v \mmember{} new\_23\_sig\_retry'base(Cmd;notify;propose;f)(e) {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E ((e' < e) \mwedge{} <fst(fst(v)), snd(v)> \mmember{} new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e')))) 24. e1 : E@i 25. e1 c\mleq{} e@i 26. n : \mBbbZ{}@i 27. rnd : \mBbbZ{}@i 28. c : Cmd@i 29. (c \mmember{} fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>es.e1;e)))@i \mvdash{} \mdownarrow{}\mexists{}e':E. ((e' < e) \mwedge{} <n, c> \mmember{} new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e')) By Latex: (D (-1) 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{}<n , rnd >\mkleeneclose{}]\mcdot{} THENA Auto ) THEN (InstLemma `new\_23\_sig\_quorum\_inv\_vote\_fun` [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}notify\mkleeneclose{};\mkleeneopen{}propose\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es.e1\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}<n , rnd >\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}] \mcdot{} THENA Auto ) THEN SquashExRepD THEN (SimpleSubstTerm \mkleeneopen{}fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>es.e1;e))[i]\mkleeneclose{} (-\000C1)\mcdot{} THENA Auto) THEN All(\mbackslash{}i.(RW EoForwardC i THENA Auto))\mcdot{} THEN All(\mbackslash{}i.(RW EoForwardBaseC i THENA Auto))\mcdot{} THEN InstHyp [\mkleeneopen{}e'\mkleeneclose{}] 20\mcdot{} THEN Auto THEN (InstHyp [\mkleeneopen{}<<<n, rnd>, c>, snd(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>es.e1;e\000C))[i]>\mkleeneclose{}] (-3)\mcdot{} THENA Auto) THEN AllReduce THEN SquashExRepD THEN D 0 THEN InstConcl [\mkleeneopen{}e'@0\mkleeneclose{}]\mcdot{} THEN Auto) Home Index