Nuprl Lemma : pv11_p1_acc_state_from_p2a_fun

∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ⟶ ℤ.
∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀c:Cmd.
  (Inj(Id;ℤ;ldrs_uid)
  ⇒ (<b, s, c> ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e)))
  ⇒ (↓∃e':E
        ∃l:Id
         (e' ≤loc e 
         ∧ <l, b, s, c> ∈ pv11_p1_p2a'base(Cmd;f)(e')
         ∧ (b = (fst(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e'))) ∈ pv11_p1_Ballot_Num())
         ∧ (∀e'':E
              (e' ≤loc e''  ⇒ e'' ≤loc e  ⇒ (<b, s, c> ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e''))))))))


Proof



Definitions occuring in Statement :  pv11_p1_AcceptorStateFun: pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;mf;es;e),  pv11_p1_p2a'base: pv11_p1_p2a'base(Cmd;mf),  pv11_p1_headers_type: pv11_p1_headers_type{i:l}(Cmd),  pv11_p1_Ballot_Num: pv11_p1_Ballot_Num(),  Message: Message(f),  classrel: v ∈ X(e),  event-ordering+: EO+(Info),  es-le: e ≤loc e' ,  es-E: E,  Id: Id,  l_member: (x ∈ l),  inject: Inj(A;B;f),  vatype: ValueAllType,  pi1: fst(t),  pi2: snd(t),  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  squash: ↓T,  implies: P ⇒ Q,  and: P ∧ Q,  function: x:A ⟶ B[x],  pair: <a, b>,  product: x:A × B[x],  int: ℤ,  equal: s = t ∈ T
Definitions unfolded in proof :  vatype: ValueAllType,  all: ∀x:A. B[x],  implies: P ⇒ Q,  pv11_p1_headers_type: pv11_p1_headers_type{i:l}(Cmd),  l_all: (∀x∈L.P[x]),  and: P ∧ Q,  member: t ∈ T,  uall: ∀[x:A]. B[x],  so_lambda: λ2x.t[x],  subtype_rel: A ⊆r B,  prop: ℙ,  so_apply: x[s],  iff: P ⇐⇒ Q,  listp: A List+,  name: Name,  int_seg: {i..j-},  lelt: i ≤ j < k,  le: A ≤ B,  less_than': less_than'(a;b),  false: False,  not: ¬A,  less_than: a < b,  squash: ↓T,  length: ||as||,  list_ind: list_ind,  pv11_p1_headers: pv11_p1_headers(),  cons: [a / b],  nil: [],  it: ⋅,  true: True,  select: L[n],  subtract: n - m,  uimplies: b supposing a,  guard: {T},  rev_implies: P ⇐ Q,  pv11_p1_headers_fun: pv11_p1_headers_fun(Cmd),  name_eq: name_eq(x;y),  name-deq: NameDeq,  list-deq: list-deq(eq),  band: p ∧b q,  ifthenelse: if b then t else f fi ,  atom-deq: AtomDeq,  eq_atom: x =a y,  bfalse: ff,  btrue: tt,  null: null(as),  top: Top
Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}f:pv11\_p1\_headers\_type\{i:l\}(Cmd).  \mforall{}es:EO+(Message(f)).  \mforall{}e:E.  \mforall{}ldrs$_\mbackslash{}ff7\000Cbuid}$:Id  {}\mrightarrow{}  \mBbbZ{}.
\mforall{}b:pv11\_p1\_Ballot\_Num().  \mforall{}s:\mBbbZ{}.  \mforall{}c:Cmd.
    (Inj(Id;\mBbbZ{};ldrs$_{uid}$)
    {}\mRightarrow{}  (<b,  s,  c>  \mmember{}  snd(pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es;e)))
    {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E
                \mexists{}l:Id
                  (e'  \mleq{}loc  e 
                  \mwedge{}  <l,  b,  s,  c>  \mmember{}  pv11\_p1\_p2a'base(Cmd;f)(e')
                  \mwedge{}  (b  =  (fst(pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es;e'))))
                  \mwedge{}  (\mforall{}e'':E
                            (e'  \mleq{}loc  e'' 
                            {}\mRightarrow{}  e''  \mleq{}loc  e 
                            {}\mRightarrow{}  (<b,  s,  c>  \mmember{}  snd(pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es\000C;e''))))))))


Date html generated: 2016_05_17-PM-03_58_47
Last ObjectModification: 2016_01_18-AM-11_15_19

Theory : paxos!synod


Home Index