---

Step * of Lemma lookup_fails

∀a:DSet. ∀B:Type. ∀z:B. ∀k:|a|. ∀ps:(|a| × B) List.  ((¬↑(k ∈b map(λx.(fst(x));ps))) ⇒ ((ps[k]) = z ∈ B))
BY
{ (InductionOnListA THEN Reduce 0 THEN Auto) }

1
1. a : DSet
2. B : Type
3. z : B
4. k : |a|
5. p : |a| × B
6. ps : (|a| × B) List
7. (¬↑(k ∈b map(λx.(fst(x));ps))) ⇒ ((ps[k]) = z ∈ B)
8. ¬↑(((fst(p)) (=b) k) ∨b(k ∈b map(λx.(fst(x));ps)))
⊢ ([p / ps][k]) = z ∈ B

---

Latex:

---

Latex:
\mforall{}a:DSet.  \mforall{}B:Type.  \mforall{}z:B.  \mforall{}k:|a|.  \mforall{}ps:(|a|  \mtimes{}  B)  List.
    ((\mneg{}\muparrow{}(k  \mmember{}\msubb{}  map(\mlambda{}x.(fst(x));ps)))  {}\mRightarrow{}  ((ps[k])  =  z))


By

---

Latex:
(InductionOnListA  THEN  Reduce  0  THEN  Auto)

---

Home Index