---

Step * 1 1 1 1 1 1 of Lemma general-cantor-to-int-uniform-continuity


1. B : ℕ ⟶ ℕ+
2. F : (k:ℕ ⟶ ℕB[k]) ⟶ ℤ
3. n : ℕ
4. ∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ))
5. j : ℕ
6. j < n
7. finite(i:ℕn ⟶ ℕB[i])
8. ∀p,q:i:ℕn ⟶ ℕB[i].  Dec(∀i:ℕj. ((p i) = (q i) ∈ ℕB[i]))
9. ∀p,q:i:ℕn ⟶ ℕB[i].  Dec(p = q ∈ (i:ℕj ⟶ ℕB[i]))
⊢ Dec(∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕj ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ)))
BY
{ (Assert Dec(∃p,q:i:ℕn ⟶ ℕB[i]
               ((p = q ∈ (i:ℕj ⟶ ℕB[i]))
               ∧ (¬((F (λi.if i <z n then p i else 0 fi )) = (F (λi.if i <z n then q i else 0 fi )) ∈ ℤ)))) BY
         RepeatFor 2 ((BLemma `decidable-exists-finite` THEN Auto))) }

1
1. B : ℕ ⟶ ℕ+
2. F : (k:ℕ ⟶ ℕB[k]) ⟶ ℤ
3. n : ℕ
4. ∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ))
5. j : ℕ
6. j < n
7. finite(i:ℕn ⟶ ℕB[i])
8. ∀p,q:i:ℕn ⟶ ℕB[i].  Dec(∀i:ℕj. ((p i) = (q i) ∈ ℕB[i]))
9. ∀p,q:i:ℕn ⟶ ℕB[i].  Dec(p = q ∈ (i:ℕj ⟶ ℕB[i]))
10. Dec(∃p,q:i:ℕn ⟶ ℕB[i]
         ((p = q ∈ (i:ℕj ⟶ ℕB[i]))
         ∧ (¬((F (λi.if i <z n then p i else 0 fi )) = (F (λi.if i <z n then q i else 0 fi )) ∈ ℤ))))
⊢ Dec(∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕj ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ)))

---

Latex:

---

Latex:

1.  B  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
2.  F  :  (k:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[k])  {}\mrightarrow{}  \mBbbZ{}
3.  n  :  \mBbbN{}
4.  \mforall{}f,g:i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i].    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g)))
5.  j  :  \mBbbN{}
6.  j  <  n
7.  finite(i:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}B[i])
8.  \mforall{}p,q:i:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}B[i].    Dec(\mforall{}i:\mBbbN{}j.  ((p  i)  =  (q  i)))
9.  \mforall{}p,q:i:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}B[i].    Dec(p  =  q)
\mvdash{}  Dec(\mforall{}f,g:i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i].    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g))))


By

---

Latex:
(Assert  Dec(\mexists{}p,q:i:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}B[i]
                          ((p  =  q)
                          \mwedge{}  (\mneg{}((F  (\mlambda{}i.if  i  <z  n  then  p  i  else  0  fi  ))
                              =  (F  (\mlambda{}i.if  i  <z  n  then  q  i  else  0  fi  ))))))  BY
              RepeatFor  2  ((BLemma  `decidable-exists-finite`  THEN  Auto)))

---

Home Index