---

Step * 3 of Lemma select_concat

.....antecedent..... 
1. [T] : Type
⊢ ∀n:ℕ||concat([])||
    ∃m:ℕ||[]||
     ((||concat(firstn(m;[]))|| ≤ n)
     c∧ n - ||concat(firstn(m;[]))|| < ||[][m]||
     c∧ (concat([])[n] = [][m][n - ||concat(firstn(m;[]))||] ∈ T))
BY
{ (Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  [T]  :  Type
\mvdash{}  \mforall{}n:\mBbbN{}||concat([])||
        \mexists{}m:\mBbbN{}||[]||
          ((||concat(firstn(m;[]))||  \mleq{}  n)
          c\mwedge{}  n  -  ||concat(firstn(m;[]))||  <  ||[][m]||
          c\mwedge{}  (concat([])[n]  =  [][m][n  -  ||concat(firstn(m;[]))||]))


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index