---

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


1. [Info] : Type
2. [A] : {A:Type| valueall-type(A)} 
3. [X] : EClass(A)
4. GlobalClass(Info;A;X)@i'
⊢ LocBounded(A;X)
BY
{ (Unfold `loc-bounded-class` 0
   THEN D (-1)
   THEN InstConcl [⌈bag-map(λp.(fst(p));components)⌉]⋅
   THEN Auto
   THEN Unfold `class-loc-bound` 0
   THEN Auto
   THEN BagMemberD 0
   THEN (RWO "-5" (-1) THENA Auto)
   THEN RepUR ``classrel`` (-1)
   THEN Repeat ((BagMemberD (-1) THEN SquashExRepD))
   THEN DVarSets
   THEN BagMemberD (-2)
   THEN D 0
   THEN InstConcl [⌈v1⌉]⋅
   THEN Auto) }

---

Latex:



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


By

(Unfold  `loc-bounded-class`  0
  THEN  D  (-1)
  THEN  InstConcl  [\mkleeneopen{}bag-map(\mlambda{}p.(fst(p));components)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Unfold  `class-loc-bound`  0
  THEN  Auto
  THEN  BagMemberD  0
  THEN  (RWO  "-5"  (-1)  THENA  Auto)
  THEN  RepUR  ``classrel``  (-1)
  THEN  Repeat  ((BagMemberD  (-1)  THEN  SquashExRepD))
  THEN  DVarSets
  THEN  BagMemberD  (-2)
  THEN  D  0
  THEN  InstConcl  [\mkleeneopen{}v1\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index