---

Step * 1 of Lemma es-before-no_repeats

.....truecase..... 
1. es : EO
2. e : E@i
3. ∀e':E. ((e' < e) ⇒ no_repeats(E;before(e')))
4. i : ℕ
5. j : ℕ
6. i < ||before(e)||
7. j < ||before(e)||
8. [][i] = [][j] ∈ E@i
9. ↑first(e)
⊢ i = j ∈ ℕ
BY
{ (RecUnfold `es-before` (-3)
   THEN (Subst ⌈first(e) ~ tt⌉ (-3)⋅ THENA Auto)
   THEN Reduce (-3)
   THEN Assert ⌈False⌉⋅
   THEN Auto)⋅ }

---

Latex:


.....truecase..... 
1.  es  :  EO
2.  e  :  E@i
3.  \mforall{}e':E.  ((e'  <  e)  {}\mRightarrow{}  no\_repeats(E;before(e')))
4.  i  :  \mBbbN{}
5.  j  :  \mBbbN{}
6.  i  <  ||before(e)||
7.  j  <  ||before(e)||
8.  [][i]  =  [][j]@i
9.  \muparrow{}first(e)
\mvdash{}  i  =  j


By

(RecUnfold  `es-before`  (-3)
  THEN  (Subst  \mkleeneopen{}first(e)  \msim{}  tt\mkleeneclose{}  (-3)\mcdot{}  THENA  Auto)
  THEN  Reduce  (-3)
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index