Step * 1 1 2 of Lemma weak-continuity-principle-nat+-int-nat


1. (ℕ+ ⟶ ℤ) ⟶ ℕ
2. : ℕ+ ⟶ ℤ
3. n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤg ∈ (ℕ+n ⟶ ℤ)} 
4. ⇃(∃n:ℕ. ∀g:ℕ ⟶ ℤ(((λn.(f (n 1))) g ∈ (ℕn ⟶ ℤ))  ((F n.(f ((n 1) 1)))) (F n.(g (n 1)))) ∈ ℕ)))
5. : ℕ
6. ∀g:ℕ ⟶ ℤ(((λn.(f (n 1))) g ∈ (ℕn ⟶ ℤ))  ((F n.(f ((n 1) 1)))) (F n.(g (n 1)))) ∈ ℕ))
7. (F n.(f ((n 1) 1)))) (F n@0.((λi.(G (n 1) (i 1))) (n@0 1)))) ∈ ℕ
⊢ (F f) (F (G (n 1))) ∈ ℕ
BY
(Subst' n.(f ((n 1) 1))) f ∈ (ℕ+ ⟶ ℤ-1 THENA Auto) }

1
1. (ℕ+ ⟶ ℤ) ⟶ ℕ
2. : ℕ+ ⟶ ℤ
3. n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤg ∈ (ℕ+n ⟶ ℤ)} 
4. ⇃(∃n:ℕ. ∀g:ℕ ⟶ ℤ(((λn.(f (n 1))) g ∈ (ℕn ⟶ ℤ))  ((F n.(f ((n 1) 1)))) (F n.(g (n 1)))) ∈ ℕ)))
5. : ℕ
6. ∀g:ℕ ⟶ ℤ(((λn.(f (n 1))) g ∈ (ℕn ⟶ ℤ))  ((F n.(f ((n 1) 1)))) (F n.(g (n 1)))) ∈ ℕ))
7. (F f) (F n@0.((λi.(G (n 1) (i 1))) (n@0 1)))) ∈ ℕ
⊢ (F f) (F (G (n 1))) ∈ ℕ


Latex:


Latex:

1.  F  :  (\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{})  {}\mrightarrow{}  \mBbbN{}
2.  f  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  G  :  n:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \{g:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  f  =  g\} 
4.  \00D9(\mexists{}n:\mBbbN{}
            \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbZ{}.  (((\mlambda{}n.(f  (n  +  1)))  =  g)  {}\mRightarrow{}  ((F  (\mlambda{}n.(f  ((n  -  1)  +  1))))  =  (F  (\mlambda{}n.(g  (n  -  1)))))))
5.  n  :  \mBbbN{}
6.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbZ{}.  (((\mlambda{}n.(f  (n  +  1)))  =  g)  {}\mRightarrow{}  ((F  (\mlambda{}n.(f  ((n  -  1)  +  1))))  =  (F  (\mlambda{}n.(g  (n  -  1))))))
7.  (F  (\mlambda{}n.(f  ((n  -  1)  +  1))))  =  (F  (\mlambda{}n@0.((\mlambda{}i.(G  (n  +  1)  (i  +  1)))  (n@0  -  1))))
\mvdash{}  (F  f)  =  (F  (G  (n  +  1)))


By


Latex:
(Subst'  (\mlambda{}n.(f  ((n  -  1)  +  1)))  =  f  -1  THENA  Auto)




Home Index