---

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


1. F : (ℕ+ ⟶ ℤ) ⟶ 𝔹
2. H : (ℕ+ ⟶ ℤ) ⟶ 𝔹
3. f : ℕ+ ⟶ ℤ
4. G : n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} 
5. n1 : ℕ
6. ∀g:ℕ ⟶ ℤ
     (((λn.(f (n + 1))) = g ∈ (ℕn1 ⟶ ℤ))
     ⇒ (if F (λn.(f ((n - 1) + 1))) then 1 else 0 fi  = if F (λn.(g (n - 1))) then 1 else 0 fi  ∈ ℕ))
7. n : ℕ
8. ∀g:ℕ ⟶ ℤ
     (((λn.(f (n + 1))) = g ∈ (ℕn ⟶ ℤ))
     ⇒ (if H (λn.(f ((n - 1) + 1))) then 1 else 0 fi  = if H (λn.(g (n - 1))) then 1 else 0 fi  ∈ ℕ))
9. ∀k:ℕ. ((λn.(f (n + 1))) = (λi.(G (k + 1) (i + 1))) ∈ (ℕk ⟶ ℤ))
10. (λn.(f (n + 1))) = (λi.(G (imax(n;n1) + 1) (i + 1))) ∈ (ℕimax(n;n1) ⟶ ℤ)
⊢ ∃n:ℕ. (F f = F (G (n + 1)) ∧ H f = H (G (n + 1)))
BY
{ ((InstHyp [⌜λi.(G (imax(n;n1) + 1) (i + 1))⌝] (-5)⋅ THENA Auto)
   THEN (InstHyp [⌜λi.(G (imax(n;n1) + 1) (i + 1))⌝] (-4)⋅ THENA Auto)
   ) }

1
1. F : (ℕ+ ⟶ ℤ) ⟶ 𝔹
2. H : (ℕ+ ⟶ ℤ) ⟶ 𝔹
3. f : ℕ+ ⟶ ℤ
4. G : n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} 
5. n1 : ℕ
6. ∀g:ℕ ⟶ ℤ
     (((λn.(f (n + 1))) = g ∈ (ℕn1 ⟶ ℤ))
     ⇒ (if F (λn.(f ((n - 1) + 1))) then 1 else 0 fi  = if F (λn.(g (n - 1))) then 1 else 0 fi  ∈ ℕ))
7. n : ℕ
8. ∀g:ℕ ⟶ ℤ
     (((λn.(f (n + 1))) = g ∈ (ℕn ⟶ ℤ))
     ⇒ (if H (λn.(f ((n - 1) + 1))) then 1 else 0 fi  = if H (λn.(g (n - 1))) then 1 else 0 fi  ∈ ℕ))
9. ∀k:ℕ. ((λn.(f (n + 1))) = (λi.(G (k + 1) (i + 1))) ∈ (ℕk ⟶ ℤ))
10. (λn.(f (n + 1))) = (λi.(G (imax(n;n1) + 1) (i + 1))) ∈ (ℕimax(n;n1) ⟶ ℤ)
11. if F (λn.(f ((n - 1) + 1))) then 1 else 0 fi 
= if F (λn@0.((λi.(G (imax(n;n1) + 1) (i + 1))) (n@0 - 1))) then 1 else 0 fi 
∈ ℕ
12. if H (λn.(f ((n - 1) + 1))) then 1 else 0 fi 
= if H (λn@0.((λi.(G (imax(n;n1) + 1) (i + 1))) (n@0 - 1))) then 1 else 0 fi 
∈ ℕ
⊢ ∃n:ℕ. (F f = F (G (n + 1)) ∧ H f = H (G (n + 1)))

---

Latex:

---

Latex:

1.  F  :  (\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{})  {}\mrightarrow{}  \mBbbB{}
2.  H  :  (\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{})  {}\mrightarrow{}  \mBbbB{}
3.  f  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
4.  G  :  n:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \{g:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  f  =  g\} 
5.  n1  :  \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.  n  :  \mBbbN{}
8.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbZ{}
          (((\mlambda{}n.(f  (n  +  1)))  =  g)
          {}\mRightarrow{}  (if  H  (\mlambda{}n.(f  ((n  -  1)  +  1)))  then  1  else  0  fi    =  if  H  (\mlambda{}n.(g  (n  -  1)))  then  1  else  0  fi  ))
9.  \mforall{}k:\mBbbN{}.  ((\mlambda{}n.(f  (n  +  1)))  =  (\mlambda{}i.(G  (k  +  1)  (i  +  1))))
10.  (\mlambda{}n.(f  (n  +  1)))  =  (\mlambda{}i.(G  (imax(n;n1)  +  1)  (i  +  1)))
\mvdash{}  \mexists{}n:\mBbbN{}.  (F  f  =  F  (G  (n  +  1))  \mwedge{}  H  f  =  H  (G  (n  +  1)))


By

---

Latex:
((InstHyp  [\mkleeneopen{}\mlambda{}i.(G  (imax(n;n1)  +  1)  (i  +  1))\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}i.(G  (imax(n;n1)  +  1)  (i  +  1))\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  )

---

Home Index