---

Step * of Lemma mk-lookup-list-map_wf

∀[Key,Value:Type]. ∀[deqKey:EqDecider(Key)].  (mk-lookup-list-map(Key;Value;deqKey) ∈ map-sig{i:l}(Key;Value))
BY
{ (RepUR ``mk-lookup-list-map`` 0 THEN (UnivCD THENA Auto)) }

1
1. Key : Type
2. Value : Type
3. deqKey : EqDecider(Key)
⊢ mk-map(Key;Value;lookup-list-map-type(Key;Value);lookup-list-map-eqKey(deqKey);λk,m. lookup-list-map-find(deqKey;k;m);
         λk,m. lookup-list-map-inDom(deqKey;k;m);lookup-list-map-empty();λm.lookup-list-map-isEmpty(m);
         λk,v,m. lookup-list-map-update(deqKey;k;v;m);λk,v,m. lookup-list-map-add(deqKey;k;v;m);
         λk,m. lookup-list-map-remove(deqKey;k;m)) ∈ map-sig{i:l}(Key;Value)

---

Latex:

---

Latex:
\mforall{}[Key,Value:Type].  \mforall{}[deqKey:EqDecider(Key)].
    (mk-lookup-list-map(Key;Value;deqKey)  \mmember{}  map-sig\{i:l\}(Key;Value))


By

---

Latex:
(RepUR  ``mk-lookup-list-map``  0  THEN  (UnivCD  THENA  Auto))

---

Home Index