---

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

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

---

Latex:

---

Latex:
\mforall{}F,H:(\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)  \mwedge{}  H  f  =  H  (G  n))


By

---

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

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

not  unfolding    mu  eq\_bool  band
finishing  with  Auto

---

Home Index