---

Step * 2 1 of Lemma before-upto


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
BY
{ (RWO "length_upto" (-2) THEN Auto) }

---

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
7.  v  :  \mBbbN{}||upto(n)||
8.  (f  j)  =  v
\mvdash{}  v  <  n


By

---

Latex:
(RWO  "length\_upto"  (-2)  THEN  Auto)

---

Home Index