Nuprl Lemma : processComm_wf2
∀[l_comm,l_choose:Id]. (processComm(l_comm;l_choose) ∈ pi-process())
Proof
Definitions occuring in Statement :
processComm: processComm(l_comm;l_choose),
pi-process: pi-process(),
Id: Id,
uall: ∀[x:A]. B[x],
member: t ∈ T
Lemmas :
rec-process_wf_pi_simple_state,
Comm-state_wf,
fpf-empty_wf,
list_wf,
pi_prefix_wf,
nil_wf,
bfalse_wf,
false_wf,
le_wf,
subtype_rel_wf,
pi-process_wf,
pDVguards?_wf,
bool_wf,
eqtt_to_assert,
subtype_rel_tagged+_general,
tag-by_wf,
PiDataVal_wf,
tagged+_wf,
tag-case_wf,
Id_wf,
unit_wf2,
tag-by-subtype-tag-case,
Comm-next-guards_wf,
subtype_rel_product,
ldag_wf,
Com_wf,
piM_wf,
subtype_rel-ldag,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
pDVselex?_wf,
Comm-next-selex_wf,
pDVcontinue?_wf,
Comm-next-continue_wf,
make-lg_wf_dag,
subtype_rel_self,
not_wf,
true_wf
Latex:
\mforall{}[l$_{comm}$,l$_{choose}$:Id]. (processComm(l$_\mbackslash{}ff7\000Cbcomm}$;l$_{choose}$) \mmember{} pi-process())
Date html generated:
2015_07_23-AM-11_58_59
Last ObjectModification:
2015_01_29-AM-07_41_04
Home
Index