---

Step * 2 of Lemma classfun-res-disjoint-union-comb-as-parallel-eclass1


1. Info : Type
2. A : Type
3. B : Type
4. S : Type
5. es : EO+(Info)
6. X1 : EClass(A)
7. X2 : EClass(B)
8. e : E
9. f1 : Id ─→ A ─→ S ─→ S
10. f2 : Id ─→ B ─→ S ─→ S
11. s : S
12. ↑e ∈b X2
13. single-valued-classrel(es;X2;B)
14. single-valued-classrel(es;X1;A)
15. disjoint-classrel(es;A;X1;B;X2)
⊢ (f1 + f2 loc(e) X1 (+) X2@e s) = ((f1 o X1) || (f2 o X2)@e s) ∈ S
BY
{ ((RWO "classfun-res-parallel-class-right" 0 THENA Auto)
   THEN Try ((RWO "member-eclass-eclass1" 0 THEN Auto))
   THEN Try (DisjointClassRel)
   THEN (RWO "classfun-res-disjoint-union-comb-right" 0 THENA Auto)
   THEN ProveSingleVal
   THEN RWO "classfun-res-eclass1" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  S  :  Type
5.  es  :  EO+(Info)
6.  X1  :  EClass(A)
7.  X2  :  EClass(B)
8.  e  :  E
9.  f1  :  Id  {}\mrightarrow{}  A  {}\mrightarrow{}  S  {}\mrightarrow{}  S
10.  f2  :  Id  {}\mrightarrow{}  B  {}\mrightarrow{}  S  {}\mrightarrow{}  S
11.  s  :  S
12.  \muparrow{}e  \mmember{}\msubb{}  X2
13.  single-valued-classrel(es;X2;B)
14.  single-valued-classrel(es;X1;A)
15.  disjoint-classrel(es;A;X1;B;X2)
\mvdash{}  (f1  +  f2  loc(e)  X1  (+)  X2@e  s)  =  ((f1  o  X1)  ||  (f2  o  X2)@e  s)


By

---

Latex:
((RWO  "classfun-res-parallel-class-right"  0  THENA  Auto)
  THEN  Try  ((RWO  "member-eclass-eclass1"  0  THEN  Auto))
  THEN  Try  (DisjointClassRel)
  THEN  (RWO  "classfun-res-disjoint-union-comb-right"  0  THENA  Auto)
  THEN  ProveSingleVal
  THEN  RWO  "classfun-res-eclass1"  0
  THEN  Auto)

---

Home Index