---

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


1. F : (ℕ+ ⟶ ℤ) ⟶ 𝔹
2. f : ℕ+ ⟶ ℤ
3. G : n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} 
4. ⇃(∃n:ℕ
      ∀g:ℕ ⟶ ℤ
        (((λn.(f (n + 1))) = g ∈ (ℕn ⟶ ℤ))
        ⇒ (if F (λn.(f ((n - 1) + 1))) then 1 else 0 fi  = if F (λn.(g (n - 1))) then 1 else 0 fi  ∈ ℕ)))
5. n : ℕ
6. ∀g:ℕ ⟶ ℤ
     (((λn.(f (n + 1))) = g ∈ (ℕn ⟶ ℤ))
     ⇒ (if F (λn.(f ((n - 1) + 1))) then 1 else 0 fi  = if F (λn.(g (n - 1))) then 1 else 0 fi  ∈ ℕ))
7. x : ℕn
⊢ (f (x + 1)) = (G (n + 1) (x + 1)) ∈ ℤ
BY
{ (GenConclTerm ⌜G (n + 1)⌝⋅ THENA Auto) }

1
1. F : (ℕ+ ⟶ ℤ) ⟶ 𝔹
2. f : ℕ+ ⟶ ℤ
3. G : n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} 
4. ⇃(∃n:ℕ
      ∀g:ℕ ⟶ ℤ
        (((λn.(f (n + 1))) = g ∈ (ℕn ⟶ ℤ))
        ⇒ (if F (λn.(f ((n - 1) + 1))) then 1 else 0 fi  = if F (λn.(g (n - 1))) then 1 else 0 fi  ∈ ℕ)))
5. n : ℕ
6. ∀g:ℕ ⟶ ℤ
     (((λn.(f (n + 1))) = g ∈ (ℕn ⟶ ℤ))
     ⇒ (if F (λn.(f ((n - 1) + 1))) then 1 else 0 fi  = if F (λn.(g (n - 1))) then 1 else 0 fi  ∈ ℕ))
7. x : ℕn
8. v : {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n + 1 ⟶ ℤ)} 
9. (G (n + 1)) = v ∈ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n + 1 ⟶ ℤ)} 
⊢ (f (x + 1)) = (v (x + 1)) ∈ ℤ

---

Latex:

---

Latex:

1.  F  :  (\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{})  {}\mrightarrow{}  \mBbbB{}
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{}  (if  F  (\mlambda{}n.(f  ((n  -  1)  +  1)))  then  1  else  0  fi 
                      =  if  F  (\mlambda{}n.(g  (n  -  1)))  then  1  else  0  fi  )))
5.  n  :  \mBbbN{}
6.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbZ{}
          (((\mlambda{}n.(f  (n  +  1)))  =  g)
          {}\mRightarrow{}  (if  F  (\mlambda{}n.(f  ((n  -  1)  +  1)))  then  1  else  0  fi    =  if  F  (\mlambda{}n.(g  (n  -  1)))  then  1  else  0  fi  ))
7.  x  :  \mBbbN{}n
\mvdash{}  (f  (x  +  1))  =  (G  (n  +  1)  (x  +  1))


By

---

Latex:
(GenConclTerm  \mkleeneopen{}G  (n  +  1)\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index