Nuprl Lemma : in-simple-loc-comb-1-concat
∀[Info,A,B:Type]. ∀[f:Id ─→ A ─→ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
(Singlevalued(X) ⇒ (∀i:Id. ∀a:A. (#(f i a) ≤ 1)) ⇒ e ∈b f@(Loc, X) = e ∈b X ∧b (¬bbag-null(f loc(e) X(e))))
Proof
Definitions occuring in Statement :
concat-lifting-loc-1: f@,
simple-loc-comb-1: F(Loc, X),
sv-class: Singlevalued(X),
eclass-val: X(e),
in-eclass: e ∈b X,
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-loc: loc(e),
es-E: E,
Id: Id,
band: p ∧b q,
bnot: ¬bb,
bool: 𝔹,
uall: ∀[x:A]. B[x],
le: A ≤ B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
function: x:A ─→ B[x],
natural_number: $n,
universe: Type,
equal: s = t ∈ T,
bag-size: #(bs),
bag-null: bag-null(bs),
bag: bag(T)
Lemmas :
all_wf,
Id_wf,
le_wf,
bag-size_wf,
nat_wf,
sv-class_wf,
es-E_wf,
event-ordering+_subtype,
event-ordering+_wf,
eclass_wf,
bag_wf,
eq_int_wf,
bool_wf,
eqtt_to_assert,
assert_of_eq_int,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_int,
nequal-le-implies,
equal-wf-base-T,
bag-size-one,
bag-combine-single-left,
single-bag_wf,
es-loc_wf,
eclass-val_wf,
bag-union-single,
bag-subtype-list,
null-bag-size,
iff_imp_equal_bool,
bnot_wf,
equal-wf-T-base,
not_wf,
assert_wf,
iff_wf,
iff_transitivity,
iff_weakening_uiff,
assert_of_bnot,
bag-size-zero,
decidable__le,
false_wf,
not-le-2,
condition-implies-le,
minus-add,
minus-one-mul,
add-swap,
add-associates,
zero-add,
add-commutes,
minus-zero,
add_functionality_wrt_le,
le-add-cancel2,
bag_combine_empty_lemma,
bag_union_empty_lemma,
bag_size_empty_lemma,
bfalse_wf
Latex:
\mforall{}[Info,A,B:Type]. \mforall{}[f:Id {}\mrightarrow{} A {}\mrightarrow{} bag(B)]. \mforall{}[X:EClass(A)]. \mforall{}[es:EO+(Info)]. \mforall{}[e:E].
(Singlevalued(X)
{}\mRightarrow{} (\mforall{}i:Id. \mforall{}a:A. (\#(f i a) \mleq{} 1))
{}\mRightarrow{} e \mmember{}\msubb{} f@(Loc, X) = e \mmember{}\msubb{} X \mwedge{}\msubb{} (\mneg{}\msubb{}bag-null(f loc(e) X(e))))
Date html generated:
2015_07_23-AM-11_29_39
Last ObjectModification:
2015_01_28-PM-11_16_55
Home
Index