---

Step * 1 1 2 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
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)
BY
{ ((RWO "hdf-ap-run" 0 THENA Auto)
   THEN Reduce 0
   THEN (RWO "bag-map-map" 0 THENA Auto)
   THEN RepUR ``compose`` 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN Reduce 0
   THEN (RWO "bag-map-mapfilter" 0 THENA Auto)
   THEN RepUR ``compose`` 0
   THEN (InstLemma `bag-combine-mapfilter` [⌈Id × hdataflow(Info;A)⌉;⌈hdataflow(Info;A) × bag(A)⌉;⌈A⌉;⌈components⌉;
         ⌈λp.fst(p) = loc(e)⌉;⌈λx.snd(x)*(map(λx.info(x);before(e)))(info(e))⌉;⌈λ2p.snd(p)⌉]⋅
         THENA Auto
         )
   THEN (RWO "-1" 0 THENA Auto)
   THEN RepUR ``so_apply`` 0
   THEN RepUR ``bag-mapfilter`` 0
   THEN Fold `bag-combine` 0
   THEN RWO "bag-combine-filter" 0
   THEN Auto) }

---

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
8.  \mneg{}\muparrow{}bag\_all(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));\mlambda{}x.hdf-halted(x))
\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-run(\mlambda{}a.let  s1,b  =  eval  x  =  bag-map(\mlambda{}X.X(a);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)))  in
                                                          let  out  \mleftarrow{}{}  \mcup{}p\mmember{}x.snd(p)
                                                          in  <bag-map(\mlambda{}p.(fst(p));x),  out> 
                                    in  <hdf-parallel-bag(s1),  b>)(info(e))))


By

((RWO  "hdf-ap-run"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (RWO  "bag-map-map"  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  Reduce  0
  THEN  (RWO  "bag-map-mapfilter"  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  (InstLemma  `bag-combine-mapfilter`  [\mkleeneopen{}Id  \mtimes{}  hdataflow(Info;A)\mkleeneclose{};\mkleeneopen{}hdataflow(Info;A)  \mtimes{}  bag(A)\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};
              \mkleeneopen{}components\mkleeneclose{};\mkleeneopen{}\mlambda{}p.fst(p)  =  loc(e)\mkleeneclose{};\mkleeneopen{}\mlambda{}x.snd(x)*(map(\mlambda{}x.info(x);before(e)))(info(e))\mkleeneclose{};
              \mkleeneopen{}\mlambda{}\msubtwo{}p.snd(p)\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  RepUR  ``so\_apply``  0
  THEN  RepUR  ``bag-mapfilter``  0
  THEN  Fold  `bag-combine`  0
  THEN  RWO  "bag-combine-filter"  0
  THEN  Auto)

---

Home Index