---

Step * 2 1 1 1 1 of Lemma CCC-bool


1. R : ℕ ⟶ 𝔹 ⟶ ℙ
2. B : ℕ
3. h : f:(ℕB ⟶ 𝔹) ⟶ ℕB
4. ∀f:ℕB ⟶ 𝔹. (R (h f) (f (h f)))
5. finite(ℕB ⟶ 𝔹)
6. ∀[P:(ℕB ⟶ 𝔹) ⟶ ℙ]. ((∀t:ℕB ⟶ 𝔹. Dec(P[t])) ⇒ Dec(∃t:ℕB ⟶ 𝔹. P[t]))
7. ∀[P:(ℕB ⟶ 𝔹) ⟶ ℙ]. ((∀t:ℕB ⟶ 𝔹. Dec(P[t])) ⇒ Dec(∀t:ℕB ⟶ 𝔹. P[t]))
⊢ ∃n:ℕ. ∀m:𝔹. (R n m)
BY
{ (Decide ⌜∃f,g:ℕB ⟶ 𝔹. (((h f) = (h g) ∈ ℤ) ∧ (¬f (h f) = g (h g)))⌝⋅ THENA Auto) }

1
1. R : ℕ ⟶ 𝔹 ⟶ ℙ
2. B : ℕ
3. h : f:(ℕB ⟶ 𝔹) ⟶ ℕB
4. ∀f:ℕB ⟶ 𝔹. (R (h f) (f (h f)))
5. finite(ℕB ⟶ 𝔹)
6. ∀[P:(ℕB ⟶ 𝔹) ⟶ ℙ]. ((∀t:ℕB ⟶ 𝔹. Dec(P[t])) ⇒ Dec(∃t:ℕB ⟶ 𝔹. P[t]))
7. ∀[P:(ℕB ⟶ 𝔹) ⟶ ℙ]. ((∀t:ℕB ⟶ 𝔹. Dec(P[t])) ⇒ Dec(∀t:ℕB ⟶ 𝔹. P[t]))
8. ∃f,g:ℕB ⟶ 𝔹. (((h f) = (h g) ∈ ℤ) ∧ (¬f (h f) = g (h g)))
⊢ ∃n:ℕ. ∀m:𝔹. (R n m)

2
1. R : ℕ ⟶ 𝔹 ⟶ ℙ
2. B : ℕ
3. h : f:(ℕB ⟶ 𝔹) ⟶ ℕB
4. ∀f:ℕB ⟶ 𝔹. (R (h f) (f (h f)))
5. finite(ℕB ⟶ 𝔹)
6. ∀[P:(ℕB ⟶ 𝔹) ⟶ ℙ]. ((∀t:ℕB ⟶ 𝔹. Dec(P[t])) ⇒ Dec(∃t:ℕB ⟶ 𝔹. P[t]))
7. ∀[P:(ℕB ⟶ 𝔹) ⟶ ℙ]. ((∀t:ℕB ⟶ 𝔹. Dec(P[t])) ⇒ Dec(∀t:ℕB ⟶ 𝔹. P[t]))
8. ¬(∃f,g:ℕB ⟶ 𝔹. (((h f) = (h g) ∈ ℤ) ∧ (¬f (h f) = g (h g))))
⊢ ∃n:ℕ. ∀m:𝔹. (R n m)

---

Latex:

---

Latex:

1.  R  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}  {}\mrightarrow{}  \mBbbP{}
2.  B  :  \mBbbN{}
3.  h  :  f:(\mBbbN{}B  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}B
4.  \mforall{}f:\mBbbN{}B  {}\mrightarrow{}  \mBbbB{}.  (R  (h  f)  (f  (h  f)))
5.  finite(\mBbbN{}B  {}\mrightarrow{}  \mBbbB{})
6.  \mforall{}[P:(\mBbbN{}B  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}t:\mBbbN{}B  {}\mrightarrow{}  \mBbbB{}.  Dec(P[t]))  {}\mRightarrow{}  Dec(\mexists{}t:\mBbbN{}B  {}\mrightarrow{}  \mBbbB{}.  P[t]))
7.  \mforall{}[P:(\mBbbN{}B  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}t:\mBbbN{}B  {}\mrightarrow{}  \mBbbB{}.  Dec(P[t]))  {}\mRightarrow{}  Dec(\mforall{}t:\mBbbN{}B  {}\mrightarrow{}  \mBbbB{}.  P[t]))
\mvdash{}  \mexists{}n:\mBbbN{}.  \mforall{}m:\mBbbB{}.  (R  n  m)


By

---

Latex:
(Decide  \mkleeneopen{}\mexists{}f,g:\mBbbN{}B  {}\mrightarrow{}  \mBbbB{}.  (((h  f)  =  (h  g))  \mwedge{}  (\mneg{}f  (h  f)  =  g  (h  g)))\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index