---

Step * 2 2 2 of Lemma increasing_split


1. m : ℤ
2. [%1] : 0 < m
3. ∀[P:ℕm - 1 ⟶ ℙ]
     ((∀i:ℕm - 1. Dec(P i))
     ⇒ (∃n,k:ℕ
          ∃f:ℕn ⟶ ℕm - 1
           ∃g:ℕk ⟶ ℕm - 1
            (increasing(f;n)
            ∧ increasing(g;k)
            ∧ (∀i:ℕn. (P (f i)))
            ∧ (∀j:ℕk. (¬(P (g j))))
            ∧ (∀i:ℕm - 1. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))))))
4. [P] : ℕm ⟶ ℙ
5. ∀i:ℕm. Dec(P i)
6. n : ℕ
7. k : ℕ
8. f : ℕn ⟶ ℕm - 1
9. g : ℕk ⟶ ℕm - 1
10. increasing(f;n)
11. increasing(g;k)
12. ∀i:ℕn. (P (f i))
13. ∀j:ℕk. (¬(P (g j)))
14. ∀i:ℕm - 1. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))
15. ¬(P (m - 1))
⊢ ∃n,k:ℕ
   ∃f:ℕn ⟶ ℕm
    ∃g:ℕk ⟶ ℕm
     (increasing(f;n)
     ∧ increasing(g;k)
     ∧ (∀i:ℕn. (P (f i)))
     ∧ (∀j:ℕk. (¬(P (g j))))
     ∧ (∀i:ℕm. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))))
BY
{ TACTIC:(InstConcl [n;k + 1;f;g[k:=m - 1]]⋅ THENA Try (Complete (Auto'))) }

1
1. m : ℤ
2. [%1] : 0 < m
3. ∀[P:ℕm - 1 ⟶ ℙ]
     ((∀i:ℕm - 1. Dec(P i))
     ⇒ (∃n,k:ℕ
          ∃f:ℕn ⟶ ℕm - 1
           ∃g:ℕk ⟶ ℕm - 1
            (increasing(f;n)
            ∧ increasing(g;k)
            ∧ (∀i:ℕn. (P (f i)))
            ∧ (∀j:ℕk. (¬(P (g j))))
            ∧ (∀i:ℕm - 1. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))))))
4. [P] : ℕm ⟶ ℙ
5. ∀i:ℕm. Dec(P i)
6. n : ℕ
7. k : ℕ
8. f : ℕn ⟶ ℕm - 1
9. g : ℕk ⟶ ℕm - 1
10. increasing(f;n)
11. increasing(g;k)
12. ∀i:ℕn. (P (f i))
13. ∀j:ℕk. (¬(P (g j)))
14. ∀i:ℕm - 1. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))
15. ¬(P (m - 1))
⊢ increasing(f;n)
∧ increasing(g[k:=m - 1];k + 1)
∧ (∀i:ℕn. (P (f i)))
∧ (∀j:ℕk + 1. (¬(P (g[k:=m - 1] j))))
∧ (∀i:ℕm. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk + 1. (i = (g[k:=m - 1] j) ∈ ℤ))))

---

Latex:

---

Latex:

1.  m  :  \mBbbZ{}
2.  [\%1]  :  0  <  m
3.  \mforall{}[P:\mBbbN{}m  -  1  {}\mrightarrow{}  \mBbbP{}]
          ((\mforall{}i:\mBbbN{}m  -  1.  Dec(P  i))
          {}\mRightarrow{}  (\mexists{}n,k:\mBbbN{}
                    \mexists{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}m  -  1
                      \mexists{}g:\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}m  -  1
                        (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{}m  -  1.  ((\mexists{}j:\mBbbN{}n.  (i  =  (f  j)))  \mvee{}  (\mexists{}j:\mBbbN{}k.  (i  =  (g  j))))))))
4.  [P]  :  \mBbbN{}m  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}i:\mBbbN{}m.  Dec(P  i)
6.  n  :  \mBbbN{}
7.  k  :  \mBbbN{}
8.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}m  -  1
9.  g  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbN{}m  -  1
10.  increasing(f;n)
11.  increasing(g;k)
12.  \mforall{}i:\mBbbN{}n.  (P  (f  i))
13.  \mforall{}j:\mBbbN{}k.  (\mneg{}(P  (g  j)))
14.  \mforall{}i:\mBbbN{}m  -  1.  ((\mexists{}j:\mBbbN{}n.  (i  =  (f  j)))  \mvee{}  (\mexists{}j:\mBbbN{}k.  (i  =  (g  j))))
15.  \mneg{}(P  (m  -  1))
\mvdash{}  \mexists{}n,k:\mBbbN{}
      \mexists{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}m
        \mexists{}g:\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}m
          (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{}m.  ((\mexists{}j:\mBbbN{}n.  (i  =  (f  j)))  \mvee{}  (\mexists{}j:\mBbbN{}k.  (i  =  (g  j))))))


By

---

Latex:
TACTIC:(InstConcl  [n;k  +  1;f;g[k:=m  -  1]]\mcdot{}  THENA  Try  (Complete  (Auto')))

---

Home Index