---

Step * of Lemma oalist_strong-subtype

∀[a:LOSet]. ∀[b1,b2:AbDMon].
  strong-subtype(|oal(a;b1)|;|oal(a;b2)|) supposing strong-subtype(|b1|;|b2|) ∧ (e = e ∈ |b2|)
BY
{ ((UnivCD THENA Auto)
   THEN Reduce 0
   THEN (BLemma `strong-subtype-set` THENA Auto)
   THEN Try ((BLemma `strong-subtype-list` THEN Auto))) }

1
1. a : LOSet
2. b1 : AbDMon
3. b2 : AbDMon
4. strong-subtype(|b1|;|b2|) ∧ (e = e ∈ |b2|)
⊢ ∀ps:(|a| × |b1|) List
    (((↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps))))
    ⇒ ((↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))))

---

Latex:

---

Latex:
\mforall{}[a:LOSet].  \mforall{}[b1,b2:AbDMon].
    strong-subtype(|oal(a;b1)|;|oal(a;b2)|)  supposing  strong-subtype(|b1|;|b2|)  \mwedge{}  (e  =  e)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Reduce  0
  THEN  (BLemma  `strong-subtype-set`  THENA  Auto)
  THEN  Try  ((BLemma  `strong-subtype-list`  THEN  Auto)))

---

Home Index