---

Step * 1 of Lemma lookup_fails


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
BY
{ ((RW bool_to_propC 8 
THENM RWH (LemmaC `not_over_or`) 8 
THENM D 8) THENA Auto) 
THEN New [`kp';`vp'] (D 5) 
THEN Reduce 0 }

1
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

---

Latex:

---

Latex:

1.  a  :  DSet
2.  B  :  Type
3.  z  :  B
4.  k  :  |a|
5.  p  :  |a|  \mtimes{}  B
6.  ps  :  (|a|  \mtimes{}  B)  List
7.  (\mneg{}\muparrow{}(k  \mmember{}\msubb{}  map(\mlambda{}x.(fst(x));ps)))  {}\mRightarrow{}  ((ps[k])  =  z)
8.  \mneg{}\muparrow{}(((fst(p))  (=\msubb{})  k)  \mvee{}\msubb{}(k  \mmember{}\msubb{}  map(\mlambda{}x.(fst(x));ps)))
\mvdash{}  ([p  /  ps][k])  =  z


By

---

Latex:
((RW  bool\_to\_propC  8 
THENM  RWH  (LemmaC  `not\_over\_or`)  8 
THENM  D  8)  THENA  Auto) 
THEN  New  [`kp';`vp']  (D  5) 
THEN  Reduce  0

---

Home Index