---

Step * of Lemma upto_decomp

∀[m:ℕ]. ∀[n:ℕm + 1].  (upto(m) ~ upto(n) @ map(λx.(x + n);upto(m - n)))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN Unfold `upto` 0) }

1
1. m : ℕ
2. n : ℕm + 1
⊢ [0, m) ~ [0, n) @ map(λx.(x + n);[0, m - n))

---

Latex:

---

Latex:
\mforall{}[m:\mBbbN{}].  \mforall{}[n:\mBbbN{}m  +  1].    (upto(m)  \msim{}  upto(n)  @  map(\mlambda{}x.(x  +  n);upto(m  -  n)))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  Unfold  `upto`  0)

---

Home Index