Nuprl Lemma : parallel-class-program_wf
∀[Info,B:Type].
∀[X,Y:EClass(B)]. ∀[Xpr:LocalClass(X)]. ∀[Ypr:LocalClass(Y)]. (Xpr || Ypr ∈ LocalClass(X || Y))
supposing valueall-type(B)
Proof
Definitions occuring in Statement :
parallel-class-program: X || Y,
parallel-class: X || Y,
local-class: LocalClass(X),
eclass: EClass(A[eo; e]),
valueall-type: valueall-type(T),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
member: t ∈ T,
universe: Type
Lemmas :
hdataflow_wf,
bag_wf,
valueall-type-has-valueall,
bag-valueall-type,
bag-append_wf,
evalall-reduce,
bag-subtype-list,
bag-append-empty,
hdf-ap_wf,
iterate-hdataflow_wf,
hdf-halt_wf,
iterate-hdf-halt,
subtype_rel_list,
top_wf,
iff_weakening_equal,
pi2_wf,
squash_wf,
true_wf,
list_wf,
hdf-parallel-halt-right,
empty_bag_append_lemma
Latex:
\mforall{}[Info,B:Type].
\mforall{}[X,Y:EClass(B)]. \mforall{}[Xpr:LocalClass(X)]. \mforall{}[Ypr:LocalClass(Y)]. (Xpr || Ypr \mmember{} LocalClass(X || Y))
supposing valueall-type(B)
Date html generated:
2015_07_22-PM-00_03_50
Last ObjectModification:
2015_02_04-PM-05_10_36
Home
Index