---

Step * of Lemma oalist_subtype

∀[a:LOSet]. ∀[b1,b2:AbDMon].  |oal(a;b1)| ⊆r |oal(a;b2)| supposing strong-subtype(|b1|;|b2|) ∧ (e = e ∈ |b2|)
BY
{ ((UnivCD THENA Auto) THEN (D 0 THENA Auto) THEN D -1 THEN Reduce 0 THEN MemTypeCD THEN Auto THEN ParallelOp (-2)) }

1
1. a : LOSet
2. b1 : AbDMon
3. b2 : AbDMon
4. strong-subtype(|b1|;|b2|)
5. e = e ∈ |b2|
6. x : |((a × (b1↓set)) List)|
7. ↑sd_ordered(map(λx.(fst(x));x))
8. ↑sd_ordered(map(λx.(fst(x));x))
9. ↑(e ∈b map(λx.(snd(x));x))
⊢ ↑(e ∈b map(λx.(snd(x));x))

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  Reduce  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  ParallelOp  (-2))

---

Home Index