---

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


1. b : ℕ ⟶ ℕ
2. n : ℤ
3. 0 < n
4. ∀x,k:ℕ.  ((min-increasing-sequence(b;n - 1;x) = (inl k) ∈ (ℕ?)) ⇒ (x ≤ (b k)))
5. x : ℕ
6. k : ℕ
7. min-increasing-sequence(b;n;x) = (inl k) ∈ (ℕ?)
⊢ x ≤ (b k)
BY
{ (RepUR ``min-increasing-sequence`` (-1)
   THEN (RWO "primrec-unroll" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN Fold `min-increasing-sequence` (-1)
   THEN MoveToConcl (-1)
   THEN AutoSplit) }

1
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))

---

Latex:

---

Latex:

1.  b  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  \mforall{}x,k:\mBbbN{}.    ((min-increasing-sequence(b;n  -  1;x)  =  (inl  k))  {}\mRightarrow{}  (x  \mleq{}  (b  k)))
5.  x  :  \mBbbN{}
6.  k  :  \mBbbN{}
7.  min-increasing-sequence(b;n;x)  =  (inl  k)
\mvdash{}  x  \mleq{}  (b  k)


By

---

Latex:
(RepUR  ``min-increasing-sequence``  (-1)
  THEN  (RWO  "primrec-unroll"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  Fold  `min-increasing-sequence`  (-1)
  THEN  MoveToConcl  (-1)
  THEN  AutoSplit)

---

Home Index