---

Step * 1 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
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)
BY
{ ((RWO "bag-map-mapfilter" (-1) THENM RepUR ``compose`` (-1)) 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
8. ↑bag_all(bag-mapfilter(λx.snd(x)*(map(λx.info(x);before(e)));λ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)

---

Latex:

---

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.  \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))
=  \{\}


By

---

Latex:
((RWO  "bag-map-mapfilter"  (-1)  THENM  RepUR  ``compose``  (-1))  THENA  Auto)

---

Home Index