Nuprl Lemma : mu_ex_v5_HandleLeaveCS_wf

[initial_token,proc1,proc2:Id].  (mu_ex_v5_HandleLeaveCS(initial_token;proc1;proc2)  Id  EClass'(Id  Message))


Proof not projected



Definitions occuring in Statement :  mu_ex_v5_HandleLeaveCS: mu_ex_v5_HandleLeaveCS(initial_token;proc1;proc2),  Message: Message,  eclass: EClass(A[eo; e]),  Id: Id,  uall: [x:A]. B[x],  member: t  T,  function: x:A  B[x],  product: x:A  B[x]
Definitions :  uall: [x:A]. B[x],  member: t  T,  mu_ex_v5_HandleLeaveCS: mu_ex_v5_HandleLeaveCS(initial_token;proc1;proc2),  let: let,  spreadn: spread3,  all: x:A. B[x],  prop:
Lemmas :  simple-loc-comb-2_wf,  Message_wf,  unit_wf2,  bool_wf,  Id_wf,  concat-lifting-loc-2_wf,  ifthenelse-wf,  band_wf,  bag_wf,  single-bag_wf,  mu_ex_v5_send_token_wf,  mu_ex_v5_getOtherProc_wf,  it_wf,  assert_wf,  empty-bag_wf,  not_wf,  mu_ex_v5_LeaveCS_wf,  mu_ex_v5_PrState_wf
\mforall{}[initial$_{token}$,proc1,proc2:Id].
    (mu\_ex\_v5\_HandleLeaveCS(initial$_{token}$;proc1;proc2)  \mmember{}  Id  {}\mrightarrow{}  EClass'(Id  \mtimes{}  Me\000Cssage))


Date html generated: 2012_02_20-PM-06_56_29
Last ObjectModification: 2012_02_02-PM-02_59_27

Home Index