---

Step * 1 of Lemma State2-state-class2

.....subterm..... T:t
1:n
1. Info : Type
2. A1 : Type
3. A2 : Type
4. S : Type
5. init : Id ─→ S
6. tr1 : Id ─→ A1 ─→ S ─→ S
7. X1 : EClass(A1)
8. tr2 : Id ─→ A2 ─→ S ─→ S
9. X2 : EClass(A2)
⊢ (tr1 + tr2 o X1 (+) X2) = (tr1 o X1) || (tr2 o X2) ∈ 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.  S  :  Type
5.  init  :  Id  {}\mrightarrow{}  S
6.  tr1  :  Id  {}\mrightarrow{}  A1  {}\mrightarrow{}  S  {}\mrightarrow{}  S
7.  X1  :  EClass(A1)
8.  tr2  :  Id  {}\mrightarrow{}  A2  {}\mrightarrow{}  S  {}\mrightarrow{}  S
9.  X2  :  EClass(A2)
\mvdash{}  (tr1  +  tr2  o  X1  (+)  X2)  =  (tr1  o  X1)  ||  (tr2  o  X2)


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

---

Home Index