---

Step * 1 1 1 of Lemma append_firstn_lastn_sq


1. u : Top
2. v : Top List
3. ∀[n:ℕ||v|| + 1]. (v ~ firstn(n;v) @ nth_tl(n;v))
4. n : ℕ||[u / v]|| + 1
5. 0 < n
6. v ~ firstn(n - 1;v) @ nth_tl(n - 1;v)
⊢ v ~ firstn(n - 1;v) @ nth_tl(n;[u / v])
BY
{ ((NthHypSq (-1)) THEN EqCD THEN EqCD THEN Try (Trivial)) }

1
1. u : Top
2. v : Top List
3. ∀[n:ℕ||v|| + 1]. (v ~ firstn(n;v) @ nth_tl(n;v))
4. n : ℕ||[u / v]|| + 1
5. 0 < n
6. v ~ firstn(n - 1;v) @ nth_tl(n - 1;v)
⊢ nth_tl(n;[u / v]) ~ nth_tl(n - 1;v)

---

Latex:

---

Latex:

1.  u  :  Top
2.  v  :  Top  List
3.  \mforall{}[n:\mBbbN{}||v||  +  1].  (v  \msim{}  firstn(n;v)  @  nth\_tl(n;v))
4.  n  :  \mBbbN{}||[u  /  v]||  +  1
5.  0  <  n
6.  v  \msim{}  firstn(n  -  1;v)  @  nth\_tl(n  -  1;v)
\mvdash{}  v  \msim{}  firstn(n  -  1;v)  @  nth\_tl(n;[u  /  v])


By

---

Latex:
((NthHypSq  (-1))  THEN  EqCD  THEN  EqCD  THEN  Try  (Trivial))

---

Home Index