---

Step * 1 of Lemma State3-state-class3

.....subterm..... T:t
1:n
1. Info : Type
2. A1 : Type
3. A2 : Type
4. A3 : Type
5. S : Type
6. init : Id ─→ S
7. tr1 : Id ─→ A1 ─→ S ─→ S
8. X1 : EClass(A1)
9. tr2 : Id ─→ A2 ─→ S ─→ S
10. X2 : EClass(A2)
11. tr3 : Id ─→ A3 ─→ S ─→ S
12. X3 : EClass(A3)
⊢ (tr1 + tr2 + tr3 o X1 (+) X2 (+) X3) = (tr1 o X1) || (tr2 o X2) || (tr3 o X3) ∈ EClass(S ─→ S)
BY
{ (Unfold `eclass` 0
   THEN RepeatFor 2 ((Ext THEN Reduce 0 THEN Auto))
   THEN RepUR ``eclass1 parallel-class eclass-compose2 disjoint-union-comb`` 0
   THEN RepUR ``lifting-1 lifting1 simple-comb-1 simple-comb lifting-gen-rev`` 0
   THEN RepeatFor 2 ((RecUnfold `lifting-gen-list-rev` 0 THEN Reduce 0))
   THEN RepUR ``class-ap`` 0
   THEN (RWW "bag-map-append bag-map-map bag-combine-single-right-as-map" 0 THENA Auto)
   THEN RepUR ``compose disjoint-union-tr`` 0 
   THEN Repeat ((EqCD THEN Auto))
   THEN Repeat ((Ext THEN Reduce 0 THEN Auto)))⋅ }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  Info  :  Type
2.  A1  :  Type
3.  A2  :  Type
4.  A3  :  Type
5.  S  :  Type
6.  init  :  Id  {}\mrightarrow{}  S
7.  tr1  :  Id  {}\mrightarrow{}  A1  {}\mrightarrow{}  S  {}\mrightarrow{}  S
8.  X1  :  EClass(A1)
9.  tr2  :  Id  {}\mrightarrow{}  A2  {}\mrightarrow{}  S  {}\mrightarrow{}  S
10.  X2  :  EClass(A2)
11.  tr3  :  Id  {}\mrightarrow{}  A3  {}\mrightarrow{}  S  {}\mrightarrow{}  S
12.  X3  :  EClass(A3)
\mvdash{}  (tr1  +  tr2  +  tr3  o  X1  (+)  X2  (+)  X3)  =  (tr1  o  X1)  ||  (tr2  o  X2)  ||  (tr3  o  X3)


By

---

Latex:
(Unfold  `eclass`  0
  THEN  RepeatFor  2  ((Ext  THEN  Reduce  0  THEN  Auto))
  THEN  RepUR  ``eclass1  parallel-class  eclass-compose2  disjoint-union-comb``  0
  THEN  RepUR  ``lifting-1  lifting1  simple-comb-1  simple-comb  lifting-gen-rev``  0
  THEN  RepeatFor  2  ((RecUnfold  `lifting-gen-list-rev`  0  THEN  Reduce  0))
  THEN  RepUR  ``class-ap``  0
  THEN  (RWW  "bag-map-append  bag-map-map  bag-combine-single-right-as-map"  0  THENA  Auto)
  THEN  RepUR  ``compose  disjoint-union-tr``  0 
  THEN  Repeat  ((EqCD  THEN  Auto))
  THEN  Repeat  ((Ext  THEN  Reduce  0  THEN  Auto)))\mcdot{}

---

Home Index