Nuprl Lemma : processChoose_wf2
∀[l_comm:Id]. (processChoose(l_comm) ∈ pi-process())
Proof
Definitions occuring in Statement :
processChoose: processChoose(l_comm),
pi-process: pi-process(),
Id: Id,
uall: ∀[x:A]. B[x],
member: t ∈ T
Lemmas :
nil_wf,
nat_wf,
rec-process_wf_pi_simple_state,
list_wf,
subtype_rel_wf,
pi-process_wf,
pDVrequest?_wf,
bool_wf,
eqtt_to_assert,
deq-member_wf,
nat-deq_wf,
pDVrequest-counter_wf,
assert-deq-member,
make-lg_wf_dag,
Com_wf,
piM_wf,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
l_member_wf,
cons_wf,
mk-tagged_wf_pCom_msg,
PiDataVal_wf,
Process_wf,
subtype_rel_transitivity,
pDVselex_wf,
pDVrequest-rndv2_wf,
subtype_rel_self,
name_wf,
pi_prefix_wf,
unit_wf2,
Id_wf
Latex:
\mforall{}[l$_{comm}$:Id]. (processChoose(l$_{comm}$) \mmember{} pi-process())
Date html generated:
2015_07_23-AM-11_36_34
Last ObjectModification:
2015_01_29-AM-07_40_17
Home
Index