Nuprl Lemma : hdf-halt_wf
∀[A,B:Type]. (hdf-halt() ∈ hdataflow(A;B))
Proof
Definitions occuring in Statement :
hdf-halt: hdf-halt(),
hdataflow: hdataflow(A;B),
uall: ∀[x:A]. B[x],
member: t ∈ T,
universe: Type
Lemmas :
it_wf,
subtype-corec1,
bag_wf,
subtype_rel_sum,
subtype_rel_function,
subtype_rel_simple_product,
subtype_rel_wf
\mforall{}[A,B:Type]. (hdf-halt() \mmember{} hdataflow(A;B))
Date html generated:
2015_07_17-AM-08_04_43
Last ObjectModification:
2015_01_27-PM-00_16_39
Home
Index