---

Step * 2 of Lemma lookup-list-map-update-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-update(deqKey;key2;val;v))
= if deqKey key1 key2 then inl val else lookup-list-map-find(deqKey;key1;v) fi 
∈ (Value?)@i
⊢ lookup-list-map-find(deqKey;key1;lookup-list-map-update(deqKey;key2;val;[u / v]))
= if deqKey key1 key2 then inl val else lookup-list-map-find(deqKey;key1;[u / v]) fi 
∈ (Value?)
BY
{ (DProds
   THEN RepUR ``lookup-list-map-update update-alist`` 0
   THEN Fold `update-alist` 0⋅
   THEN Fold `lookup-list-map-update` 0
   THEN RepUR ``lookup-list-map-find eqof`` 0
   THEN Fold `lookup-list-map-find` 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-update(deqKey;key2;val;v))
= if deqKey key1 key2 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, val> / v]
else [<u1, u2> / lookup-list-map-update(deqKey;key2;val;v)]
fi )
= if deqKey key1 key2 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-update(deqKey;key2;val;v))
=  if  deqKey  key1  key2  then  inl  val  else  lookup-list-map-find(deqKey;key1;v)  fi  @i
\mvdash{}  lookup-list-map-find(deqKey;key1;lookup-list-map-update(deqKey;key2;val;[u  /  v]))
=  if  deqKey  key1  key2  then  inl  val  else  lookup-list-map-find(deqKey;key1;[u  /  v])  fi 


By

---

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

---

Home Index