---

Step * of Lemma firstn_upto

∀[n,m:ℕ].  (firstn(n;upto(m)) ~ if n ≤z m then upto(n) else upto(m) fi )
BY
{ (((UnivCD THENA Auto) THEN SplitOnConclITE) THENA Auto) }

1
.....truecase..... 
1. n : ℕ
2. m : ℕ
3. n ≤ m
⊢ firstn(n;upto(m)) ~ upto(n)

2
.....falsecase..... 
1. n : ℕ
2. m : ℕ
3. m < n
⊢ firstn(n;upto(m)) ~ upto(m)

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbN{}].    (firstn(n;upto(m))  \msim{}  if  n  \mleq{}z  m  then  upto(n)  else  upto(m)  fi  )


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  SplitOnConclITE)  THENA  Auto)

---

Home Index