---

Step * 2 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
7. u : Key × Value@i
8. v : (Key × Value) List@i
9. lookup-list-map-find(deqKey;key1;lookup-list-map-add(deqKey;key2;val;v))
= if (deqKey key1 key2) ∧b (¬blookup-list-map-inDom(deqKey;key2;v))
  then inl val
  else lookup-list-map-find(deqKey;key1;v)
  fi 
∈ (Value?)@i
⊢ lookup-list-map-find(deqKey;key1;lookup-list-map-add(deqKey;key2;val;[u / v]))
= if (deqKey key1 key2) ∧b (¬blookup-list-map-inDom(deqKey;key2;[u / v]))
  then inl val
  else lookup-list-map-find(deqKey;key1;[u / v])
  fi 
∈ (Value?)
BY
{ (DProds
   THEN RepUR ``lookup-list-map-add update-alist`` 0
   THEN Fold `update-alist` 0⋅
   THEN Fold `lookup-list-map-add` 0
   THEN RepUR ``lookup-list-map-find eqof`` 0
   THEN Fold `lookup-list-map-find` 0
   THEN RepUR ``lookup-list-map-inDom`` 0
   THEN Fold `lookup-list-map-inDom` 0) }

1
1. Key : Type
2. Value : Type
3. deqKey : EqDecider(Key)
4. key2 : Key
5. val : Value
6. key1 : Key
7. u1 : Key@i
8. u2 : Value@i
9. v : (Key × Value) List@i
10. lookup-list-map-find(deqKey;key1;lookup-list-map-add(deqKey;key2;val;v))
= if (deqKey key1 key2) ∧b (¬blookup-list-map-inDom(deqKey;key2;v))
  then inl val
  else lookup-list-map-find(deqKey;key1;v)
  fi 
∈ (Value?)@i
⊢ lookup-list-map-find(deqKey;key1;if deqKey u1 key2
then [<key2, u2> / v]
else [<u1, u2> / lookup-list-map-add(deqKey;key2;val;v)]
fi )
= if (deqKey key1 key2) ∧b (¬b((deqKey key2 u1) ∨blookup-list-map-inDom(deqKey;key2;v))) then inl val
  if deqKey u1 key1 then inl u2
  else lookup-list-map-find(deqKey;key1;v)
  fi 
∈ (Value?)

---

Latex:

---

Latex:

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


By

---

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

---

Home Index