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