---

Step * 1 1 of Lemma oal_merge_comm


1. a : LOSet
2. b : AbDMon
3. ps : |oal(a;b)|
4. qs : |oal(a;b)|
5. u : |a|
⊢ ((ps[u]) * (qs[u])) = ((qs[u]) * (ps[u])) ∈ |b|
BY
{ ((RW AbMonNormC 0) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  a  :  LOSet
2.  b  :  AbDMon
3.  ps  :  |oal(a;b)|
4.  qs  :  |oal(a;b)|
5.  u  :  |a|
\mvdash{}  ((ps[u])  *  (qs[u]))  =  ((qs[u])  *  (ps[u]))


By

---

Latex:
((RW  AbMonNormC  0)  THEN  Auto)\mcdot{}

---

Home Index