---

Step * 1 of Lemma select-filter-from-upto-order-preserving

.....assertion..... 
∀d:ℕ. ∀n,m:ℤ.
  (((m - n) ≤ d)
  ⇒ (∀P:{n..m-} ⟶ 𝔹. ∀i,j:ℕ||filter(P;[n, m))||.  (i < j ⇐⇒ filter(P;[n, m))[i] < filter(P;[n, m))[j])))
BY
{ (All Thin
   THEN (InstLemma `complete-nat-induction` [⌜λ2d.∀n,m:ℤ.
                                                    (((m - n) ≤ d)
                                                    ⇒ (∀P:{n..m-} ⟶ 𝔹. ∀i,j:ℕ||filter(P;[n, m))||.
                                                          (i < j ⇐⇒ filter(P;[n, m))[i] < filter(P;[n, m))[j])))⌝]⋅
         THENW Auto
         )
   THEN Try (Trivial)) }

1
.....antecedent..... 
∀n:ℕ
  ((∀m:ℕn. ∀n,m@0:ℤ.
      (((m@0 - n) ≤ m)
      ⇒ (∀P:{n..m@0-} ⟶ 𝔹. ∀i,j:ℕ||filter(P;[n, m@0))||.  (i < j ⇐⇒ filter(P;[n, m@0))[i] < filter(P;[n, m@0))[j]))))
  ⇒ (∀n@0,m:ℤ.
        (((m - n@0) ≤ n)
        ⇒ (∀P:{n@0..m-} ⟶ 𝔹. ∀i,j:ℕ||filter(P;[n@0, m))||.
              (i < j ⇐⇒ filter(P;[n@0, m))[i] < filter(P;[n@0, m))[j])))))

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}d:\mBbbN{}.  \mforall{}n,m:\mBbbZ{}.
    (((m  -  n)  \mleq{}  d)
    {}\mRightarrow{}  (\mforall{}P:\{n..m\msupminus{}\}  {}\mrightarrow{}  \mBbbB{}.  \mforall{}i,j:\mBbbN{}||filter(P;[n,  m))||.
                (i  <  j  \mLeftarrow{}{}\mRightarrow{}  filter(P;[n,  m))[i]  <  filter(P;[n,  m))[j])))


By

---

Latex:
(All  Thin
  THEN  (InstLemma  `complete-nat-induction`  [
              \mkleeneopen{}\mlambda{}\msubtwo{}d.\mforall{}n,m:\mBbbZ{}.
                            (((m  -  n)  \mleq{}  d)
                            {}\mRightarrow{}  (\mforall{}P:\{n..m\msupminus{}\}  {}\mrightarrow{}  \mBbbB{}.  \mforall{}i,j:\mBbbN{}||filter(P;[n,  m))||.
                                        (i  <  j  \mLeftarrow{}{}\mRightarrow{}  filter(P;[n,  m))[i]  <  filter(P;[n,  m))[j])))\mkleeneclose{}]\mcdot{}
              THENW  Auto
              )
  THEN  Try  (Trivial))

---

Home Index