---

Step * 1 of Lemma global-class-iff-bounded-local-class


1. [Info] : Type
2. [A] : {A:Type| valueall-type(A)} 
3. [X] : EClass(A)
4. GlobalClass(Info;A;X)@i'
⊢ LocalClass(X)
BY
{ (Unfold `local-class` 0
   THEN D (-1)
   THEN UseWitness ⌈λi.hdf-parallel-bag(bag-mapfilter(λp.(snd(p));λp.fst(p) = i;components))⌉⋅
   THEN MemTypeCD
   THEN Auto
   THEN (RWO "-3" 0 THENA Auto)
   THEN RepUR ``class-ap`` 0
   THEN (RWO "hdf-parallel-bag-iterate" 0 THENA Auto)) }

1
1. Info : Type
2. A : {A:Type| valueall-type(A)} 
3. X : EClass(A)
4. components : bag(Id × hdataflow(Info;A))@i'
5. X
= (λes,e. bag-union(bag-mapfilter(λp.(snd(snd(p)*(map(λx.info(x);before(e)))(info(e))));λp.fst(p) = loc(e);components)))
∈ EClass(A)@i'
6. es : EO+(Info)@i'
7. e : E@i
⊢ bag-union(bag-mapfilter(λp.(snd(snd(p)*(map(λx.info(x);before(e)))(info(e))));λp.fst(p) = loc(e);components))
= (snd(hdf-parallel-bag(bag-map(λx.x*(map(λx.info(x);before(e)));
                        bag-mapfilter(λp.(snd(p));λp.fst(p) = loc(e);components)))(info(e))))
∈ bag(A)

---

Latex:



1.  [Info]  :  Type
2.  [A]  :  \{A:Type|  valueall-type(A)\} 
3.  [X]  :  EClass(A)
4.  GlobalClass(Info;A;X)@i'
\mvdash{}  LocalClass(X)


By

(Unfold  `local-class`  0
  THEN  D  (-1)
  THEN  UseWitness  \mkleeneopen{}\mlambda{}i.hdf-parallel-bag(bag-mapfilter(\mlambda{}p.(snd(p));\mlambda{}p.fst(p)  =  i;components))\mkleeneclose{}\mcdot{}
  THEN  MemTypeCD
  THEN  Auto
  THEN  (RWO  "-3"  0  THENA  Auto)
  THEN  RepUR  ``class-ap``  0
  THEN  (RWO  "hdf-parallel-bag-iterate"  0  THENA  Auto))

---

Home Index