Nuprl Lemma : mk-map-int-decr_wf
∀[Value:Type]. (mk-map-int-decr(Value) ∈ map-sig{i:l}(ℤ;Value))
Proof
Definitions occuring in Statement :
mk-map-int-decr: mk-map-int-decr(Value),
map-sig: map-sig{i:l}(Key;Value),
uall: ∀[x:A]. B[x],
member: t ∈ T,
int: ℤ,
universe: Type
Definitions :
member: t ∈ T,
bool: 𝔹,
unit: Unit,
int-decr-map-inDom: int-decr-map-inDom(k;m),
isl: isl(x),
int-decr-map-find: int-decr-map-find(k;m),
find-combine: find-combine(cmp;l),
int-decr-map-empty: int-decr-map-empty(),
nil: [],
it: ⋅,
bfalse: ff
Lemmas :
mk-map_wf,
set-valueall-type,
list_wf,
l-ordered_wf,
gt_wf,
list-valueall-type,
product-valueall-type,
int-valueall-type,
equal-wf-base,
base_wf,
valueall-type_wf,
assert_of_eq_int,
assert_wf,
all_wf,
iff_wf,
int_subtype_base,
int-decr-map-find-wf,
int-decr-map-type_wf,
int-decr-map-inDom_wf,
isl_wf,
not_wf,
null_wf3,
subtype_rel_list,
top_wf,
l_member_wf,
squash_wf,
l_all_wf2,
equal-wf-base-T,
int-decr-map-find_wf,
int-decr-map-empty-prop,
int-decr-map-isEmpty-prop,
int-decr-map-update-prop,
equal_wf,
unit_wf2,
eq_int_wf,
bool_wf,
eqtt_to_assert,
eqff_to_assert,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_int,
int-decr-map-add-prop,
bnot_wf,
iff_transitivity,
iff_weakening_uiff,
assert_of_band,
assert_of_bnot,
int-decr-map-remove-prop,
it_wf
\mforall{}[Value:Type]. (mk-map-int-decr(Value) \mmember{} map-sig\{i:l\}(\mBbbZ{};Value))
Date html generated:
2015_07_17-AM-08_23_40
Last ObjectModification:
2015_04_16-AM-00_25_53
Home
Index