---

Step * 2 1 of Lemma classfun-res-disjoint-union-comb-left


1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. X : EClass(A)
6. Y : EClass(B)
7. e : E
8. ↑e ∈b X
9. disjoint-classrel(es;A;X;B;Y)
10. single-valued-classrel(es;X;A)
11. lifting-1(λx.(inl x))|X| || lifting-1(λx.(inr x ))|Y|@e ~ lifting-1(λx.(inl x))|X|@e
12. ∪x∈X es e.{inl x} ~ bag-map(λx.(inl x);X es e)
⊢ sv-bag-only(bag-map(λx.(inl x);X es e)) = (inl sv-bag-only(X es e)) ∈ (A + B)
BY
{ (InstLemma `sv-bag-only-map` [⌈A⌉;⌈A + B⌉;⌈λ2x.inl x⌉;⌈X es e⌉]⋅
   THEN Auto
   THEN Try ((RWO "member-eclass-iff-size" (-5) THEN Auto))
   THEN ProveSingleVal)⋅ }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  es  :  EO+(Info)
5.  X  :  EClass(A)
6.  Y  :  EClass(B)
7.  e  :  E
8.  \muparrow{}e  \mmember{}\msubb{}  X
9.  disjoint-classrel(es;A;X;B;Y)
10.  single-valued-classrel(es;X;A)
11.  lifting-1(\mlambda{}x.(inl  x))|X|  ||  lifting-1(\mlambda{}x.(inr  x  ))|Y|@e  \msim{}  lifting-1(\mlambda{}x.(inl  x))|X|@e
12.  \mcup{}x\mmember{}X  es  e.\{inl  x\}  \msim{}  bag-map(\mlambda{}x.(inl  x);X  es  e)
\mvdash{}  sv-bag-only(bag-map(\mlambda{}x.(inl  x);X  es  e))  =  (inl  sv-bag-only(X  es  e))


By

---

Latex:
(InstLemma  `sv-bag-only-map`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}A  +  B\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.inl  x\mkleeneclose{};\mkleeneopen{}X  es  e\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((RWO  "member-eclass-iff-size"  (-5)  THEN  Auto))
  THEN  ProveSingleVal)\mcdot{}

---

Home Index