---

Step * of Lemma oalist_cases_c

∀a:LOSet. ∀b:AbDMon. ∀Q:|oal(a;b)| ⟶ ℙ.
  (Q[00]
  ⇒ (∀ws:|oal(a;b)|. ∀x:|a|. ∀y:|b|.  ((↑before(x;map(λx.(fst(x));ws))) ⇒ (¬(y = e ∈ |b|)) ⇒ Q[oal_cons_pr(x;y;ws)]))
  ⇒ {∀ws:|oal(a;b)|. Q[ws]})
BY
{ Unfolds ``oal_nil oal_cons_pr`` 0 THEN Lemma `oalist_cases_a` }

---

Latex:

---

Latex:
\mforall{}a:LOSet.  \mforall{}b:AbDMon.  \mforall{}Q:|oal(a;b)|  {}\mrightarrow{}  \mBbbP{}.
    (Q[00]
    {}\mRightarrow{}  (\mforall{}ws:|oal(a;b)|.  \mforall{}x:|a|.  \mforall{}y:|b|.
                ((\muparrow{}before(x;map(\mlambda{}x.(fst(x));ws)))  {}\mRightarrow{}  (\mneg{}(y  =  e))  {}\mRightarrow{}  Q[oal\_cons\_pr(x;y;ws)]))
    {}\mRightarrow{}  \{\mforall{}ws:|oal(a;b)|.  Q[ws]\})


By

---

Latex:
Unfolds  ``oal\_nil  oal\_cons\_pr``  0  THEN  Lemma  `oalist\_cases\_a`

---

Home Index