---

Step * of Lemma test-recursion-extract

∀k:ℕ. ∀f:ℕ ⟶ ℚ.  ((∃n:ℕk. ((f n) = 0 ∈ ℚ)) ∨ True)
BY
{ (GeneralInductionOnNat⋅ THENA Auto) }

1
1. k : ℕ
2. ∀k1:ℕk. ∀f:ℕ ⟶ ℚ.  ((∃n:ℕk1. ((f n) = 0 ∈ ℚ)) ∨ True)
⊢ ∀f:ℕ ⟶ ℚ. ((∃n:ℕk. ((f n) = 0 ∈ ℚ)) ∨ True)

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}.    ((\mexists{}n:\mBbbN{}k.  ((f  n)  =  0))  \mvee{}  True)


By

---

Latex:
(GeneralInductionOnNat\mcdot{}  THENA  Auto)

---

Home Index