---

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


1. [Info] : Type
2. [A] : {A:Type| valueall-type(A)} 
3. [X] : EClass(A)
4. LocalClass(X)@i'
5. LocBounded(A;X)@i'
⊢ GlobalClass(Info;A;X)
BY
{ (UnfoldTopAb (-1)
   THEN UnfoldTopAb (-2)
   THEN UnfoldTopAb 0
   THEN ExRepD
   THEN UnfoldTopAb (-1)
   THEN UseWitness ⌈bag-map(λi.<i, F i>;bag-remove-repeats(IdDeq;L))⌉⋅
   THEN MemTypeCD
   THEN Auto
   THEN Unfold `eclass` 0
   THEN RepeatFor 2 ((Ext THEN Auto))
   THEN Reduce 0
   THEN Fold `class-ap` 0
   THEN RenameVar `es' (-2)
   THEN RenameVar `e' (-1)
   THEN (InstLemma `bag-mapfilter-map` [⌈Id⌉;⌈Id × hdataflow(Info;A)⌉;⌈bag(A)⌉;⌈bag-remove-repeats(IdDeq;L)⌉;
         ⌈λp.fst(p) = loc(e)⌉;⌈λp.(snd(snd(p)*(map(λx.info(x);before(e)))(info(e))))⌉;⌈λi.<i, F i>⌉]⋅
         THENA Auto
         )
   THEN (RWO "-1" 0 THENA Auto)
   THEN Thin (-1)
   THEN RepUR ``compose`` 0
   THEN (Decide ⌈loc(e) ↓∈ L⌉⋅ THENA Auto)) }

1
1. Info : Type
2. A : {A:Type| valueall-type(A)} 
3. X : EClass(A)
4. F : Id ─→ hdataflow(Info;A)@i'
5. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(F loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(A))
6. L : bag(Id)@i'
7. ∀es:EO+(Info). ∀v:A. ∀e:E.  (v ∈ X(e) ⇒ loc(e) ↓∈ L)@i'
8. es : EO+(Info)
9. e : E
10. loc(e) ↓∈ L
⊢ X(e)
= bag-union(bag-mapfilter(λx.(snd(F x*(map(λx@0.info(x@0);before(e)))(info(e))));λx.x = loc(e);
                          bag-remove-repeats(IdDeq;L)))
∈ bag(A)

2
1. Info : Type
2. A : {A:Type| valueall-type(A)} 
3. X : EClass(A)
4. F : Id ─→ hdataflow(Info;A)@i'
5. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(F loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(A))
6. L : bag(Id)@i'
7. ∀es:EO+(Info). ∀v:A. ∀e:E.  (v ∈ X(e) ⇒ loc(e) ↓∈ L)@i'
8. es : EO+(Info)
9. e : E
10. ¬loc(e) ↓∈ L
⊢ X(e)
= bag-union(bag-mapfilter(λx.(snd(F x*(map(λx@0.info(x@0);before(e)))(info(e))));λx.x = loc(e);
                          bag-remove-repeats(IdDeq;L)))
∈ bag(A)

---

Latex:



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


By

(UnfoldTopAb  (-1)
  THEN  UnfoldTopAb  (-2)
  THEN  UnfoldTopAb  0
  THEN  ExRepD
  THEN  UnfoldTopAb  (-1)
  THEN  UseWitness  \mkleeneopen{}bag-map(\mlambda{}i.<i,  F  i>bag-remove-repeats(IdDeq;L))\mkleeneclose{}\mcdot{}
  THEN  MemTypeCD
  THEN  Auto
  THEN  Unfold  `eclass`  0
  THEN  RepeatFor  2  ((Ext  THEN  Auto))
  THEN  Reduce  0
  THEN  Fold  `class-ap`  0
  THEN  RenameVar  `es'  (-2)
  THEN  RenameVar  `e'  (-1)
  THEN  (InstLemma  `bag-mapfilter-map`  [\mkleeneopen{}Id\mkleeneclose{};\mkleeneopen{}Id  \mtimes{}  hdataflow(Info;A)\mkleeneclose{};\mkleeneopen{}bag(A)\mkleeneclose{};
              \mkleeneopen{}bag-remove-repeats(IdDeq;L)\mkleeneclose{};\mkleeneopen{}\mlambda{}p.fst(p)  =  loc(e)\mkleeneclose{};
              \mkleeneopen{}\mlambda{}p.(snd(snd(p)*(map(\mlambda{}x.info(x);before(e)))(info(e))))\mkleeneclose{};\mkleeneopen{}\mlambda{}i.<i,  F  i>\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RepUR  ``compose``  0
  THEN  (Decide  \mkleeneopen{}loc(e)  \mdownarrow{}\mmember{}  L\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index