Nuprl Lemma : hdataflow_subtype

[A1,B1,A2,B2:Type].  (hdataflow(A1;B1) ⊆hdataflow(A2;B2)) supposing ((B1 ⊆B2) and (A2 ⊆A1))


Definitions occuring in Statement :  hdataflow: hdataflow(A;B) uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a hdataflow: hdataflow(A;B) so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] implies:  Q subtype_rel: A ⊆B

\mforall{}[A1,B1,A2,B2:Type].    (hdataflow(A1;B1)  \msubseteq{}r  hdataflow(A2;B2))  supposing  ((B1  \msubseteq{}r  B2)  and  (A2  \msubseteq{}r  A1))

Date html generated: 2016_05_16-AM-10_37_37
Last ObjectModification: 2015_12_28-PM-07_45_28

Theory : halting!dataflow

Home Index