Nuprl Lemma : int-decr-map-add_wf

[Value:Type]. ∀[k:ℤ]. ∀[v:Value]. ∀[m:int-decr-map-type(Value)].  (int-decr-map-add(k;v;m) ∈ int-decr-map-type(Value))


Proof




Definitions occuring in Statement :  int-decr-map-add: int-decr-map-add(k;v;m) int-decr-map-type: int-decr-map-type(Value) uall: [x:A]. B[x] member: t ∈ T int: universe: Type
Lemmas :  nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf l-ordered_wf gt_wf equal-wf-T-base colength_wf_list list_wf list-cases true_wf l-ordered-nil-true nil_wf member_wf 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 nat_wf 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 subtype_base_sq set_subtype_base int_subtype_base all_wf l_member_wf l-ordered-cons cons_wf int-decr-map-type_wf list_ind_nil_lemma l-ordered-single insert-combine-cons value-type-has-value int-value-type bool_cases_sqequal eq_int_wf sqequal-tt-to-assert assert_of_eq_int sqequal-ff-to-assert neg_assert_of_eq_int lt_int_wf assert_of_lt_int cons_member set_wf member-insert-combine int-minus-comparison_wf l_exists_iff top_wf comparison_wf and_wf equal_wf
\mforall{}[Value:Type].  \mforall{}[k:\mBbbZ{}].  \mforall{}[v:Value].  \mforall{}[m:int-decr-map-type(Value)].
    (int-decr-map-add(k;v;m)  \mmember{}  int-decr-map-type(Value))



Date html generated: 2015_07_17-AM-08_23_29
Last ObjectModification: 2015_04_02-PM-05_44_27

Home Index