Nuprl Lemma : lookup-list-map-inDom-prop
∀[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key]. ∀[m:lookup-list-map-type(Key;Value)].
(↑lookup-list-map-inDom(deqKey;key;m) ⇐⇒ ↑isl(lookup-list-map-find(deqKey;key;m)))
Proof
Definitions occuring in Statement :
lookup-list-map-inDom: lookup-list-map-inDom(deqKey;key;m),
lookup-list-map-find: lookup-list-map-find(deqKey;key;m),
lookup-list-map-type: lookup-list-map-type(Key;Value),
deq: EqDecider(T),
assert: ↑b,
isl: isl(x),
uall: ∀[x:A]. B[x],
iff: P ⇐⇒ Q,
universe: Type
Lemmas :
list_ind_nil_lemma,
false_wf,
list_ind_cons_lemma,
apply_alist_cons_lemma,
bool_wf,
eqtt_to_assert,
safe-assert-deq,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
true_wf,
assert_wf,
isl_wf,
unit_wf2,
apply-alist_wf,
Error :list_ind_wf,
bfalse_wf,
bor_wf,
list_wf,
lookup-list-map-find_wf,
lookup-list-map-inDom_wf,
iff_wf
\mforall{}[Key,Value:Type]. \mforall{}[deqKey:EqDecider(Key)]. \mforall{}[key:Key]. \mforall{}[m:lookup-list-map-type(Key;Value)].
(\muparrow{}lookup-list-map-inDom(deqKey;key;m) \mLeftarrow{}{}\mRightarrow{} \muparrow{}isl(lookup-list-map-find(deqKey;key;m)))
Date html generated:
2015_07_17-AM-08_23_50
Last ObjectModification:
2015_04_02-PM-05_44_46
Home
Index