Proof of Nuprl Lemma : increasing

Step * 2 2 2 1 1 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) ∈ ℤ)))))))

⊢ (∀i:ℕ(k + 1) - 1. if (i =_z k) then m - 1 else g i fi  < if (i + 1 =_z k) then m - 1 else g (i + 1) fi )

∧ (∀j:ℕk + 1. (¬(P if (j =_z k) then m - 1 else g j fi )))

∧ (∀i:ℕm. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk + 1. (i = if (j =_z k) then m - 1 else g j fi  ∈ ℤ))))

BY
{ RepeatFor 2 ((D 0 THENA Auto)) }

1
1. m : ℤ
2. 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))
16. i : ℕ(k + 1) - 1
⊢ if (i =_z k) then m - 1 else g i fi  < if (i + 1 =_z k) then m - 1 else g (i + 1) fi

2
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))
⊢ ∀j:ℕk + 1. (¬(P if (j =_z k) then m - 1 else g j fi ))

3
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) ∈ ℤ)))))))

⊢ ∀i:ℕm. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk + 1. (i = if (j =_z k) then m - 1 else g j fi  ∈ ℤ)))

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{} (\mforall{}i:\mBbbN{}(k + 1) - 1 if (i =\msubz{} k) then m - 1 else g i fi < if (i + 1 =\msubz{} k) then m - 1 else g (i + 1) fi ) \mwedge{} (\mforall{}j:\mBbbN{}k + 1. (\mneg{}(P if (j =\msubz{} k) then m - 1 else g j fi ))) \mwedge{} (\mforall{}i:\mBbbN{}m. ((\mexists{}j:\mBbbN{}n. (i = (f j))) \mvee{} (\mexists{}j:\mBbbN{}k + 1. (i = if (j =\msubz{} k) then m - 1 else g j fi )))) By Latex: RepeatFor 2 ((D 0 THENA Auto)) Home Index