Nuprl Lemma : sequence-class-program_wf
∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[Z:EClass(A)]. ∀[xpr:LocalClass(X)]. ∀[ypr:LocalClass(Y)].
∀[zpr:LocalClass(Z)].
sequence-class-program(xpr;ypr;zpr) ∈ LocalClass(sequence-class(X;Y;Z)) supposing valueall-type(A)
Proof
Definitions occuring in Statement :
sequence-class-program: sequence-class-program(xpr;ypr;zpr),
sequence-class: sequence-class(X;Y;Z),
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 :
hdf-sequence_wf,
Id_wf,
bool_wf,
band_wf,
squash_wf,
true_wf,
bnot_bnot_elim,
eq_int_wf,
bag-size_wf,
class-ap_wf,
nat_wf,
bnot_wf,
bag-null_wf,
eqtt_to_assert,
assert-bag-null,
iff_weakening_equal,
null-bag-size,
assert_of_eq_int,
bag_wf,
es-first-event_wf,
es-le_wf,
eo-forward_wf,
member-eo-forward-E,
equal_wf,
es-loc_wf,
hdf-ap_wf,
iterate-hdataflow_wf,
map_wf,
es-info_wf,
es-before_wf,
hdataflow_wf,
es-E_wf,
event-ordering+_subtype,
all_wf,
sequence-class_wf,
valueall-type_wf,
local-class_wf,
eclass_wf,
event-ordering+_wf,
set_wf,
event_ordering_wf,
or_wf,
sq_exists_wf,
assert_wf,
es-locl_wf,
not_wf,
eo-forward-loc,
subtype_base_sq,
atom2_subtype_base,
es-le-loc,
assert_functionality_wrt_uiff,
pi2_wf,
list_wf,
and_wf,
eo-forward-split-before,
length_wf_nat,
append_wf,
subtype_rel_list,
eo-forward-E-subtype,
eo-forward-info,
hdf-halted_wf,
bool_cases_sqequal,
bool_subtype_base,
eqff_to_assert,
assert-bnot,
iff_transitivity,
iff_weakening_uiff,
assert_of_band,
assert_of_bnot,
l_member_wf,
map_append_sq,
iterate-hdf-append,
top_wf,
map_functionality,
mk-hdf_wf,
iseg_member,
member_append,
cons_member,
member-es-before,
iseg_wf,
iseg-es-before-is-before,
cons_wf,
nil_wf,
nat_properties,
less_than_transitivity1,
less_than_irreflexivity,
ge_wf,
less_than_wf,
equal-wf-T-base,
colength_wf_list,
list-cases,
map_nil_lemma,
iter_hdf_nil_lemma,
product_subtype_list,
spread_cons_lemma,
sq_stable__le,
le_antisymmetry_iff,
add_functionality_wrt_le,
add-associates,
add-zero,
zero-add,
le-add-cancel,
decidable__le,
false_wf,
not-le-2,
condition-implies-le,
minus-add,
minus-one-mul,
add-commutes,
le_wf,
subtract_wf,
not-ge-2,
less-iff-le,
minus-minus,
add-swap,
set_subtype_base,
int_subtype_base,
map_cons_lemma,
iter_hdf_cons_lemma,
bfalse_wf,
hdf-ap-run,
hdataflow-ext,
unit_wf2,
hdf-ap-inl,
hdf-run_wf,
bag_null_empty_lemma,
hdf_ap_halt_lemma,
iterate-hdf-halt,
btrue_wf,
hdf-halt_wf,
list_ind_cons_lemma,
cons_iseg,
list_ind_nil_lemma,
nil_iseg,
assert_of_ff,
band_ff_simp,
es-closed-open-interval-eq-before,
es-closed-open-interval-decomp,
es-open-interval_wf,
list_induction,
hdf_halted_inl_red_lemma,
hdf_halted_halt_red_lemma,
empty-bag_wf,
es-closed-open-interval_wf,
es-closed-open-interval-nil,
equal-nil-sq-nil,
member-es-le-before,
iseg-es-le-before-is-before,
iseg_weakening
Latex:
\mforall{}[Info,A,B:Type]. \mforall{}[X:EClass(A)]. \mforall{}[Y:EClass(B)]. \mforall{}[Z:EClass(A)]. \mforall{}[xpr:LocalClass(X)].
\mforall{}[ypr:LocalClass(Y)]. \mforall{}[zpr:LocalClass(Z)].
sequence-class-program(xpr;ypr;zpr) \mmember{} LocalClass(sequence-class(X;Y;Z)) supposing valueall-type(A)
Date html generated:
2015_07_22-PM-00_05_07
Last ObjectModification:
2015_02_04-PM-05_53_48
Home
Index