### Nuprl Lemma : int-decr-map-find-not-in

`∀[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)].`
`  int-decr-map-find(k;m) = (inr ⋅ ) ∈ (Value?) supposing (∀p∈m.¬(k = (fst(p)) ∈ ℤ))`

Proof

Definitions occuring in Statement :  int-decr-map-find: `int-decr-map-find(k;m)` int-decr-map-type: `int-decr-map-type(Value)` l_all: `(∀x∈L.P[x])` it: `⋅` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` pi1: `fst(t)` not: `¬A` unit: `Unit` inr: `inr x ` union: `left + right` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Lemmas :  nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf l_all_wf2 l_member_wf not_wf equal-wf-base-T l-ordered_wf gt_wf equal-wf-T-base colength_wf_list list-cases it_wf nil_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 int_subtype_base subtract_wf not-ge-2 less-iff-le minus-minus add-swap subtype_base_sq set_subtype_base l_all_cons l-ordered-cons find-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_wf int-decr-map-type_wf
\mforall{}[Value:Type].  \mforall{}[k:\mBbbZ{}].  \mforall{}[m:int-decr-map-type(Value)].
int-decr-map-find(k;m)  =  (inr  \mcdot{}  )  supposing  (\mforall{}p\mmember{}m.\mneg{}(k  =  (fst(p))))

Date html generated: 2015_07_17-AM-08_22_56
Last ObjectModification: 2015_04_02-PM-05_44_02

Home Index