---

Step * of Lemma upto_iseg

∀i,j:ℕ.  upto(i) ≤ upto(j) supposing i ≤ j
BY
{ (((Auto THEN Unfold `iseg` 0 THEN (InstLemma `upto_decomp` [⌜j⌝; ⌜i⌝])⋅) THENA Auto)
   THEN (HypSubst (-1) 0)
   THEN (InstConcl [⌜map(λx.(x + i);upto(j - i))⌝])⋅
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}i,j:\mBbbN{}.    upto(i)  \mleq{}  upto(j)  supposing  i  \mleq{}  j


By

---

Latex:
(((Auto  THEN  Unfold  `iseg`  0  THEN  (InstLemma  `upto\_decomp`  [\mkleeneopen{}j\mkleeneclose{};  \mkleeneopen{}i\mkleeneclose{}])\mcdot{})  THENA  Auto)
  THEN  (HypSubst  (-1)  0)
  THEN  (InstConcl  [\mkleeneopen{}map(\mlambda{}x.(x  +  i);upto(j  -  i))\mkleeneclose{}])\mcdot{}
  THEN  Auto')

---

Home Index