---

Step * 1 2 of Lemma oal_merge_preserves_lt


1. s : LOSet
2. g : OCMon
3. ps : |oal(s;g)|
4. qs : |oal(s;g)|
5. rs : |oal(s;g)|
6. k : |s|
7. ∀k':|s|. ((k <s k') ⇒ ((qs[k']) = (rs[k']) ∈ |g|))
8. (qs[k]) < (rs[k])
⊢ ((ps[k]) * (qs[k])) < ((ps[k]) * (rs[k]))
BY
{ ((BLemma `grp_op_preserves_lt`) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  LOSet
2.  g  :  OCMon
3.  ps  :  |oal(s;g)|
4.  qs  :  |oal(s;g)|
5.  rs  :  |oal(s;g)|
6.  k  :  |s|
7.  \mforall{}k':|s|.  ((k  <s  k')  {}\mRightarrow{}  ((qs[k'])  =  (rs[k'])))
8.  (qs[k])  <  (rs[k])
\mvdash{}  ((ps[k])  *  (qs[k]))  <  ((ps[k])  *  (rs[k]))


By

---

Latex:
((BLemma  `grp\_op\_preserves\_lt`)  THEN  Auto)

---

Home Index