---

Step * 3 2 1 1 of Lemma general-cantor-to-int-uniform-continuity-half-squashed


1. B : ℕ ⟶ ℕ+
2. F : (i:ℕ ⟶ ℕB[i]) ⟶ ℤ
3. M : n:ℕ ⟶ (ℕn ⟶ (i:ℕ × ℕB[i])) ⟶ (ℤ?)
4. ∀f:ℕ ⟶ (i:ℕ × ℕB[i])
     ((∃n:ℕ. ((M n f) = (inl ((λf.(F (λi.let j,n = f i in if (j =z i) then n else 0 fi ))) f)) ∈ (ℤ?)))
     ∧ (∀n:ℕ
          (M n f) = (inl ((λf.(F (λi.let j,n = f i in if (j =z i) then n else 0 fi ))) f)) ∈ (ℤ?) 
          supposing ↑isl(M n f)))
⊢ ∃M:n:ℕ ⟶ (i:ℕn ⟶ ℕB[i]) ⟶ (ℤ?) [(∀f:i:ℕ ⟶ ℕB[i]
                                        ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℤ?)))
                                        ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (ℤ?) supposing ↑isl(M n f))))]
BY
{ ((D 0 With ⌜λn,f. (M n (λi.<i, f i>))⌝  THENW Auto)
   THEN (D 0 THENA Auto)
   THEN (D -2 With ⌜λi.<i, f i>⌝  THENA Auto)
   THEN All Reduce
   THEN RepeatFor 3 (ParallelLast)
   THEN Try (ParallelLast)
   THEN EqCDA
   THEN (FunExt THENA Auto)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  B  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
2.  F  :  (i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  \mBbbZ{}
3.  M  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  (i:\mBbbN{}  \mtimes{}  \mBbbN{}B[i]))  {}\mrightarrow{}  (\mBbbZ{}?)
4.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  (i:\mBbbN{}  \mtimes{}  \mBbbN{}B[i])
          ((\mexists{}n:\mBbbN{}.  ((M  n  f)  =  (inl  ((\mlambda{}f.(F  (\mlambda{}i.let  j,n  =  f  i  in  if  (j  =\msubz{}  i)  then  n  else  0  fi  )))  f))))
          \mwedge{}  (\mforall{}n:\mBbbN{}
                    (M  n  f)  =  (inl  ((\mlambda{}f.(F  (\mlambda{}i.let  j,n  =  f  i  in  if  (j  =\msubz{}  i)  then  n  else  0  fi  )))  f)) 
                    supposing  \muparrow{}isl(M  n  f)))
\mvdash{}  \mexists{}M:n:\mBbbN{}  {}\mrightarrow{}  (i:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  (\mBbbZ{}?)  [(\mforall{}f:i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i]
                                                                                ((\mexists{}n:\mBbbN{}.  ((M  n  f)  =  (inl  (F  f))))
                                                                                \mwedge{}  (\mforall{}n:\mBbbN{}.  (M  n  f)  =  (inl  (F  f))  supposing  \muparrow{}isl(M  n  f))))]


By

---

Latex:
((D  0  With  \mkleeneopen{}\mlambda{}n,f.  (M  n  (\mlambda{}i.<i,  f  i>))\mkleeneclose{}    THENW  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (D  -2  With  \mkleeneopen{}\mlambda{}i.<i,  f  i>\mkleeneclose{}    THENA  Auto)
  THEN  All  Reduce
  THEN  RepeatFor  3  (ParallelLast)
  THEN  Try  (ParallelLast)
  THEN  EqCDA
  THEN  (FunExt  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index