---

Step * 1 of Lemma oal_merge_preserves_le


1. s : LOSet@i'
2. g : OGrp@i'
3. ps : |oal(s;g)|@i
4. qs : |oal(s;g)|@i
5. rs : |oal(s;g)|@i
6. qs ≤{s,g} rs@1
⊢ (ps ++ qs) ≤{s,g} (ps ++ rs)
BY
{ OnCls [0;6] (RWD (oal_grpC ORELSEC oal_grp_leC)) }

1
1. s : LOSet@i'
2. g : OGrp@i'
3. ps : |oal(s;g)|@i
4. qs : |oal(s;g)|@i
5. rs : |oal(s;g)|@i
6. qs ≤ rs@1
⊢ (ps * qs) ≤ (ps * rs)

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
3.  ps  :  |oal(s;g)|@i
4.  qs  :  |oal(s;g)|@i
5.  rs  :  |oal(s;g)|@i
6.  qs  \mleq{}\{s,g\}  rs@1
\mvdash{}  (ps  ++  qs)  \mleq{}\{s,g\}  (ps  ++  rs)


By

---

Latex:
OnCls  [0;6]  (RWD  (oal\_grpC  ORELSEC  oal\_grp\_leC))

---

Home Index