---

Step * 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])
⊢ ∃k:|s|. ((∀k':|s|. ((k <s k') ⇒ (((ps ++ qs)[k']) = ((ps ++ rs)[k']) ∈ |g|))) ∧ (((ps ++ qs)[k]) < ((ps ++ rs)[k])))
BY
{ (((With k (D 0) THENM GenRepD 
   THENM RWH (LemmaC `lookup_merge`) 0) THENA Auto)
   THEN Try ((BLemma `omon_inc` THEN Complete (Auto))⋅)
   ) }

1
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|

2
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]))

---

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{}  \mexists{}k:|s|
      ((\mforall{}k':|s|.  ((k  <s  k')  {}\mRightarrow{}  (((ps  ++  qs)[k'])  =  ((ps  ++  rs)[k']))))
      \mwedge{}  (((ps  ++  qs)[k])  <  ((ps  ++  rs)[k])))


By

---

Latex:
(((With  k  (D  0)  THENM  GenRepD 
  THENM  RWH  (LemmaC  `lookup\_merge`)  0)  THENA  Auto)
  THEN  Try  ((BLemma  `omon\_inc`  THEN  Complete  (Auto))\mcdot{})
  )

---

Home Index