### Nuprl Lemma : int-decr-map-find-prop2

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

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])` assert: `↑b` isl: `isl(x)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` pi1: `fst(t)` not: `¬A` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Lemmas :  int-decr-map-find_wf not_wf assert_wf null_wf3 subtype_rel_list top_wf l_member_wf squash_wf l_all_wf2 equal-wf-base-T int_subtype_base true_wf sq_stable__l_all sq_stable__not set_wf select_wf sq_stable__le int_seg_wf length_wf false_wf equal_wf int-decr-map-type_wf isl_wf
\mforall{}[Value:Type].  \mforall{}[k:\mBbbZ{}].  \mforall{}[m:int-decr-map-type(Value)].
(\mforall{}p\mmember{}m.\mneg{}(k  =  (fst(p))))  supposing  \mneg{}\muparrow{}isl(int-decr-map-find(k;m))

Date html generated: 2015_07_17-AM-08_22_54
Last ObjectModification: 2015_04_02-PM-05_44_00

Home Index