---

Step * 2 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
⊢ lifting-1(λx.(inl x))|X| || lifting-1(λx.(inr x ))|Y|@e = (inr Y@e ) ∈ (A + B)
BY
{ (RWO "-1" 0
   THEN LiftingReduce
   THEN RepUR ``simple-comb-1 simple-comb classfun-res classfun`` 0
   THEN (InstLemma `bag-combine-single-right-as-map` [⌈Y es e⌉;⌈λ2x.inr x ⌉]⋅ THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN Try ((BLemma `member-eclass-iff-size` THEN Auto))
   THEN Try (ProveSingleVal))⋅ }

1
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)

---

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
\mvdash{}  lifting-1(\mlambda{}x.(inl  x))|X|  ||  lifting-1(\mlambda{}x.(inr  x  ))|Y|@e  =  (inr  Y@e  )


By

---

Latex:
(RWO  "-1"  0
  THEN  LiftingReduce
  THEN  RepUR  ``simple-comb-1  simple-comb  classfun-res  classfun``  0
  THEN  (InstLemma  `bag-combine-single-right-as-map`  [\mkleeneopen{}Y  es  e\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.inr  x  \mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  Try  ((BLemma  `member-eclass-iff-size`  THEN  Auto))
  THEN  Try  (ProveSingleVal))\mcdot{}

---

Home Index