---

Step * 1 1 1 of Lemma select_firstn

.....truecase..... 
1. T : Type
2. n : ℤ
3. [%1] : 0 < n
4. ∀as:T List. (((n - 1) ≤ ||as||) ⇒ (∀i:ℕn - 1. (firstn(n - 1;as)[i] = as[i] ∈ T)))
5. 0 < n
⊢ ∀as:T List. ((n ≤ ||as||) ⇒ (∀i:ℕn. (case as of [] => [] | a::as' => [a / firstn(n - 1;as')] esac[i] = as[i] ∈ T)))
BY
{ (((((D 0 THENM (D (-1))) THENM Reduce 0) THENM RepD) THENM Try (Complete (Auto))) THENA Auto) }

1
1. T : Type
2. n : ℤ
3. 0 < n
4. ∀as:T List. (((n - 1) ≤ ||as||) ⇒ (∀i:ℕn - 1. (firstn(n - 1;as)[i] = as[i] ∈ T)))
5. 0 < n
6. u : T
7. v : T List
8. n ≤ (||v|| + 1)
9. i : ℕn
⊢ [u / firstn(n - 1;v)][i] = [u / v][i] ∈ T

---

Latex:

---

Latex:
.....truecase..... 
1.  T  :  Type
2.  n  :  \mBbbZ{}
3.  [\%1]  :  0  <  n
4.  \mforall{}as:T  List.  (((n  -  1)  \mleq{}  ||as||)  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n  -  1.  (firstn(n  -  1;as)[i]  =  as[i])))
5.  0  <  n
\mvdash{}  \mforall{}as:T  List
        ((n  \mleq{}  ||as||)
        {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n.  (case  as  of  []  =>  []  |  a::as'  =>  [a  /  firstn(n  -  1;as')]  esac[i]  =  as[i])))


By

---

Latex:
(((((D  0  THENM  (D  (-1)))  THENM  Reduce  0)  THENM  RepD)  THENM  Try  (Complete  (Auto)))  THENA  Auto)

---

Home Index