---

Step * 2 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. before(pred(e))[i]
= if j <z ||before(pred(e))|| then before(pred(e))[j] else [pred(e)][j - ||before(pred(e))||] fi 
∈ E@i
9. ¬↑first(e)
10. no_repeats(E;before(pred(e)))
11. i < ||before(pred(e))||
⊢ i = j ∈ ℕ
BY
{ ((SplitOnHypITE (-4) THENA Auto)
   THEN Try (Complete ((SupposeNot THEN Assert ⌈False⌉⋅ THEN Auto)))
   THEN (InstLemma `es-before-pred-length` [⌈es⌉;⌈e⌉]⋅ THENA Auto)⋅
   THEN (Assert ⌈j = ||before(pred(e))|| ∈ ℤ⌉⋅ THENA Auto)
   THEN RevHypSubst' (-1) (-7)
   THEN (Subst ⌈j - j ~ 0⌉ (-7)⋅ THENA Auto)
   THEN Reduce (-7)
   THEN (Assert ⌈(i = j ∈ ℤ) ∨ i < j⌉⋅ THENA Auto)
   THEN D (-1)
   THEN Auto
   THEN Assert ⌈False⌉⋅
   THEN Auto
   THEN (Assert ⌈(before(pred(e))[i] ∈ before(pred(e)))⌉⋅ THENA (BLemma `select_member` THEN Auto))
   THEN (RWO "member-es-before" (-1) THENA Auto)
   THEN (HypSubst' (-9) (-1) THENA Auto)
   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.  before(pred(e))[i]
=  if  j  <z  ||before(pred(e))||  then  before(pred(e))[j]  else  [pred(e)][j  -  ||before(pred(e))||]  fi  @i
9.  \mneg{}\muparrow{}first(e)
10.  no\_repeats(E;before(pred(e)))
11.  i  <  ||before(pred(e))||
\mvdash{}  i  =  j


By

((SplitOnHypITE  (-4)  THENA  Auto)
  THEN  Try  (Complete  ((SupposeNot  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)))
  THEN  (InstLemma  `es-before-pred-length`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)\mcdot{}
  THEN  (Assert  \mkleeneopen{}j  =  ||before(pred(e))||\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RevHypSubst'  (-1)  (-7)
  THEN  (Subst  \mkleeneopen{}j  -  j  \msim{}  0\mkleeneclose{}  (-7)\mcdot{}  THENA  Auto)
  THEN  Reduce  (-7)
  THEN  (Assert  \mkleeneopen{}(i  =  j)  \mvee{}  i  <  j\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Auto
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (Assert  \mkleeneopen{}(before(pred(e))[i]  \mmember{}  before(pred(e)))\mkleeneclose{}\mcdot{}  THENA  (BLemma  `select\_member`  THEN  Auto))
  THEN  (RWO  "member-es-before"  (-1)  THENA  Auto)
  THEN  (HypSubst'  (-9)  (-1)  THENA  Auto)
  THEN  Auto)

---

Home Index