---

Step * of Lemma oal_inj_wf

∀a:LOSet. ∀b:AbDMon. ∀k:|a|. ∀v:|b|.  (inj(k,v) ∈ |oal(a;b)|)
BY
{ ((Unfold `oal_inj` 0  
THEN RepD THENM SplitOnConclITE) THENA Auto) }

1
.....truecase..... 
1. a : LOSet
2. b : AbDMon
3. k : |a|
4. v : |b|
5. v = e ∈ |b|
⊢ [] ∈ |oal(a;b)|

2
.....falsecase..... 
1. a : LOSet
2. b : AbDMon
3. k : |a|
4. v : |b|
5. ¬(v = e ∈ |b|)
⊢ [<k, v>] ∈ |oal(a;b)|

---

Latex:

---

Latex:
\mforall{}a:LOSet.  \mforall{}b:AbDMon.  \mforall{}k:|a|.  \mforall{}v:|b|.    (inj(k,v)  \mmember{}  |oal(a;b)|)


By

---

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

---

Home Index