Nuprl Lemma : Paxos-spec5-body_wf

[Info:Type]. [es:EO+(Info)]. [T:Type]. [f:]. [acceptors:Id List]. [Reserve:EClass()].
[VoteState:EClass(AcceptorState)]. [Proposal,Accept:EClass(  T)]. [leader:  Id]. [Decide,Input:EClass(T)].
[OK:EClass(Id  )].
  (Paxos-spec5-body{i:l}(Info; es; T; f; acceptors; Reserve; VoteState; Proposal; Accept; leader; Decide; OK; Input)
   )


Proof not projected



Definitions occuring in Statement :  Paxos-spec5-body: Paxos-spec5-body{i:l}(Info; es; T; f; acceptors; Reserve; VoteState; Proposal; Accept; leader; Decide; OK; Input),  paxos-acceptor-state: AcceptorState,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  Id: Id,  nat: ,  uall: [x:A]. B[x],  prop: ,  member: t  T,  function: x:A  B[x],  product: x:A  B[x],  list: type List,  universe: Type
Definitions :  uall: [x:A]. B[x],  nat: ,  member: t  T,  prop: ,  Paxos-spec5-body: Paxos-spec5-body{i:l}(Info; es; T; f; acceptors; Reserve; VoteState; Proposal; Accept; leader; Decide; OK; Input),  and: P  Q,  all: x:A. B[x],  exists: x:A. B[x],  implies: P  Q,  let: let,  or: P  Q,  l_exists: (xL. P[x]),  cand: A c B,  top: Top,  subtype: S  T,  assert: b,  so_lambda: x y.t[x; y],  btrue: tt,  ifthenelse: if b then t else f fi ,  true: True,  so_lambda: x.t[x],  squash: T,  es-E-interface: E(X),  es-first-at: e is first@ i s.t.  e.P[e],  so_apply: x[s1;s2],  uimplies: b supposing a,  sq_type: SQType(T),  guard: {T},  so_apply: x[s]
Lemmas :  length_wf1,  Id_wf,  nat_properties,  no_repeats_wf,  es-E-interface_wf,  es-interface-top,  paxos-acceptor-state_wf,  es-causle_wf,  event-ordering+_inc,  l_member_wf,  es-loc_wf,  eclass-val_wf,  es-E_wf,  subtype_base_sq,  bool_wf,  bool_subtype_base,  paxos-state-reservation_wf,  paxos-state-name_wf,  MaxVote_wf,  paxos-state-info_wf,  pi1_wf_top,  es-first-at_wf,  filter_type,  eq_int_wf,  event-ordering+_wf,  nat_wf,  es-interface-predecessors_wf,  assert_wf,  imax-list_wf,  map_wf,  paxos-state-ballot_wf,  length-map,  es-le_wf,  pi2_wf,  le_wf,  unit_wf,  es-locl_wf,  eclass_wf,  assert_elim,  in-eclass_wf,  squash_wf,  true_wf
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[T:Type].  \mforall{}[f:\mBbbN{}].  \mforall{}[acceptors:Id  List].  \mforall{}[Reserve:EClass(\mBbbN{})].
\mforall{}[VoteState:EClass(AcceptorState)].  \mforall{}[Proposal,Accept:EClass(\mBbbN{}  \mtimes{}  T)].  \mforall{}[leader:\mBbbN{}  {}\mrightarrow{}  Id].
\mforall{}[Decide,Input:EClass(T)].  \mforall{}[OK:EClass(Id  \mtimes{}  \mBbbN{})].
    (Paxos-spec5-body\{i:l\}(Info;
                                                  es;
                                                  T;
                                                  f;
                                                  acceptors;
                                                  Reserve;
                                                  VoteState;
                                                  Proposal;
                                                  Accept;
                                                  leader;
                                                  Decide;
                                                  OK;
                                                  Input)  \mmember{}  \mBbbP{})


Date html generated: 2011_10_20-PM-04_31_13
Last ObjectModification: 2011_06_18-PM-01_58_46

Home Index