---

Step * 1 of Lemma oal_lk_merge_2


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([]) = lk(qs) ∈ |s|)
    ⇒ (¬((lv([]) * lv(qs)) = e ∈ |g|))
    ⇒ (lk([] ++ qs) = lk(qs) ∈ |s|))
BY
{ ((Subst' [] ~ 00 0 THENA Computation) 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([])  =  lk(qs))
        {}\mRightarrow{}  (\mneg{}((lv([])  *  lv(qs))  =  e))
        {}\mRightarrow{}  (lk([]  ++  qs)  =  lk(qs)))


By

---

Latex:
((Subst'  []  \msim{}  00  0  THENA  Computation)  THEN  Auto)

---

Home Index