---

Step * of Lemma firstn_firstn

∀[L:Top List]. ∀[n:ℤ]. ∀[m:ℕn + 1].  (firstn(m;firstn(n;L)) ~ firstn(m;L))
BY
{ (((((InductionOnList THEN UnivCD) THENM RecUnfold `firstn` 0) THEN Reduce 0) THENA Auto) THEN Try (Trivial)) }

1
1. u : Top
2. v : Top List
3. ∀[n:ℤ]. ∀[m:ℕn + 1].  (firstn(m;firstn(n;v)) ~ firstn(m;v))
4. n : ℤ
5. m : ℕn + 1
⊢ case if 0 <z n then [u / firstn(n - 1;v)] else [] fi  of 
    [] => [] 
    a::as' =>
     if 0 <z m then [a / firstn(m - 1;as')] else [] fi  
esac ~ if 0 <z m then [u / firstn(m - 1;v)] else [] fi 

---

Latex:

---

Latex:
\mforall{}[L:Top  List].  \mforall{}[n:\mBbbZ{}].  \mforall{}[m:\mBbbN{}n  +  1].    (firstn(m;firstn(n;L))  \msim{}  firstn(m;L))


By

---

Latex:
(((((InductionOnList  THEN  UnivCD)  THENM  RecUnfold  `firstn`  0)  THEN  Reduce  0)  THENA  Auto)
  THEN  Try  (Trivial)
  )

---

Home Index