---

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

∀F:(ℕ+ ⟶ ℤ) ⟶ 𝔹. ∀f:ℕ+ ⟶ ℤ. ∀G:n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} .  ∃n:ℕ+. F f = F (G n)
BY
{ Extract of Obid: weak-continuity-principle-nat+-int-bool
  normalizes to:
  
  λF,f,G. <mu(λn.F f =b F (G (n + 1))) + 1, Ax>
  
  not unfolding  mu eq_bool
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}F:(\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{})  {}\mrightarrow{}  \mBbbB{}.  \mforall{}f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}G:n:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \{g:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  f  =  g\}  .    \mexists{}n:\mBbbN{}\msupplus{}.  F  f  =  F  (G  n)


By

---

Latex:
Extract  of  Obid:  weak-continuity-principle-nat+-int-bool
normalizes  to:

\mlambda{}F,f,G.  <mu(\mlambda{}n.F  f  =b  F  (G  (n  +  1)))  +  1,  Ax>

not  unfolding    mu  eq\_bool
finishing  with  Auto

---

Home Index