---

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


1. Key : Type
2. Value : Type
3. deqKey : EqDecider(Key)
4. key2 : Key
5. key1 : Key
6. u : Key × Value@i
7. v : (Key × Value) List@i
8. lookup-list-map-find(deqKey;key1;lookup-list-map-remove(deqKey;key2;v))
= if deqKey key1 key2 then inr ⋅  else lookup-list-map-find(deqKey;key1;v) fi 
∈ (Value?)@i
⊢ lookup-list-map-find(deqKey;key1;lookup-list-map-remove(deqKey;key2;[u / v]))
= if deqKey key1 key2 then inr ⋅  else lookup-list-map-find(deqKey;key1;[u / v]) fi 
∈ (Value?)
BY
{ (DProds
   THEN RepUR ``lookup-list-map-remove remove-alist`` 0
   THEN Fold `remove-alist` 0
   THEN Fold `lookup-list-map-remove` 0
   THEN RepUR ``lookup-list-map-find`` 0
   THEN Fold `lookup-list-map-find` 0) }

1
1. Key : Type
2. Value : Type
3. deqKey : EqDecider(Key)
4. key2 : Key
5. key1 : Key
6. u1 : Key@i
7. u2 : Value@i
8. v : (Key × Value) List@i
9. lookup-list-map-find(deqKey;key1;lookup-list-map-remove(deqKey;key2;v))
= if deqKey key1 key2 then inr ⋅  else lookup-list-map-find(deqKey;key1;v) fi 
∈ (Value?)@i
⊢ lookup-list-map-find(deqKey;key1;if deqKey u1 key2
then lookup-list-map-remove(deqKey;key2;v)
else [<u1, u2> / lookup-list-map-remove(deqKey;key2;v)]
fi )
= if deqKey key1 key2 then inr ⋅ 
  if eqof(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.  key1  :  Key
6.  u  :  Key  \mtimes{}  Value@i
7.  v  :  (Key  \mtimes{}  Value)  List@i
8.  lookup-list-map-find(deqKey;key1;lookup-list-map-remove(deqKey;key2;v))
=  if  deqKey  key1  key2  then  inr  \mcdot{}    else  lookup-list-map-find(deqKey;key1;v)  fi  @i
\mvdash{}  lookup-list-map-find(deqKey;key1;lookup-list-map-remove(deqKey;key2;[u  /  v]))
=  if  deqKey  key1  key2  then  inr  \mcdot{}    else  lookup-list-map-find(deqKey;key1;[u  /  v])  fi 


By

---

Latex:
(DProds
  THEN  RepUR  ``lookup-list-map-remove  remove-alist``  0
  THEN  Fold  `remove-alist`  0
  THEN  Fold  `lookup-list-map-remove`  0
  THEN  RepUR  ``lookup-list-map-find``  0
  THEN  Fold  `lookup-list-map-find`  0)

---

Home Index