Nuprl Lemma : lookup-list-map-empty-prop
∀[Key:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key]. (¬↑lookup-list-map-inDom(deqKey;key;lookup-list-map-empty()))
Proof
Definitions occuring in Statement :
lookup-list-map-empty: lookup-list-map-empty(),
lookup-list-map-inDom: lookup-list-map-inDom(deqKey;key;m),
deq: EqDecider(T),
assert: ↑b,
uall: ∀[x:A]. B[x],
not: ¬A,
universe: Type
Lemmas :
list_ind_nil_lemma,
false_wf,
deq_wf
\mforall{}[Key:Type]. \mforall{}[deqKey:EqDecider(Key)]. \mforall{}[key:Key].
(\mneg{}\muparrow{}lookup-list-map-inDom(deqKey;key;lookup-list-map-empty()))
Date html generated:
2015_07_17-AM-08_23_54
Last ObjectModification:
2015_04_02-PM-05_44_51
Home
Index