---

Step * of Lemma es-before-no_repeats

∀[es:EO]. ∀[e:E].  no_repeats(E;before(e))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN MoveToConcl (-1)
   THEN VrCausalInd'
   THEN Unfold `no_repeats` 0
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN D (-2)
   THEN RecUnfold `es-before` (-1)⋅
   THEN (SplitOnHypITE (-1) 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. [][i] = [][j] ∈ E@i
9. ↑first(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. before(pred(e)) @ [pred(e)][i] = before(pred(e)) @ [pred(e)][j] ∈ E@i
9. ¬↑first(e)
⊢ i = j ∈ ℕ

---

Latex:


\mforall{}[es:EO].  \mforall{}[e:E].    no\_repeats(E;before(e))


By

(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  MoveToConcl  (-1)
  THEN  VrCausalInd'
  THEN  Unfold  `no\_repeats`  0
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  D  (-2)
  THEN  RecUnfold  `es-before`  (-1)\mcdot{}
  THEN  (SplitOnHypITE  (-1)  THENA  Auto))

---

Home Index