---

Step * of Lemma oalist_cases_b

∀a:LOSet. ∀b:AbDMon. ∀Q:|oal(a;b)| ⟶ ℙ.
  (Q[[]]
  ⇒ (∀ws:|oal(a;b)|. ∀k:|a|. ∀v:|b|.
        ((↑(∀bx(:|a|) ∈ map(λz.(fst(z));ws). (x <b k))) ⇒ (¬(v = e ∈ |b|)) ⇒ Q[[<k, v> / ws]]))
  ⇒ {∀ws:|oal(a;b)|. Q[ws]})
BY
{ ((RepD THENM BLemma `oalist_cases_a`) THEN Auto) }

1
1. a : LOSet@i'
2. b : AbDMon@i'
3. Q : |oal(a;b)| ⟶ ℙ@i'
4. Q[[]]@i
5. ∀ws:|oal(a;b)|. ∀k:|a|. ∀v:|b|.
     ((↑(∀bx(:|a|) ∈ map(λz.(fst(z));ws). (x <b k))) ⇒ (¬(v = e ∈ |b|)) ⇒ Q[[<k, v> / ws]])@i
6. ws : |oal(a;b)|@i
7. x : |a|@i
8. y : |b|@i
9. ↑before(x;map(λx.(fst(x));ws))@i
10. ¬(y = e ∈ |b|)@i
⊢ Q[[<x, y> / ws]]

2
1. a : LOSet@i'
2. b : AbDMon@i'
3. Q : |oal(a;b)| ⟶ ℙ@i'
4. Q[[]]@i
5. ws : |oal(a;b)|@i
6. k : |a|@i
7. v : |b|@i
8. ↑(∀bx(:|a|) ∈ map(λz.(fst(z));ws)
        (x <b k))
9. ¬(v = e ∈ |b|)
⊢ [<k, v> / ws] ∈ {ps:(|a| × |b|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))} 

---

Latex:

---

Latex:
\mforall{}a:LOSet.  \mforall{}b:AbDMon.  \mforall{}Q:|oal(a;b)|  {}\mrightarrow{}  \mBbbP{}.
    (Q[[]]
    {}\mRightarrow{}  (\mforall{}ws:|oal(a;b)|.  \mforall{}k:|a|.  \mforall{}v:|b|.
                ((\muparrow{}(\mforall{}\msubb{}x(:|a|)  \mmember{}  map(\mlambda{}z.(fst(z));ws).  (x  <\msubb{}  k)))  {}\mRightarrow{}  (\mneg{}(v  =  e))  {}\mRightarrow{}  Q[[<k,  v>  /  ws]]))
    {}\mRightarrow{}  \{\mforall{}ws:|oal(a;b)|.  Q[ws]\})


By

---

Latex:
((RepD  THENM  BLemma  `oalist\_cases\_a`)  THEN  Auto)

---

Home Index