---

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


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
BY
{ (InstHyp [⌈es⌉; ⌈a⌉; ⌈e⌉] (-9)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  C  :  Type
5.  f  :  Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  C
6.  X  :  EClass(A)
7.  Y  :  EClass(B)
8.  L  :  bag(Id)@i'
9.  \mforall{}es:EO+(Info).  \mforall{}v:A.  \mforall{}e:E.    (v  \mmember{}  X(e)  {}\mRightarrow{}  loc(e)  \mdownarrow{}\mmember{}  L)@i'
10.  es  :  EO+(Info)@i'
11.  v  :  C@i
12.  e  :  E@i
13.  a  :  A
14.  b  :  B
15.  a  \mmember{}  X(e)
16.  b  \mmember{}  Y(e)
17.  v  =  (f  loc(e)  a  b)
\mvdash{}  loc(e)  \mdownarrow{}\mmember{}  L


By

---

Latex:
(InstHyp  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}a\mkleeneclose{};  \mkleeneopen{}e\mkleeneclose{}]  (-9)\mcdot{}  THEN  Auto)

---

Home Index