---

Step * 2 of Lemma in-first-eclass


1. [Info] : Type
2. [A] : Type
3. Xs : EClass(A) List@i'
4. ¬↑null(Xs)
5. ||Xs|| ≥ 1 
6. ∀es:EO+(Info). ∀e:E.  (↑e ∈b first-eclass(firstn(||Xs|| - 1;Xs)) ⇐⇒ (∃X∈firstn(||Xs|| - 1;Xs). ↑e ∈b X))
⊢ ∀es:EO+(Info). ∀e:E.
    (↑e ∈b first-eclass(firstn(||Xs|| - 1;Xs) @ [last(Xs)]) ⇐⇒ (∃X∈firstn(||Xs|| - 1;Xs) @ [last(Xs)]. ↑e ∈b X))
BY
{ (MoveToConcl (-1)
   THEN (GenConcl ⌜firstn(||Xs|| - 1;Xs) = Zs ∈ (EClass(A) List)⌝⋅ THENA Auto)
   THEN (GenConcl ⌜last(Xs) = Z ∈ EClass(A)⌝⋅ THENA Auto)
   THEN ThinVar `Xs') }

1
1. [Info] : Type
2. [A] : Type
3. Zs : EClass(A) List@i'
4. Z : EClass(A)@i'
⊢ (∀es:EO+(Info). ∀e:E.  (↑e ∈b first-eclass(Zs) ⇐⇒ (∃X∈Zs. ↑e ∈b X)))
⇒ (∀es:EO+(Info). ∀e:E.  (↑e ∈b first-eclass(Zs @ [Z]) ⇐⇒ (∃X∈Zs @ [Z]. ↑e ∈b X)))

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  [A]  :  Type
3.  Xs  :  EClass(A)  List@i'
4.  \mneg{}\muparrow{}null(Xs)
5.  ||Xs||  \mgeq{}  1 
6.  \mforall{}es:EO+(Info).  \mforall{}e:E.
          (\muparrow{}e  \mmember{}\msubb{}  first-eclass(firstn(||Xs||  -  1;Xs))  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}X\mmember{}firstn(||Xs||  -  1;Xs).  \muparrow{}e  \mmember{}\msubb{}  X))
\mvdash{}  \mforall{}es:EO+(Info).  \mforall{}e:E.
        (\muparrow{}e  \mmember{}\msubb{}  first-eclass(firstn(||Xs||  -  1;Xs)  @  [last(Xs)])
        \mLeftarrow{}{}\mRightarrow{}  (\mexists{}X\mmember{}firstn(||Xs||  -  1;Xs)  @  [last(Xs)].  \muparrow{}e  \mmember{}\msubb{}  X))


By

---

Latex:
(MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}firstn(||Xs||  -  1;Xs)  =  Zs\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}last(Xs)  =  Z\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `Xs')

---

Home Index