---

Step * of Lemma lookup_oal_inj

∀a:LOSet. ∀b:AbDMon. ∀k,k':|a|. ∀v:|b|.  ((inj(k,v)[k']) = (when k (=b) k'. v) ∈ |b|)
BY
{ ((RepD THENM Unfold `oal_inj` 0 
THENM SplitOnConclITE 
THENM Reduce 0) THENA Auto) }

1
1. a : LOSet
2. b : AbDMon
3. k : |a|
4. k' : |a|
5. v : |b|
6. v = e ∈ |b|
⊢ e = (when k (=b) k'. v) ∈ |b|

2
1. a : LOSet
2. b : AbDMon
3. k : |a|
4. k' : |a|
5. v : |b|
6. ¬(v = e ∈ |b|)
⊢ if k (=b) k' then v else e fi  = (when k (=b) k'. v) ∈ |b|

---

Latex:

---

Latex:
\mforall{}a:LOSet.  \mforall{}b:AbDMon.  \mforall{}k,k':|a|.  \mforall{}v:|b|.    ((inj(k,v)[k'])  =  (when  k  (=\msubb{})  k'.  v))


By

---

Latex:
((RepD  THENM  Unfold  `oal\_inj`  0 
THENM  SplitOnConclITE 
THENM  Reduce  0)  THENA  Auto)

---

Home Index