Nuprl Lemma : mu_ex_v5_strong-message-constraint_wf
[es:EO']. [m1,m2,init,p1,p2:Id]. (mu_ex_v5_strong-message-constraint{i:l}(es;m1;m2;init;p1;p2) 
')
Proof not projected
Definitions occuring in Statement :
mu_ex_v5_strong-message-constraint: mu_ex_v5_strong-message-constraint{i:l}(es;m1;m2;init;p1;p2),
Message: Message,
event-ordering+: EO+(Info),
Id: Id,
uall: [x:A]. B[x],
prop: ,
member: t T
Definitions :
uall: [x:A]. B[x],
member: t T,
mu_ex_v5_strong-message-constraint: mu_ex_v5_strong-message-constraint{i:l}(es;m1;m2;init;p1;p2)
Lemmas :
strong-message-constraint-no-rep_wf,
Error :mu_ex_v5_main_wf,
Error :mu_ex_v5_headers_no_inputs_wf,
Id_wf,
event-ordering+_wf,
Message_wf
\mforall{}[es:EO']. \mforall{}[m1,m2,init,p1,p2:Id].
(mu\_ex\_v5\_strong-message-constraint\{i:l\}(es;m1;m2;init;p1;p2) \mmember{} \mBbbP{}')
Date html generated:
2012_02_20-PM-06_59_35
Last ObjectModification:
2012_02_02-PM-03_01_26
Home
Index