---

Step * 2 of Lemma lookup-list-map-isEmpty-prop


1. Key : Type
2. Value : Type
3. deqKey : EqDecider(Key)
4. u : Key × Value@i
5. v : (Key × Value) List@i
6. ↑lookup-list-map-isEmpty(v) ⇐⇒ ∀k:Key. (¬↑lookup-list-map-inDom(deqKey;k;v))@i
⊢ ↑lookup-list-map-isEmpty([u / v]) ⇐⇒ ∀k:Key. (¬↑lookup-list-map-inDom(deqKey;k;[u / v]))
BY
{ (RepUR ``lookup-list-map-isEmpty`` 0 THEN RepeatFor 2 (D 0) THEN Try (CpltAuto)) }

1
1. Key : Type
2. Value : Type
3. deqKey : EqDecider(Key)
4. u : Key × Value@i
5. v : (Key × Value) List@i
6. ↑lookup-list-map-isEmpty(v) ⇐⇒ ∀k:Key. (¬↑lookup-list-map-inDom(deqKey;k;v))@i
7. ∀k:Key. (¬↑lookup-list-map-inDom(deqKey;k;[u / v]))@i
⊢ False

---

Latex:

---

Latex:

1.  Key  :  Type
2.  Value  :  Type
3.  deqKey  :  EqDecider(Key)
4.  u  :  Key  \mtimes{}  Value@i
5.  v  :  (Key  \mtimes{}  Value)  List@i
6.  \muparrow{}lookup-list-map-isEmpty(v)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}k:Key.  (\mneg{}\muparrow{}lookup-list-map-inDom(deqKey;k;v))@i
\mvdash{}  \muparrow{}lookup-list-map-isEmpty([u  /  v])  \mLeftarrow{}{}\mRightarrow{}  \mforall{}k:Key.  (\mneg{}\muparrow{}lookup-list-map-inDom(deqKey;k;[u  /  v]))


By

---

Latex:
(RepUR  ``lookup-list-map-isEmpty``  0  THEN  RepeatFor  2  (D  0)  THEN  Try  (CpltAuto))

---

Home Index