---

Step * 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. before(pred(e)) @ [pred(e)][i] = before(pred(e)) @ [pred(e)][j] ∈ E@i
9. ¬↑first(e)
⊢ i = j ∈ ℕ
BY
{ ((InstHyp [⌈pred(e)⌉] (-7)⋅ THENA Auto)
   THEN (RWO "select-append" (-3) THENA Auto)
   THEN (SplitOnHypITE (-3) THENA Auto))⋅ }

1
.....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 ∈ ℕ

2
.....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 ∈ ℕ

---

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


By

((InstHyp  [\mkleeneopen{}pred(e)\mkleeneclose{}]  (-7)\mcdot{}  THENA  Auto)
  THEN  (RWO  "select-append"  (-3)  THENA  Auto)
  THEN  (SplitOnHypITE  (-3)  THENA  Auto))\mcdot{}

---

Home Index