---

Step * 2 of Lemma reject_eq_firstn_nth_tl


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])
BY
{ (RWO "reject_cons_tl_sq" 0
   THEN Auto
   THEN (RWO "-5" 0 THENA Auto)
   THEN RW (AddrC [2;1] (RecUnfoldTopC `firstn`)) 0
   THEN Reduce 0
   THEN AutoSplit
   THEN (Subst ⌜1 + (i - 1) ~ i⌝ 0⋅ THENA Auto)
   THEN (Assert ⌜nth_tl(i;v) ~ nth_tl(1 + i;[u / v])⌝⋅ THENM (RWO "-1" 0 THEN Auto))
   THEN RW (AddrC [2] (RecUnfoldTopC `nth_tl`)) 0
   THEN AutoSplit) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}i:\mBbbN{}||v||.  (v\mbackslash{}[i]  \msim{}  firstn(i;v)  @  nth\_tl(1  +  i;v))
5.  i  :  \mBbbZ{}
6.  0  \mleq{}  i  <  ||v||  +  1
7.  0  <  i
\mvdash{}  [u  /  v]\mbackslash{}[i]  \msim{}  firstn(i;[u  /  v])  @  nth\_tl(1  +  i;[u  /  v])


By

---

Latex:
(RWO  "reject\_cons\_tl\_sq"  0
  THEN  Auto
  THEN  (RWO  "-5"  0  THENA  Auto)
  THEN  RW  (AddrC  [2;1]  (RecUnfoldTopC  `firstn`))  0
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  (Subst  \mkleeneopen{}1  +  (i  -  1)  \msim{}  i\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}nth\_tl(i;v)  \msim{}  nth\_tl(1  +  i;[u  /  v])\mkleeneclose{}\mcdot{}  THENM  (RWO  "-1"  0  THEN  Auto))
  THEN  RW  (AddrC  [2]  (RecUnfoldTopC  `nth\_tl`))  0
  THEN  AutoSplit)

---

Home Index