---

Step * of Lemma l_before_no_repeats

∀[T:Type]. ∀L:T List. ∀i,j:ℕ||L||.  uiff(j < i;L[j] before L[i] ∈ L) supposing no_repeats(T;L)
BY
{ ((UnivCD THENA Auto)
   THEN D 0
   THEN Auto
   THEN Try (Complete ((BLemma `l_before_select` THEN Auto)))
   THEN (Assert ⌜j < i ∨ (j = i ∈ ℤ) ∨ i < j⌝⋅ THENA Auto')
   THEN D (-1)
   THEN Auto
   THEN D (-1)) }

1
1. T : Type
2. L : T List@i
3. i : ℕ||L||@i
4. j : ℕ||L||@i
5. no_repeats(T;L)
6. L[j] before L[i] ∈ L
7. j = i ∈ ℤ
⊢ j < i

2
1. T : Type
2. L : T List@i
3. i : ℕ||L||@i
4. j : ℕ||L||@i
5. no_repeats(T;L)
6. L[j] before L[i] ∈ L
7. i < j
⊢ j < i

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}i,j:\mBbbN{}||L||.    uiff(j  <  i;L[j]  before  L[i]  \mmember{}  L)  supposing  no\_repeats(T;L)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  0
  THEN  Auto
  THEN  Try  (Complete  ((BLemma  `l\_before\_select`  THEN  Auto)))
  THEN  (Assert  \mkleeneopen{}j  <  i  \mvee{}  (j  =  i)  \mvee{}  i  <  j\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  D  (-1)
  THEN  Auto
  THEN  D  (-1))

---

Home Index