Nuprl Lemma : lookup-list-map-update_wf

[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key]. ∀[val:Value]. ∀[m:lookup-list-map-type(Key;Value)].
  (lookup-list-map-update(deqKey;key;val;m) ∈ lookup-list-map-type(Key;Value))


Proof




Definitions occuring in Statement :  lookup-list-map-update: lookup-list-map-update(deqKey;key;val;m) lookup-list-map-type: lookup-list-map-type(Key;Value) deq: EqDecider(T) uall: [x:A]. B[x] member: t ∈ T universe: Type
Lemmas :  update-alist_wf list_wf lookup-list-map-type_wf deq_wf
\mforall{}[Key,Value:Type].  \mforall{}[deqKey:EqDecider(Key)].  \mforall{}[key:Key].  \mforall{}[val:Value].
\mforall{}[m:lookup-list-map-type(Key;Value)].
    (lookup-list-map-update(deqKey;key;val;m)  \mmember{}  lookup-list-map-type(Key;Value))



Date html generated: 2015_07_17-AM-08_24_01
Last ObjectModification: 2015_04_02-PM-05_44_58

Home Index