---

Step * of Lemma select-firstn

∀[L:Top List]. ∀[n:ℕ]. ∀[x:ℕn].  (firstn(n;L)[x] ~ L[x])
BY
{ xxx((UnivCD THENA Auto) THEN (Decide ⌜||L|| ≤ n⌝⋅ THENA Auto))xxx }

1
1. L : Top List
2. n : ℕ
3. x : ℕn
4. ||L|| ≤ n
⊢ firstn(n;L)[x] ~ L[x]

2
1. L : Top List
2. n : ℕ
3. x : ℕn
4. ¬(||L|| ≤ n)
⊢ firstn(n;L)[x] ~ L[x]

---

Latex:

---

Latex:
\mforall{}[L:Top  List].  \mforall{}[n:\mBbbN{}].  \mforall{}[x:\mBbbN{}n].    (firstn(n;L)[x]  \msim{}  L[x])


By

---

Latex:
xxx((UnivCD  THENA  Auto)  THEN  (Decide  \mkleeneopen{}||L||  \mleq{}  n\mkleeneclose{}\mcdot{}  THENA  Auto))xxx

---

Home Index