---

Step * 1 1 1 of Lemma es-interface-val-disjoint


1. Info : Type
2. es : EO+(Info)
3. A : Type
4. Xs : EClass(A) List
5. X : EClass(A)
6. (X ∈ Xs)
7. e : E
8. ↑e ∈b X
9. ↑e ∈b first-eclass(Xs)
10. i : ℕ||Xs||
11. ↑e ∈b Xs[i]
12. first-eclass(Xs)(e) = Xs[i](e) ∈ A
13. X ∩ Xs[i] = 0
⊢ X = Xs[i] ∈ EClass(A)
BY
{ ((With ⌈es⌉ (D (-1))⋅ THENA Auto) THEN (With ⌈e⌉ (D (-1))⋅ THENA Auto) THEN D -1 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  A  :  Type
4.  Xs  :  EClass(A)  List
5.  X  :  EClass(A)
6.  (X  \mmember{}  Xs)
7.  e  :  E
8.  \muparrow{}e  \mmember{}\msubb{}  X
9.  \muparrow{}e  \mmember{}\msubb{}  first-eclass(Xs)
10.  i  :  \mBbbN{}||Xs||
11.  \muparrow{}e  \mmember{}\msubb{}  Xs[i]
12.  first-eclass(Xs)(e)  =  Xs[i](e)
13.  X  \mcap{}  Xs[i]  =  0
\mvdash{}  X  =  Xs[i]


By

---

Latex:
((With  \mkleeneopen{}es\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto)  THEN  (With  \mkleeneopen{}e\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto)  THEN  D  -1  THEN  Auto)\mcdot{}

---

Home Index