---

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

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

1
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)

---

Latex:

---

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


By

---

Latex:
(((With  \mkleeneopen{}X\mkleeneclose{}  (D  5)\mcdot{}  THENA  Auto)  THEN  (D  -1  THENA  Auto))
  THEN  (With  \mkleeneopen{}Xs[i]\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  ((D  -1  THEN  Auto)))\mcdot{}

---

Home Index