---

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

.....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])))))
BY
{ (RepeatFor 6 ((D 0 THENA Auto))
   THEN RecUnfold `from-upto` 0
   THEN RenameVar `k' (-4)
   THEN (SplitOnConclITE THENA Auto)
   THEN Reduce 0
   THEN ((SplitOnConclITE THENA Auto) ORELSE Auto)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (InstHyp [⌜n - 1⌝;⌜k + 1⌝;⌜m⌝;⌜P⌝] 2⋅ THENA Auto)
   THEN Try (Trivial)) }

1
1. n : ℕ
2. ∀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])))
3. k : ℤ
4. m : ℤ
5. (m - k) ≤ n
6. P : {k..m-} ⟶ 𝔹
7. k < m
8. ↑(P k)
9. ∀i,j:ℕ||filter(P;[k + 1, m))||.  (i < j ⇐⇒ filter(P;[k + 1, m))[i] < filter(P;[k + 1, m))[j])
⊢ ∀i,j:ℕ||[k / filter(P;[k + 1, m))]||.  (i < j ⇐⇒ [k / filter(P;[k + 1, m))][i] < [k / filter(P;[k + 1, m))][j])

---

Latex:

---

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


By

---

Latex:
(RepeatFor  6  ((D  0  THENA  Auto))
  THEN  RecUnfold  `from-upto`  0
  THEN  RenameVar  `k'  (-4)
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Reduce  0
  THEN  ((SplitOnConclITE  THENA  Auto)  ORELSE  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}n  -  1\mkleeneclose{};\mkleeneopen{}k  +  1\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]  2\mcdot{}  THENA  Auto)
  THEN  Try  (Trivial))

---

Home Index