---

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


1. Info : Type
2. A : Type
3. B : Type
4. C : Type
5. f : Id ─→ A ─→ B ─→ bag(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
⊢ loc(e) ↓∈ L
BY
{ (InstHyp [⌈es⌉; ⌈b⌉; ⌈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{}  bag(C)
6.  X  :  EClass(A)
7.  Y  :  EClass(B)
8.  L  :  bag(Id)@i'
9.  \mforall{}es:EO+(Info).  \mforall{}v:B.  \mforall{}e:E.    (v  \mmember{}  Y(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  \mdownarrow{}\mmember{}  f  loc(e)  a  b
\mvdash{}  loc(e)  \mdownarrow{}\mmember{}  L


By

---

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

---

Home Index