---

Step * 1 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-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)
BY
{ ((InstLemma `assert-bag_all` [⌜hdataflow(Info;A)⌝;⌜λx.hdf-halted(x)⌝;
    ⌜bag-mapfilter(λx.snd(x)*(map(λx.info(x);before(e)));λp.fst(p) = loc(e);components)⌝]⋅
    THENA Auto
    )
   THEN (RWO "-1<" (-2) THENA Auto)
   THEN Thin (-1)
   THEN RepUR ``so_apply`` (-1)
   THEN (RWO "assert-bag-null<" 0 THENA Auto)
   THEN BLemma `bag-null-bag-union`
   THEN Auto
   THEN SquashConcl
   THEN BagMemberD (-1)
   THEN SquashExRepD
   THEN DVarSets
   THEN BagMemberD (-2)
   THEN DProdsAndUnions
   THEN AllReduce
   THEN InstHyp [⌜v2*(map(λx.info(x);before(e)))⌝] (-7)⋅
   THEN Auto
   THEN Try (Complete ((BagMemberD 0 THEN D 0 THEN InstConcl [⌜<v1, v2>⌝]⋅ THEN Auto THEN BagMemberD  0 THEN Auto)))
   THEN (FLemma `hdf-halted-is-halt` [-1] THENA Auto)
   THEN RWO "-1" (-3)
   THEN Reduce (-3)
   THEN D 0
   THEN (RWO "-3" 0 THENA Auto)
   THEN Reduce 0
   THEN Auto)⋅ }

---

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-mapfilter(\mlambda{}x.snd(x)*(map(\mlambda{}x.info(x);before(e)));\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:
((InstLemma  `assert-bag\_all`  [\mkleeneopen{}hdataflow(Info;A)\mkleeneclose{};\mkleeneopen{}\mlambda{}x.hdf-halted(x)\mkleeneclose{};
    \mkleeneopen{}bag-mapfilter(\mlambda{}x.snd(x)*(map(\mlambda{}x.info(x);before(e)));\mlambda{}p.fst(p)  =  loc(e);components)\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  (RWO  "-1<"  (-2)  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RepUR  ``so\_apply``  (-1)
  THEN  (RWO  "assert-bag-null<"  0  THENA  Auto)
  THEN  BLemma  `bag-null-bag-union`
  THEN  Auto
  THEN  SquashConcl
  THEN  BagMemberD  (-1)
  THEN  SquashExRepD
  THEN  DVarSets
  THEN  BagMemberD  (-2)
  THEN  DProdsAndUnions
  THEN  AllReduce
  THEN  InstHyp  [\mkleeneopen{}v2*(map(\mlambda{}x.info(x);before(e)))\mkleeneclose{}]  (-7)\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  ((BagMemberD  0
                                            THEN  D  0
                                            THEN  InstConcl  [\mkleeneopen{}<v1,  v2>\mkleeneclose{}]\mcdot{}
                                            THEN  Auto
                                            THEN  BagMemberD    0
                                            THEN  Auto)))
  THEN  (FLemma  `hdf-halted-is-halt`  [-1]  THENA  Auto)
  THEN  RWO  "-1"  (-3)
  THEN  Reduce  (-3)
  THEN  D  0
  THEN  (RWO  "-3"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto)\mcdot{}

---

Home Index