Nuprl Lemma : pv11_p1_acc_state_from_p2a

∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ⟶ ℤ.
∀v:pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List). ∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀c:Cmd.
  (Inj(Id;ℤ;ldrs_uid)
  ⇒ v ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e)
  ⇒ let bnum,accepted = v 
     in (<b, s, c> ∈ accepted)
        ⇒ (↓∃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_AcceptorState: pv11_p1_AcceptorState(Cmd;ldrs_uid;mf),  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),  list: T List,  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],  spread: spread def,  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),  strongwellfounded: SWellFounded(R[x; y]),  exists: ∃x:A. B[x],  nat: ℕ,  ge: i ≥ j ,  satisfiable_int_formula: satisfiable_int_formula(fmla),  top: Top,  decidable: Dec(P),  or: P ∨ Q,  pv11_p1_p1a'base: pv11_p1_p1a'base(Cmd;mf),  encodes-msg-type: hdr encodes T,  pv11_p1_p2a'base: pv11_p1_p2a'base(Cmd;mf),  uiff: uiff(P;Q),  bnot: ¬bb,  assert: ↑b,  so_apply: x[s1;s2],  bool: 𝔹,  unit: Unit,  sq_type: SQType(T),  pv11_p1_AcceptorState: pv11_p1_AcceptorState(Cmd;ldrs_uid;mf),  pv11_p1_on_p1a: pv11_p1_on_p1a(Cmd;ldrs_uid),  pv11_p1_init_acceptor: pv11_p1_init_acceptor(Cmd),  pi1: fst(t),  pi2: snd(t),  pv11_p1_init_accepted: pv11_p1_init_accepted(Cmd),  pv11_p1_on_p2a: pv11_p1_on_p2a(Cmd;ldrs_uid),  let: let,  bl-exists: (∃x∈L.P[x])_b,  cand: A c∧ B,  so_lambda: λ2x y.t[x; y],  bor: p ∨bq,  has-es-info-type: has-es-info-type(es;e;f;T),  es-le: e ≤loc e' ,  pv11_p1_add_if_new: pv11_p1_add_if_new(),  append: as @ bs,  so_lambda: so_lambda(x,y,z.t[x; y; z]),  so_apply: x[s1;s2;s3],  Id: Id,  pv11_p1_Ballot_Num: pv11_p1_Ballot_Num()
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{}v:pv11\_p1\_Ballot\_Num()  \mtimes{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List).  \mforall{}b:pv11\_p1\_Ballot\_Num().  \mforall{}s:\mBbbZ{}.
\mforall{}c:Cmd.
    (Inj(Id;\mBbbZ{};ldrs$_{uid}$)
    {}\mRightarrow{}  v  \mmember{}  pv11\_p1\_AcceptorState(Cmd;ldrs$_{uid}$;f)(e)
    {}\mRightarrow{}  let  bnum,accepted  =  v 
          in  (<b,  s,  c>  \mmember{}  accepted)
                {}\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}\mbackslash{}ff2\000C4;f;es;e''))))))))


Date html generated: 2016_05_17-PM-03_58_05
Last ObjectModification: 2016_01_18-AM-11_25_10

Theory : paxos!synod


Home Index