Nuprl Lemma : single-valued-class-implies-hdf
∀[Info,A:Type].
∀X:EClass(A). ∀pr:LocalClass(X).
(single-valued-classrel-all{i:l}(Info;A;X) ⇒ (∀i:Id. hdf-single-valued(pr i;Info;A)))
Proof
Definitions occuring in Statement :
local-class: LocalClass(X),
single-valued-classrel-all: single-valued-classrel-all{i:l}(Info;T;X),
eclass: EClass(A[eo; e]),
Id: Id,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
universe: Type,
hdf-single-valued: hdf-single-valued(X;A;B)
Lemmas :
iterate-hdataflow_wf,
hdataflow_wf,
hdataflow-ext,
bag_wf,
unit_wf2,
equal_wf,
hdf-run_wf,
subtype-corec1,
subtype_rel_sum,
subtype_rel_function,
subtype_rel_simple_product,
subtype_rel_wf,
list_wf,
Id_wf,
single-valued-classrel-all_wf,
local-class_wf,
eclass_wf,
es-E_wf,
event-ordering+_subtype,
event-ordering+_wf,
sq_stable__all,
all_wf,
bag-member_wf,
sq_stable__equal,
squash_wf,
hdf-ap_wf,
list2extended-eo,
assert_of_lt_int,
length_wf,
length_nil,
non_neg_length,
nil_wf,
length_wf_nil,
length_wf_nat,
length_cons,
length_append,
subtype_rel_list,
top_wf,
assert_wf,
lt_int_wf,
map_append_sq,
map_cons_lemma,
map_nil_lemma,
general-append-cancellation,
map_wf,
es-info_wf,
es-before_wf,
cons_wf,
length_of_cons_lemma,
reduce_hd_cons_lemma,
hd_wf,
ge_wf,
listp_properties,
cons_wf_listp,
nat_wf,
subtype_base_sq,
atom2_subtype_base,
single-valued-bag_wf,
true_wf,
iff_weakening_equal,
single-valued-classrel-all-implies-bag
Latex:
\mforall{}[Info,A:Type].
\mforall{}X:EClass(A). \mforall{}pr:LocalClass(X).
(single-valued-classrel-all\{i:l\}(Info;A;X) {}\mRightarrow{} (\mforall{}i:Id. hdf-single-valued(pr i;Info;A)))
Date html generated:
2015_07_21-PM-04_47_34
Last ObjectModification:
2015_02_04-PM-05_57_48
Home
Index