---

Step * 1 of Lemma upto_decomp


1. m : ℕ
2. n : ℕm + 1
⊢ [0, m) ~ [0, n) @ map(λx.(x + n);[0, m - n))
BY
{ ((InstLemma `from-upto-split` [⌜0⌝;⌜m⌝;⌜n⌝]⋅ THENA Auto) THEN HypSubst' (-1) 0 THEN EqCD) }

1
1. m : ℕ
2. n : ℕm + 1
3. [0, m) ~ [0, n) @ [n, m)
⊢ [0, n) ~ [0, n)

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

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}
2.  n  :  \mBbbN{}m  +  1
\mvdash{}  [0,  m)  \msim{}  [0,  n)  @  map(\mlambda{}x.(x  +  n);[0,  m  -  n))


By

---

Latex:
((InstLemma  `from-upto-split`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  HypSubst'  (-1)  0  THEN  EqCD)

---

Home Index