---

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

.....assertion..... 
1. F : (ℕ+ ⟶ ℤ) ⟶ ℕ
2. f : ℕ+ ⟶ ℤ
3. G : n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} 
4. ⇃(∃n:ℕ. ∀g:ℕ ⟶ ℤ. (((λn.(f (n + 1))) = g ∈ (ℕn ⟶ ℤ)) ⇒ ((F (λn.(f ((n - 1) + 1)))) = (F (λn.(g (n - 1)))) ∈ ℕ)))
⊢ ↓∃n:ℕ. ((F f) = (F (G (n + 1))) ∈ ℕ)
BY
{ ((InstLemma `squash-from-quotient` [⌜∃n:ℕ
                                        ∀g:ℕ ⟶ ℤ
                                          (((λn.(f (n + 1))) = g ∈ (ℕn ⟶ ℤ))
                                          ⇒ ((F (λn.(f ((n - 1) + 1)))) = (F (λn.(g (n - 1)))) ∈ ℕ))⌝]⋅
    THENA Auto
    )
   THEN RepeatFor 2 (ParallelLast)
   ) }

1
1. F : (ℕ+ ⟶ ℤ) ⟶ ℕ
2. f : ℕ+ ⟶ ℤ
3. G : n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} 
4. ⇃(∃n:ℕ. ∀g:ℕ ⟶ ℤ. (((λn.(f (n + 1))) = g ∈ (ℕn ⟶ ℤ)) ⇒ ((F (λn.(f ((n - 1) + 1)))) = (F (λn.(g (n - 1)))) ∈ ℕ)))
5. n : ℕ
6. ∀g:ℕ ⟶ ℤ. (((λn.(f (n + 1))) = g ∈ (ℕn ⟶ ℤ)) ⇒ ((F (λn.(f ((n - 1) + 1)))) = (F (λn.(g (n - 1)))) ∈ ℕ))
⊢ (F f) = (F (G (n + 1))) ∈ ℕ

---

Latex:

---

Latex:
.....assertion..... 
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)))))))
\mvdash{}  \mdownarrow{}\mexists{}n:\mBbbN{}.  ((F  f)  =  (F  (G  (n  +  1))))


By

---

Latex:
((InstLemma  `squash-from-quotient`  [\mkleeneopen{}\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))))))\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  RepeatFor  2  (ParallelLast)
  )

---

Home Index