---

Step * of Lemma lookup-list-map-add-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-add(deqKey;key2;val;m))
  = if (deqKey key1 key2) ∧b (¬blookup-list-map-inDom(deqKey;key2;m))
    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-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?)

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

---

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-add(deqKey;key2;val;m))
    =  if  (deqKey  key1  key2)  \mwedge{}\msubb{}  (\mneg{}\msubb{}lookup-list-map-inDom(deqKey;key2;m))
        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