---

Step * 2 2 of Lemma es-before-no_repeats

.....falsecase..... 
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. [pred(e)][i - ||before(pred(e))||]
= 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
{ ((InstLemma `es-before-pred-length` [⌈es⌉;⌈e⌉]⋅ THENA Auto)
   THEN (Assert ⌈||before(pred(e))|| = i ∈ ℤ⌉⋅ THENA Auto)
   THEN HypSubst' (-1) (-6)
   THEN (Subst ⌈i - i ~ 0⌉ (-6)⋅ THENA Auto)
   THEN Reduce (-6)
   THEN HypSubst' (-1) (-2)
   THEN (Assert ⌈(i = j ∈ ℤ) ∨ j < i⌉⋅ THENA Auto)
   THEN D (-1)
   THEN Auto
   THEN Assert ⌈False⌉⋅
   THEN Auto
   THEN SplitOnHypITE (-7)
   THEN Auto
   THEN (Assert ⌈(before(pred(e))[j] ∈ before(pred(e)))⌉⋅ THENA (BLemma `select_member` THEN Auto))
   THEN (RWO "member-es-before" (-1) THENA Auto)
   THEN (RevHypSubst' (-9) (-1) THENA Auto)
   THEN Auto)⋅ }

---

Latex:


.....falsecase..... 
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.  [pred(e)][i  -  ||before(pred(e))||]
=  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.  \mneg{}i  <  ||before(pred(e))||
\mvdash{}  i  =  j


By

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

---

Home Index