---

Step * 2 of Lemma lookup_before_start_a


1. a : QOSet
2. b : AbMon
3. k : |a|
4. u : |a| × |b|
5. v : (|a| × |b|) List
6. (↑(∀bk'(:|a|) ∈ map(λz.(fst(z));v). (k' <b k))) ⇒ ((v[k]) = e ∈ |b|)
⊢ (↑(∀bk'(:|a|) ∈ map(λz.(fst(z));[u / v]). (k' <b k))) ⇒ (([u / v][k]) = e ∈ |b|)
BY
{ D (-3) THEN AbReduce 0 
THEN ((D 0 THENM RW bool_to_propC (-1)) THENA Auto) 
THEN ((SplitOnConclITE) THENA Auto) }

1
.....truecase..... 
1. a : QOSet
2. b : AbMon
3. k : |a|
4. u1 : |a|
5. u2 : |b|
6. v : (|a| × |b|) List
7. (↑(∀bk'(:|a|) ∈ map(λz.(fst(z));v). (k' <b k))) ⇒ ((v[k]) = e ∈ |b|)
8. (u1 <a k) ∧ (↑(∀bk'(:|a|) ∈ map(λz.(fst(z));v). (k' <b k)))
9. u1 = k ∈ |a|
⊢ u2 = e ∈ |b|

2
.....falsecase..... 
1. a : QOSet
2. b : AbMon
3. k : |a|
4. u1 : |a|
5. u2 : |b|
6. v : (|a| × |b|) List
7. (↑(∀bk'(:|a|) ∈ map(λz.(fst(z));v). (k' <b k))) ⇒ ((v[k]) = e ∈ |b|)
8. (u1 <a k) ∧ (↑(∀bk'(:|a|) ∈ map(λz.(fst(z));v). (k' <b k)))
9. ¬(u1 = k ∈ |a|)
⊢ (v[k]) = e ∈ |b|

---

Latex:

---

Latex:

1.  a  :  QOSet
2.  b  :  AbMon
3.  k  :  |a|
4.  u  :  |a|  \mtimes{}  |b|
5.  v  :  (|a|  \mtimes{}  |b|)  List
6.  (\muparrow{}(\mforall{}\msubb{}k'(:|a|)  \mmember{}  map(\mlambda{}z.(fst(z));v).  (k'  <\msubb{}  k)))  {}\mRightarrow{}  ((v[k])  =  e)
\mvdash{}  (\muparrow{}(\mforall{}\msubb{}k'(:|a|)  \mmember{}  map(\mlambda{}z.(fst(z));[u  /  v]).  (k'  <\msubb{}  k)))  {}\mRightarrow{}  (([u  /  v][k])  =  e)


By

---

Latex:
D  (-3)  THEN  AbReduce  0 
THEN  ((D  0  THENM  RW  bool\_to\_propC  (-1))  THENA  Auto) 
THEN  ((SplitOnConclITE)  THENA  Auto)

---

Home Index