---

Step * 2 1 of Lemma min-increasing-sequence-prop1


1. b : ℕ ⟶ ℕ
2. n : ℤ
3. ¬n < 1
4. 0 < n
5. ∀x,k:ℕ.  ((min-increasing-sequence(b;n - 1;x) = (inl k) ∈ (ℕ?)) ⇒ (x ≤ (b k)))
6. x : ℕ
7. k : ℕ
⊢ (case min-increasing-sequence(b;n - 1;x)
 of inl(x@0) =>
 inl x@0
 | inr(x@0) =>
 if x ≤z b (n - 1) then inl (n - 1) else inr ⋅  fi 
= (inl k)
∈ (ℕ?))
⇒ (x ≤ (b k))
BY
{ (GenConclAtAddr [1;2;1] THEN DVar `v' THEN Reduce 0 THEN (AutoSplit ORELSE Auto)) }

---

Latex:

---

Latex:

1.  b  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  n  :  \mBbbZ{}
3.  \mneg{}n  <  1
4.  0  <  n
5.  \mforall{}x,k:\mBbbN{}.    ((min-increasing-sequence(b;n  -  1;x)  =  (inl  k))  {}\mRightarrow{}  (x  \mleq{}  (b  k)))
6.  x  :  \mBbbN{}
7.  k  :  \mBbbN{}
\mvdash{}  (case  min-increasing-sequence(b;n  -  1;x)
  of  inl(x@0)  =>
  inl  x@0
  |  inr(x@0)  =>
  if  x  \mleq{}z  b  (n  -  1)  then  inl  (n  -  1)  else  inr  \mcdot{}    fi 
=  (inl  k))
{}\mRightarrow{}  (x  \mleq{}  (b  k))


By

---

Latex:
(GenConclAtAddr  [1;2;1]  THEN  DVar  `v'  THEN  Reduce  0  THEN  (AutoSplit  ORELSE  Auto))

---

Home Index