---

Step * 1 of Lemma lookup-list-map-add-prop


1. Key : Type
2. Value : Type
3. deqKey : EqDecider(Key)
4. key2 : Key
5. val : Value
6. key1 : Key
⊢ lookup-list-map-find(deqKey;key1;lookup-list-map-add(deqKey;key2;val;[]))
= if (deqKey key1 key2) ∧b (¬blookup-list-map-inDom(deqKey;key2;[]))
  then inl val
  else lookup-list-map-find(deqKey;key1;[])
  fi 
∈ (Value?)
BY
{ (RepUR ``lookup-list-map-add update-alist lookup-list-map-find eqof apply-alist`` 0 THEN AutoSplit⋅) }

---

Latex:

---

Latex:

1.  Key  :  Type
2.  Value  :  Type
3.  deqKey  :  EqDecider(Key)
4.  key2  :  Key
5.  val  :  Value
6.  key1  :  Key
\mvdash{}  lookup-list-map-find(deqKey;key1;lookup-list-map-add(deqKey;key2;val;[]))
=  if  (deqKey  key1  key2)  \mwedge{}\msubb{}  (\mneg{}\msubb{}lookup-list-map-inDom(deqKey;key2;[]))
    then  inl  val
    else  lookup-list-map-find(deqKey;key1;[])
    fi 


By

---

Latex:
(RepUR  ``lookup-list-map-add  update-alist  lookup-list-map-find  eqof  apply-alist``  0  THEN  AutoSplit\mcdot{})

---

Home Index