Nuprl Lemma : class-at-program-wf-hdf
∀[A,B:Type]. ∀[pr:Id ─→ hdataflow(A;B)]. ∀[locs:bag(Id)].  (pr)@locs ∈ Id ─→ hdataflow(A;B) supposing valueall-type(B)
Proof
Definitions occuring in Statement : 
class-at-program: (pr)@locs
, 
Id: Id
, 
valueall-type: valueall-type(T)
, 
uimplies: b supposing a
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
function: x:A ─→ B[x]
, 
universe: Type
, 
bag: bag(T)
, 
hdataflow: hdataflow(A;B)
Lemmas : 
bag-deq-member_wf, 
id-deq_wf, 
bool_wf, 
eqtt_to_assert, 
assert-bag-deq-member, 
eqff_to_assert, 
equal_wf, 
bool_cases_sqequal, 
subtype_base_sq, 
bool_subtype_base, 
assert-bnot, 
bag-member_wf, 
hdf-halt_wf, 
valueall-type_wf, 
bag_wf, 
Id_wf, 
hdataflow_wf
Latex:
\mforall{}[A,B:Type].  \mforall{}[pr:Id  {}\mrightarrow{}  hdataflow(A;B)].  \mforall{}[locs:bag(Id)].
    (pr)@locs  \mmember{}  Id  {}\mrightarrow{}  hdataflow(A;B)  supposing  valueall-type(B)
Date html generated:
2015_07_22-PM-00_03_59
Last ObjectModification:
2015_01_28-AM-09_52_28
Home
Index