---

Step * 1 1 of Lemma lookup_fails


1. a : DSet
2. B : Type
3. z : B
4. k : |a|
5. kp : |a|
6. vp : B
7. ps : (|a| × B) List
8. (¬↑(k ∈b map(λx.(fst(x));ps))) ⇒ ((ps[k]) = z ∈ B)
9. ¬((fst(<kp, vp>)) = k ∈ |a|)
10. ¬↑(k ∈b map(λx.(fst(x));ps))
⊢ if kp (=b) k then vp else ps[k] fi  = z ∈ B
BY
{ ((Reduce 9 THENM SplitOnConclITE 
) THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  DSet
2.  B  :  Type
3.  z  :  B
4.  k  :  |a|
5.  kp  :  |a|
6.  vp  :  B
7.  ps  :  (|a|  \mtimes{}  B)  List
8.  (\mneg{}\muparrow{}(k  \mmember{}\msubb{}  map(\mlambda{}x.(fst(x));ps)))  {}\mRightarrow{}  ((ps[k])  =  z)
9.  \mneg{}((fst(<kp,  vp>))  =  k)
10.  \mneg{}\muparrow{}(k  \mmember{}\msubb{}  map(\mlambda{}x.(fst(x));ps))
\mvdash{}  if  kp  (=\msubb{})  k  then  vp  else  ps[k]  fi    =  z


By

---

Latex:
((Reduce  9  THENM  SplitOnConclITE 
)  THEN  Auto)

---

Home Index