---

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


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 Y
9. disjoint-classrel(es;A;X;B;Y)
10. single-valued-classrel(es;Y;B)
11. lifting-1(λx.(inl x))|X| || lifting-1(λx.(inr x ))|Y|@e ~ lifting-1(λx.(inr x ))|Y|@e
12. ∪x∈Y es e.{inr x } ~ bag-map(λx.(inr x );Y es e)
⊢ sv-bag-only(bag-map(λx.(inr x );Y es e)) = (inr sv-bag-only(Y es e) ) ∈ (A + B)
BY
{ (InstLemma `sv-bag-only-map` [⌈B⌉;⌈A + B⌉;⌈λ2x.inr x ⌉;⌈Y 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{}  Y
9.  disjoint-classrel(es;A;X;B;Y)
10.  single-valued-classrel(es;Y;B)
11.  lifting-1(\mlambda{}x.(inl  x))|X|  ||  lifting-1(\mlambda{}x.(inr  x  ))|Y|@e  \msim{}  lifting-1(\mlambda{}x.(inr  x  ))|Y|@e
12.  \mcup{}x\mmember{}Y  es  e.\{inr  x  \}  \msim{}  bag-map(\mlambda{}x.(inr  x  );Y  es  e)
\mvdash{}  sv-bag-only(bag-map(\mlambda{}x.(inr  x  );Y  es  e))  =  (inr  sv-bag-only(Y  es  e)  )


By

---

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

---

Home Index