---

Step * of Lemma whole_segment-sq

∀as:Top List. (as[0..||as||-] ~ as)
BY
{ (Unfold `segment` 0
   THEN InductionOnList
   THEN RecUnfold `nth_tl` 0
   THEN Reduce 0
   THEN RecUnfold `firstn` 0
   THEN Reduce 0
   THEN Auto
   THEN AutoSplit) }

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

2
1. u : Top
2. v : Top List
3. ¬0 < (||v|| + 1) - 0
4. firstn(||v|| - 0;nth_tl(0;v)) ~ v
⊢ [] ~ [u / v]

---

Latex:

---

Latex:
\mforall{}as:Top  List.  (as[0..||as||\msupminus{}]  \msim{}  as)


By

---

Latex:
(Unfold  `segment`  0
  THEN  InductionOnList
  THEN  RecUnfold  `nth\_tl`  0
  THEN  Reduce  0
  THEN  RecUnfold  `firstn`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  AutoSplit)

---

Home Index