---

Step * 1 1 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])
9. k' : |s|
10. k <s k'
⊢ ((ps[k']) * (qs[k'])) = ((ps[k']) * (rs[k'])) ∈ |g|
BY
{ ((RWH (HypC 7) 0) 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])
9.  k'  :  |s|
10.  k  <s  k'
\mvdash{}  ((ps[k'])  *  (qs[k']))  =  ((ps[k'])  *  (rs[k']))


By

---

Latex:
((RWH  (HypC  7)  0)  THEN  Auto)

---

Home Index