Nuprl Lemma : mu_ex_v4_message-constraint_wf

[cs,initial_token,proc1,proc2:Id].  (mu_ex_v4_message-constraint{i:l}(cs;initial_token;proc1;proc2)  EO'  ')


Proof not projected




Definitions occuring in Statement :  mu_ex_v4_message-constraint: mu_ex_v4_message-constraint{i:l}(cs;initial_token;proc1;proc2) Message: Message event-ordering+: EO+(Info) Id: Id uall: [x:A]. B[x] prop: member: t  T function: x:A  B[x]
Definitions :  uall: [x:A]. B[x] member: t  T mu_ex_v4_message-constraint: mu_ex_v4_message-constraint{i:l}(cs;initial_token;proc1;proc2)
Lemmas :  message-constraint_wf Id_wf Message_wf mu_ex_v4_main_wf mu_ex_v4_headers_no_inputs_wf event-ordering+_wf

\mforall{}[cs,initial$_{token}$,proc1,proc2:Id].
    (mu\_ex\_v4\_message-constraint\{i:l\}(cs;initial$_{token}$;proc1;proc2)  \mmember{}  EO'  {}\mrightarrow{}  \mBbbP{}\000C')


Date html generated: 2012_02_20-PM-06_34_48
Last ObjectModification: 2012_02_02-PM-02_55_19

Home Index