---

Step * 1 of Lemma parallel-as-bind


1. A : Type
2. Info : Type
3. X : EClass(A)
4. Y : EClass(A)
⊢ X || Y = return-bag-class(tt.ff.{}) >b> if b then X else Y fi  ∈ EClass(A)
BY
{ (RepUR ``eclass parallel-class bind-class eclass-compose2 return-bag-class`` 0
   THEN RepeatFor 2 ((Ext THENA Auto))
   THEN Reduce 0) }

1
1. A : Type
2. Info : Type
3. X : EClass(A)
4. Y : EClass(A)
5. x : EO+(Info)
6. x1 : E
⊢ ((X x x1) + (Y x x1)) = ⋃e'∈≤loc(x1).⋃b∈if first(e') then tt.{ff} else {} fi .if b then X else Y fi  x.e' x1 ∈ bag(A)

---

Latex:

---

Latex:

1.  A  :  Type
2.  Info  :  Type
3.  X  :  EClass(A)
4.  Y  :  EClass(A)
\mvdash{}  X  ||  Y  =  return-bag-class(tt.ff.\{\})  >b>  if  b  then  X  else  Y  fi 


By

---

Latex:
(RepUR  ``eclass  parallel-class  bind-class  eclass-compose2  return-bag-class``  0
  THEN  RepeatFor  2  ((Ext  THENA  Auto))
  THEN  Reduce  0)

---

Home Index