---

Step * 2 of Lemma before-upto


1. n : ℕ
2. x : ℕn
3. y : ℕn
4. f : ℕ2 ⟶ ℕ||upto(n)||
5. increasing(f;2)
6. j : ℕ2
⊢ f j < n
BY
{ (GenConclTerm ⌜f j⌝⋅ THENA Auto) }

1
1. n : ℕ
2. x : ℕn
3. y : ℕn
4. f : ℕ2 ⟶ ℕ||upto(n)||
5. increasing(f;2)
6. j : ℕ2
7. v : ℕ||upto(n)||
8. (f j) = v ∈ ℕ||upto(n)||
⊢ v < n

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  x  :  \mBbbN{}n
3.  y  :  \mBbbN{}n
4.  f  :  \mBbbN{}2  {}\mrightarrow{}  \mBbbN{}||upto(n)||
5.  increasing(f;2)
6.  j  :  \mBbbN{}2
\mvdash{}  f  j  <  n


By

---

Latex:
(GenConclTerm  \mkleeneopen{}f  j\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index