---

Step * of Lemma reject_eq_firstn_nth_tl

∀[T:Type]. ∀[L:T List]. ∀[i:ℕ||L||].  (L\[i] ~ firstn(i;L) @ nth_tl(1 + i;L))
BY
{ (Auto
   THEN ListInd (-2)
   THEN Auto
   THEN Try (Complete ((Reduce (-1) THEN D (-1) THEN Auto)))
   THEN Reduce (-1)⋅
   THEN (D (-1) THENA Auto)
   THEN (Assert ⌜(i = 0 ∈ ℤ) ∨ 0 < i⌝⋅ THENA Auto)
   THEN D (-1)) }

1
1. T : Type
2. u : T
3. v : T List
4. ∀i:ℕ||v||. (v\[i] ~ firstn(i;v) @ nth_tl(1 + i;v))
5. i : ℤ
6. 0 ≤ i < ||v|| + 1
7. i = 0 ∈ ℤ
⊢ [u / v]\[i] ~ firstn(i;[u / v]) @ nth_tl(1 + i;[u / v])

2
1. T : Type
2. u : T
3. v : T List
4. ∀i:ℕ||v||. (v\[i] ~ firstn(i;v) @ nth_tl(1 + i;v))
5. i : ℤ
6. 0 ≤ i < ||v|| + 1
7. 0 < i
⊢ [u / v]\[i] ~ firstn(i;[u / v]) @ nth_tl(1 + i;[u / v])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[i:\mBbbN{}||L||].    (L\mbackslash{}[i]  \msim{}  firstn(i;L)  @  nth\_tl(1  +  i;L))


By

---

Latex:
(Auto
  THEN  ListInd  (-2)
  THEN  Auto
  THEN  Try  (Complete  ((Reduce  (-1)  THEN  D  (-1)  THEN  Auto)))
  THEN  Reduce  (-1)\mcdot{}
  THEN  (D  (-1)  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}(i  =  0)  \mvee{}  0  <  i\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  (-1))

---

Home Index