Nuprl Lemma : Comm-next-continue_wf
∀[l_comm,l_choose:Id]. ∀[piD:PiDataVal()]. ∀[cSt:Comm-state()].
Comm-next-continue(l_comm;l_choose;piD;cSt) ∈ Comm-output() supposing ↑pDVcontinue?(piD)
Proof
Definitions occuring in Statement :
Comm-next-continue: Comm-next-continue(l_comm;l_choose;piD;cSt),
Comm-output: Comm-output(),
Comm-state: Comm-state(),
pDVcontinue?: pDVcontinue?(x),
PiDataVal: PiDataVal(),
Id: Id,
assert: ↑b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
member: t ∈ T
Lemmas :
list_ind_cons_lemma,
list_ind_nil_lemma,
assert_wf,
pDVcontinue?_wf,
Comm-state_wf,
PiDataVal_wf,
Id_wf,
Comm-waiting_wf,
bool_wf,
eqtt_to_assert,
make-lg_wf_dag,
tag-by_wf,
nil_wf,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
null_wf3,
Comm-process-q_wf,
Comm-q_wf,
Comm-st_wf,
list_wf,
pi_prefix_wf,
fpf_wf,
nat_wf,
name_wf,
subtype_rel_list,
top_wf,
assert_of_null,
Comm-count_wf,
subtype_rel_product,
subtype_rel_self,
equal-wf-T-base,
zero-le-nat,
le_wf,
cons_wf,
mk-tagged_wf2,
pDVcontinue_wf,
map_wf,
pDVrequest_wf
Latex:
\mforall{}[l$_{comm}$,l$_{choose}$:Id]. \mforall{}[piD:PiDataVal()]. \mforall{}[cSt:Com\000Cm-state()].
Comm-next-continue(l$_{comm}$;l$_{choose}$;piD;cSt) \mmember{} Comm\000C-output() supposing \muparrow{}pDVcontinue?(piD)
Date html generated:
2015_07_23-AM-11_58_55
Last ObjectModification:
2015_01_29-AM-07_41_01
Home
Index