---

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


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)
BY
{ (RepUR ``hdf-parallel-bag`` 0 THEN RecUnfold `mk-hdf` 0 THEN Fold `hdf-parallel-bag` 0 THEN Reduce 0 THEN AutoSplit) }

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
8. ↑bag_all(bag-map(λx.x*(map(λx.info(x);before(e)));
            bag-mapfilter(λp.(snd(p));λp.fst(p) = loc(e);components));λx.hdf-halted(x))
⊢ bag-union(bag-mapfilter(λp.(snd(snd(p)*(map(λx.info(x);before(e)))(info(e))));λp.fst(p) = loc(e);components))
= {}
∈ bag(A)

2
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
8. ¬↑bag_all(bag-map(λx.x*(map(λx.info(x);before(e)));
             bag-mapfilter(λp.(snd(p));λp.fst(p) = loc(e);components));λx.hdf-halted(x))
⊢ bag-union(bag-mapfilter(λp.(snd(snd(p)*(map(λx.info(x);before(e)))(info(e))));λp.fst(p) = loc(e);components))
= (snd(hdf-run(λa.let s1,b = eval x = bag-map(λX.X(a);bag-map(λx.x*(map(λx.info(x);before(e)));
                                                      bag-mapfilter(λp.(snd(p));λp.fst(p) = loc(e);components))) in
                             let out ←─ ∪p∈x.snd(p)
                             in <bag-map(λp.(fst(p));x), out> 
                  in <hdf-parallel-bag(s1), b>)(info(e))))
∈ bag(A)

---

Latex:



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


By

(RepUR  ``hdf-parallel-bag``  0
  THEN  RecUnfold  `mk-hdf`  0
  THEN  Fold  `hdf-parallel-bag`  0
  THEN  Reduce  0
  THEN  AutoSplit)

---

Home Index