---

Step * of Lemma simple-loc-comb-2-loc-bounded

∀[Info,A,B,C:Type]. ∀[f:Id ─→ A ─→ B ─→ C]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  ((LocBounded(A;X) ∨ LocBounded(B;Y)) ⇒ LocBounded(C;lifting-loc-2(f) o (Loc,X, Y)))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``loc-bounded-class class-loc-bound`` 0
   THEN RepUR ``loc-bounded-class class-loc-bound`` (-1)
   THEN D (-1)
   THEN ExRepD
   THEN InstConcl [⌈L⌉]⋅
   THEN Auto
   THEN MaUseClassRel (-1)
   THEN D (-1)
   THEN (Unhide THENA Auto)
   THEN ExRepD) }

1
1. Info : Type
2. A : Type
3. B : Type
4. C : Type
5. f : Id ─→ A ─→ B ─→ C
6. X : EClass(A)
7. Y : EClass(B)
8. L : bag(Id)@i'
9. ∀es:EO+(Info). ∀v:A. ∀e:E.  (v ∈ X(e) ⇒ loc(e) ↓∈ L)@i'
10. es : EO+(Info)@i'
11. v : C@i
12. e : E@i
13. a : A
14. b : B
15. a ∈ X(e)
16. b ∈ Y(e)
17. v = (f loc(e) a b) ∈ C
⊢ loc(e) ↓∈ L

2
1. Info : Type
2. A : Type
3. B : Type
4. C : Type
5. f : Id ─→ A ─→ B ─→ C
6. X : EClass(A)
7. Y : EClass(B)
8. L : bag(Id)@i'
9. ∀es:EO+(Info). ∀v:B. ∀e:E.  (v ∈ Y(e) ⇒ loc(e) ↓∈ L)@i'
10. es : EO+(Info)@i'
11. v : C@i
12. e : E@i
13. a : A
14. b : B
15. a ∈ X(e)
16. b ∈ Y(e)
17. v = (f loc(e) a b) ∈ C
⊢ loc(e) ↓∈ L

---

Latex:

---

Latex:
\mforall{}[Info,A,B,C:Type].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  C].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].
    ((LocBounded(A;X)  \mvee{}  LocBounded(B;Y))  {}\mRightarrow{}  LocBounded(C;lifting-loc-2(f)  o  (Loc,X,  Y)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``loc-bounded-class  class-loc-bound``  0
  THEN  RepUR  ``loc-bounded-class  class-loc-bound``  (-1)
  THEN  D  (-1)
  THEN  ExRepD
  THEN  InstConcl  [\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  MaUseClassRel  (-1)
  THEN  D  (-1)
  THEN  (Unhide  THENA  Auto)
  THEN  ExRepD)

---

Home Index