---

Step * of Lemma lookup-list-map-update-prop

∀[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key2:Key]. ∀[val:Value]. ∀[m:lookup-list-map-type(Key;Value)].
∀[key1:Key].
  (lookup-list-map-find(deqKey;key1;lookup-list-map-update(deqKey;key2;val;m))
  = if deqKey key1 key2 then inl val else lookup-list-map-find(deqKey;key1;m) fi 
  ∈ (Value?))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``lookup-list-map-type`` (-2) THEN ListInd (-2) THEN Try (CpltAuto)) }

1
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-update(deqKey;key2;val;[]))
= if deqKey key1 key2 then inl val else lookup-list-map-find(deqKey;key1;[]) fi 
∈ (Value?)

2
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?)

---

Latex:

---

Latex:
\mforall{}[Key,Value:Type].  \mforall{}[deqKey:EqDecider(Key)].  \mforall{}[key2:Key].  \mforall{}[val:Value].
\mforall{}[m:lookup-list-map-type(Key;Value)].  \mforall{}[key1:Key].
    (lookup-list-map-find(deqKey;key1;lookup-list-map-update(deqKey;key2;val;m))
    =  if  deqKey  key1  key2  then  inl  val  else  lookup-list-map-find(deqKey;key1;m)  fi  )


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``lookup-list-map-type``  (-2)  THEN  ListInd  (-2)  THEN  Try  (CpltAuto))

---

Home Index