---

Step * 2 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
⊢ lifting-1(λx.(inl x))|X| || lifting-1(λx.(inr x ))|Y|@e = (inl X@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` [⌈X es e⌉;⌈λ2x.inl 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 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)

---

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
\mvdash{}  lifting-1(\mlambda{}x.(inl  x))|X|  ||  lifting-1(\mlambda{}x.(inr  x  ))|Y|@e  =  (inl  X@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{}X  es  e\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.inl  x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  Try  ((BLemma  `member-eclass-iff-size`  THEN  Auto))
  THEN  Try  (ProveSingleVal))

---

Home Index