Nuprl Lemma : dataflow-program-cumulativity

[A:']. (DataflowProgram(A) r dataflow-program{i':l}(A))


Proof not projected



Definitions occuring in Statement :  dataflow-program: DataflowProgram(A),  subtype_rel: A r B,  uall: [x:A]. B[x],  universe: Type
Definitions :  implies: P  Q,  prop: ,  so_lambda: x.t[x],  all: x:A. B[x],  member: t  T,  dataflow-program: DataflowProgram(A),  uall: [x:A]. B[x],  so_apply: x[s],  uimplies: b supposing a
Lemmas :  subtype_rel_self,  subtype_rel_sets,  bag_wf,  unit_wf2,  valueall-type_wf,  subtype_rel_product
\mforall{}[A:\mBbbU{}'].  (DataflowProgram(A)  \msubseteq{}r  dataflow-program\{i':l\}(A))


Date html generated: 2012_01_23-AM-11_58_17
Last ObjectModification: 2011_12_12-PM-05_11_28

Home Index