Nuprl Lemma : lookup-list-map-isEmpty-prop
∀[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[m:lookup-list-map-type(Key;Value)].
(↑lookup-list-map-isEmpty(m) ⇐⇒ ∀k:Key. (¬↑lookup-list-map-inDom(deqKey;k;m)))
Proof
Definitions occuring in Statement :
lookup-list-map-isEmpty: lookup-list-map-isEmpty(m),
lookup-list-map-inDom: lookup-list-map-inDom(deqKey;key;m),
lookup-list-map-type: lookup-list-map-type(Key;Value),
deq: EqDecider(T),
assert: ↑b,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
universe: Type
Lemmas :
list_induction,
iff_wf,
assert_wf,
lookup-list-map-isEmpty_wf,
all_wf,
not_wf,
lookup-list-map-inDom_wf,
list_wf,
lookup-list-map-type_wf,
deq_wf,
null_nil_lemma,
list_ind_nil_lemma,
false_wf,
true_wf,
null_cons_lemma,
cons_wf_listp,
listp_wf,
list_ind_cons_lemma,
bor_wf,
eqof_wf,
or_wf,
equal_wf,
not_over_or,
iff_transitivity,
iff_weakening_uiff,
assert_of_bor,
safe-assert-deq
\mforall{}[Key,Value:Type]. \mforall{}[deqKey:EqDecider(Key)]. \mforall{}[m:lookup-list-map-type(Key;Value)].
(\muparrow{}lookup-list-map-isEmpty(m) \mLeftarrow{}{}\mRightarrow{} \mforall{}k:Key. (\mneg{}\muparrow{}lookup-list-map-inDom(deqKey;k;m)))
Date html generated:
2015_07_17-AM-08_23_58
Last ObjectModification:
2015_04_02-PM-05_44_56
Home
Index