Nuprl Lemma : new_23_sig-decided
∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ].
∀[notify,propose:Atom List]. ∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[auth:𝔹].
∀[k:ℤ]. ∀[v:Cmd].
  (<d, i, mk-msg(auth;``new_23_sig decided``;<k, v>)> ∈ new_23_sig_main()(e)
  
⇐⇒ loc(e) ↓∈ reps
      ∧ (↓∃e':{e':E| e' ≤loc e } 
           ∃z1:ℤ
            ∃z2:Cmd
             (((((header(e') = propose ∈ Name) ∧ has-es-info-type(es;e';f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e') ∈ (ℤ × Cmd))\000C)
              ∨ ((header(e') = ``new_23_sig vote`` ∈ Name)
                ∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
                ∧ (z1 = (fst(fst(fst(msgval(e'))))) ∈ ℤ)
                ∧ (z2 = (snd(fst(msgval(e')))) ∈ Cmd)))
              ∧ (¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))
             ∧ (no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e' and e)
             ∧ (((no new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <z1, 0> between e' 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.\000Ce';e)))
               ∧ (||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>es.e';e))|| = (coeff * flrs) ∈ ℤ)
               ∧ (d = 0 ∈ ℤ)
               ∧ ((fst(poss-maj(cmdeq;[snd(fst(msgval(e))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>\000C;es.e';e)))];snd(fst(msgval(e)))))) = ((coeff * flrs) + 1) ∈ ℤ)
               ∧ i ↓∈ reps
               ∧ auth = ff
               ∧ (k = (fst(fst(fst(msgval(e))))) ∈ ℤ)
               ∧ (v
                 = (snd(poss-maj(cmdeq;[snd(fst(msgval(e))) / 
                                        (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>es.e';e)))];snd(fst(\000Cmsgval(e))))))
                 ∈ Cmd))
               ∨ (∃e1:{e1:E| e1 ≤loc e } 
                   ∃z6:ℤ
                    ∃z7:Cmd
                     (new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e';e1) < z6
                     ∧ (((header(e1) = ``new_23_sig retry`` ∈ Name)
                       ∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd)
                       ∧ (<<z1, z6>, z7> = msgval(e1) ∈ (ℤ × ℤ × Cmd)))
                       ∨ ((header(e1) = ``new_23_sig vote`` ∈ Name)
                         ∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
                         ∧ (<<z1, z6>, z7> = (fst(msgval(e1))) ∈ (ℤ × ℤ × Cmd))))
                     ∧ (no new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <z1, z6> 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, z6> msgval(e) new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1,\000C z6>es.e1;e)))
                     ∧ (||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e1;e))|| = (coeff * flrs) ∈ ℤ)
                     ∧ (d = 0 ∈ ℤ)
                     ∧ ((fst(poss-maj(cmdeq;[snd(fst(msgval(e))) / 
                                             (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e1;e)))];sn\000Cd(fst(msgval(e))))))
                       = ((coeff * flrs) + 1)
                       ∈ ℤ)
                     ∧ i ↓∈ reps
                     ∧ auth = ff
                     ∧ (k = (fst(fst(fst(msgval(e))))) ∈ ℤ)
                     ∧ (v
                       = (snd(poss-maj(cmdeq;[snd(fst(msgval(e))) / 
                                              (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e1;e)))];s\000Cnd(fst(msgval(e))))))
                       ∈ Cmd)))))))
Proof
Definitions occuring in Statement : 
new_23_sig_main: new_23_sig_main()
, 
new_23_sig_ReplicaStateFun: new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)
, 
new_23_sig_Notify: new_23_sig_Notify(Cmd;clients;notify;propose;f)
, 
new_23_sig_NewRoundsStateFun: new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;x;es;e)
, 
new_23_sig_Quorum: new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f)
, 
new_23_sig_QuorumStateFun: new_23_sig_QuorumStateFun(Cmd;notify;propose;f;x;es;e)
, 
new_23_sig_newvote: new_23_sig_newvote(Cmd)
, 
new_23_sig_headers_type: new_23_sig_headers_type{i:l}(Cmd;notify;propose)
, 
set-sig-member: set-sig-member(s)
, 
set-sig: set-sig{i:l}(Item)
, 
msg-interface: Interface
, 
mk-msg: mk-msg(auth;hdr;val)
, 
es-info-body: msgval(e)
, 
has-es-info-type: has-es-info-type(es;e;f;T)
, 
es-header: header(e)
, 
Message: Message(f)
, 
no-classrel-in-interval: (no X between start and e)
, 
classrel: v ∈ X(e)
, 
eo-forward: eo.e
, 
event-ordering+: EO+(Info)
, 
es-le: e ≤loc e' 
, 
es-loc: loc(e)
, 
es-E: E
, 
Id: Id
, 
name: Name
, 
poss-maj: poss-maj(eq;L;x)
, 
length: ||as||
, 
cons: [a / b]
, 
nil: []
, 
list: T List
, 
deq: EqDecider(T)
, 
valueall-type: valueall-type(T)
, 
assert: ↑b
, 
bfalse: ff
, 
bool: 𝔹
, 
less_than: a < b
, 
uall: ∀[x:A]. B[x]
, 
pi1: fst(t)
, 
pi2: snd(t)
, 
exists: ∃x:A. B[x]
, 
iff: P 
⇐⇒ Q
, 
not: ¬A
, 
squash: ↓T
, 
or: P ∨ Q
, 
and: P ∧ Q
, 
set: {x:A| B[x]} 
, 
apply: f a
, 
pair: <a, b>
, 
product: x:A × B[x]
, 
multiply: n * m
, 
add: n + m
, 
natural_number: $n
, 
int: ℤ
, 
token: "$token"
, 
atom: Atom
, 
universe: Type
, 
equal: s = t ∈ T
, 
bag-member: x ↓∈ bs
, 
bag: bag(T)
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
new_23_sig_headers_type: new_23_sig_headers_type{i:l}(Cmd;notify;propose)
, 
name: Name
, 
subtype_rel: A ⊆r B
, 
vatype: ValueAllType
, 
prop: ℙ
, 
and: P ∧ Q
, 
listp: A List+
, 
implies: P 
⇒ Q
, 
sq_stable: SqStable(P)
, 
l_all: (∀x∈L.P[x])
, 
all: ∀x:A. B[x]
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s]
, 
iff: P 
⇐⇒ Q
, 
new_23_sig_headers: new_23_sig_headers(notify;propose)
, 
rev_implies: P 
⇐ Q
, 
guard: {T}
, 
or: P ∨ Q
, 
uimplies: b supposing a
, 
new_23_sig_headers_fun: new_23_sig_headers_fun(Cmd;notify;propose)
, 
bool: 𝔹
, 
unit: Unit
, 
it: ⋅
, 
btrue: tt
, 
uiff: uiff(P;Q)
, 
ifthenelse: if b then t else f fi 
, 
cand: A c∧ B
, 
new_23_sig_headers_no_rep: new_23_sig_headers_no_rep(notify;propose)
, 
squash: ↓T
, 
no_repeats: no_repeats(T;l)
, 
nat: ℕ
, 
le: A ≤ B
, 
less_than': less_than'(a;b)
, 
false: False
, 
not: ¬A
, 
length: ||as||
, 
list_ind: list_ind, 
cons: [a / b]
, 
nil: []
, 
less_than: a < b
, 
true: True
, 
ge: i ≥ j 
, 
satisfiable_int_formula: satisfiable_int_formula(fmla)
, 
exists: ∃x:A. B[x]
, 
top: Top
, 
select: L[n]
, 
subtract: n - m
, 
bfalse: ff
, 
sq_type: SQType(T)
, 
bnot: ¬bb
, 
assert: ↑b
, 
name_eq: name_eq(x;y)
, 
name-deq: NameDeq
, 
list-deq: list-deq(eq)
, 
band: p ∧b q
, 
atom-deq: AtomDeq
, 
eq_atom: x =a y
, 
null: null(as)
, 
bag-member: x ↓∈ bs
, 
make-msg-interface: make-msg-interface(i;l;m)
, 
classrel: v ∈ X(e)
, 
has-es-info-type: has-es-info-type(es;e;f;T)
, 
pi1: fst(t)
, 
pi2: snd(t)
, 
equal-info-body: v = body(e)
, 
hint: hint(t)
Latex:
\mforall{}[Cmd:\{T:Type|  valueall-type(T)\}  ].  \mforall{}[clients:bag(Id)].  \mforall{}[cmdeq:EqDecider(Cmd)].  \mforall{}[coeff,flrs:\mBbbZ{}].
\mforall{}[notify,propose:Atom  List].  \mforall{}[reps:bag(Id)].  \mforall{}[slots:set-sig\{i:l\}(\mBbbZ{})].
\mforall{}[f:new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose)].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].  \mforall{}[d:\mBbbZ{}].
\mforall{}[i:Id].  \mforall{}[auth:\mBbbB{}].  \mforall{}[k:\mBbbZ{}].  \mforall{}[v:Cmd].
    (<d,  i,  mk-msg(auth;``new\_23\_sig  decided``;<k,  v>)>  \mmember{}  new\_23\_sig\_main()(e)
    \mLeftarrow{}{}\mRightarrow{}  loc(e)  \mdownarrow{}\mmember{}  reps
            \mwedge{}  (\mdownarrow{}\mexists{}e':\{e':E|  e'  \mleq{}loc  e  \} 
                      \mexists{}z1:\mBbbZ{}
                        \mexists{}z2:Cmd
                          (((((header(e')  =  propose)
                            \mwedge{}  has-es-info-type(es;e';f;\mBbbZ{}  \mtimes{}  Cmd)
                            \mwedge{}  (<z1,  z2>  =  msgval(e')))
                            \mvee{}  ((header(e')  =  ``new\_23\_sig  vote``)
                                \mwedge{}  has-es-info-type(es;e';f;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)
                                \mwedge{}  (z1  =  (fst(fst(fst(msgval(e'))))))
                                \mwedge{}  (z2  =  (snd(fst(msgval(e')))))))
                            \mwedge{}  (\mneg{}\muparrow{}(set-sig-member(slots)  z1 
                                        new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))
                          \mwedge{}  (no  new\_23\_sig\_Notify(Cmd;clients;notify;propose;f)  z1  between  e'  and  e)
                          \mwedge{}  (((no  new\_23\_sig\_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f)  <z1,  0>  between  e\000C'  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;p\000Cropose;f;<z1,  0>es.e';e)))
                              \mwedge{}  (||fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1,  0>es.e';e))||  =  (coeff  \000C*  flrs))
                              \mwedge{}  (d  =  0)
                              \mwedge{}  ((fst(poss-maj(cmdeq;[snd(fst(msgval(e)))  / 
                                                                              (fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1,  0>e\000Cs.e';e)))];snd(fst(msgval(e))))))
                                  =  ((coeff  *  flrs)  +  1))
                              \mwedge{}  i  \mdownarrow{}\mmember{}  reps
                              \mwedge{}  auth  =  ff
                              \mwedge{}  (k  =  (fst(fst(fst(msgval(e))))))
                              \mwedge{}  (v
                                  =  (snd(poss-maj(cmdeq;[snd(fst(msgval(e)))  / 
                                                                                (fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1,  0>\000Ces.e';e)))];snd(fst(msgval(e))))))))
                              \mvee{}  (\mexists{}e1:\{e1:E|  e1  \mleq{}loc  e  \} 
                                      \mexists{}z6:\mBbbZ{}
                                        \mexists{}z7:Cmd
                                          (new\_23\_sig\_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e';e1)  <  z6
                                          \mwedge{}  (((header(e1)  =  ``new\_23\_sig  retry``)
                                              \mwedge{}  has-es-info-type(es;e1;f;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)
                                              \mwedge{}  (<<z1,  z6>,  z7>  =  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,  z6>,  z7>  =  (fst(msgval(e1))))))
                                          \mwedge{}  (no  new\_23\_sig\_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f)  <z1,  z6>  be\000Ctween  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,  z6>  msgval(e)  new\_23\_sig\_QuorumStateFun(Cmd;n\000Cotify;propose;f;<z1,  z6>es.e1;e)))
                                          \mwedge{}  (||fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1,  z6>es.e1;e))||  =  \000C(coeff  *  flrs))
                                          \mwedge{}  (d  =  0)
                                          \mwedge{}  ((fst(poss-maj(cmdeq;[snd(fst(msgval(e)))  / 
                                                                                          (fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;...;f;<z1
                                                                                                                                                                                          ,  z6
                                                                                                                                                                                          >es.e1\000C;e)))];snd(fst(msgval(e))))))
                                              =  ((coeff  *  flrs)  +  1))
                                          \mwedge{}  i  \mdownarrow{}\mmember{}  reps
                                          \mwedge{}  auth  =  ff
                                          \mwedge{}  (k  =  (fst(fst(fst(msgval(e))))))
                                          \mwedge{}  (v
                                              =  (snd(poss-maj(cmdeq;[snd(fst(msgval(e)))  / 
                                                                                            (fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;...;f;<z1
                                                                                                                                                                                            ,  z6
                                                                                                                                                                                            >es.e\000C1;e)))];snd(fst(msgval(e)))))))))))))
Date html generated:
2016_05_17-PM-02_14_08
Last ObjectModification:
2016_01_18-PM-07_50_49
Theory : 2!3!consensus!with!signatures
Home
Index