---

Step * 1 of Lemma oal_lk_merge_1


1. s : LOSet
2. g : AbDMon
⊢ ∀qs:|oal(s;g)|
    ((¬([] = 00 ∈ |oal(s;g)|))
    ⇒ (¬(qs = 00 ∈ |oal(s;g)|))
    ⇒ (¬(([] ++ qs) = 00 ∈ |oal(s;g)|))
    ⇒ (lk([]) <s lk(qs))
    ⇒ (lk([] ++ qs) = lk(qs) ∈ |s|))
BY
{ RWH (SimpleMacroC `*` [] 00 ``oal_nil``) 0 
THEN ((D 0 THENM D 0 THENM D (-1)) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  s  :  LOSet
2.  g  :  AbDMon
\mvdash{}  \mforall{}qs:|oal(s;g)|
        ((\mneg{}([]  =  00))
        {}\mRightarrow{}  (\mneg{}(qs  =  00))
        {}\mRightarrow{}  (\mneg{}(([]  ++  qs)  =  00))
        {}\mRightarrow{}  (lk([])  <s  lk(qs))
        {}\mRightarrow{}  (lk([]  ++  qs)  =  lk(qs)))


By

---

Latex:
RWH  (SimpleMacroC  `*`  []  00  ``oal\_nil``)  0 
THEN  ((D  0  THENM  D  0  THENM  D  (-1))  THEN  Auto)\mcdot{}

---

Home Index