Step * of Lemma not-d-CCC-nat

¬dCCC(ℕ)
BY
{ ((D 0 THENA Auto) THEN UnfoldTopAb (-1)) }

1
1. ∀R:ℕ ⟶ ℕ ⟶ 𝔹. ((∀g:ℕ ⟶ ℕ. ∃n:ℕ. (↑(R n (g n)))) ⇒ (∃n:ℕ. ∀m:ℕ. (↑(R n m))))
⊢ False


Latex:


Latex:
\mneg{}dCCC(\mBbbN{})


By


Latex:
((D  0  THENA  Auto)  THEN  UnfoldTopAb  (-1))




Home Index