---

Step * 1 of Lemma increasing_split

.....basecase..... 
∀[P:ℕ0 ⟶ ℙ]
  ((∀i:ℕ0. Dec(P i))
  ⇒ (∃n,k:ℕ
       ∃f:ℕn ⟶ ℕ0
        ∃g:ℕk ⟶ ℕ0
         (increasing(f;n)
         ∧ increasing(g;k)
         ∧ (∀i:ℕn. (P (f i)))
         ∧ (∀j:ℕk. (¬(P (g j))))
         ∧ (∀i:ℕ0. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))))))
BY
{ (((Auto THEN InstConcl [0;0;λi.i;λi.i]) THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:
.....basecase..... 
\mforall{}[P:\mBbbN{}0  {}\mrightarrow{}  \mBbbP{}]
    ((\mforall{}i:\mBbbN{}0.  Dec(P  i))
    {}\mRightarrow{}  (\mexists{}n,k:\mBbbN{}
              \mexists{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}0
                \mexists{}g:\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}0
                  (increasing(f;n)
                  \mwedge{}  increasing(g;k)
                  \mwedge{}  (\mforall{}i:\mBbbN{}n.  (P  (f  i)))
                  \mwedge{}  (\mforall{}j:\mBbbN{}k.  (\mneg{}(P  (g  j))))
                  \mwedge{}  (\mforall{}i:\mBbbN{}0.  ((\mexists{}j:\mBbbN{}n.  (i  =  (f  j)))  \mvee{}  (\mexists{}j:\mBbbN{}k.  (i  =  (g  j))))))))


By

---

Latex:
(((Auto  THEN  InstConcl  [0;0;\mlambda{}i.i;\mlambda{}i.i])  THEN  Reduce  0)  THEN  Auto)

---

Home Index