Step
*
of Lemma
list-functions
∀n,b:ℕ. (∃P:(ℕn ⟶ ℕb) List [(no_repeats(ℕn ⟶ ℕb;P) ∧ (∀f:ℕn ⟶ ℕb. (f ∈ P)))])
BY
{ (InstLemma `equipollent-exp` []⋅
THEN RepeatFor 2 (ParallelLast')
THEN (FLemma `equipollent-iff-list` [-1] THENA Auto)
THEN ParallelLast
THEN Auto) }
Latex:
Latex:
\mforall{}n,b:\mBbbN{}. (\mexists{}P:(\mBbbN{}n {}\mrightarrow{} \mBbbN{}b) List [(no\_repeats(\mBbbN{}n {}\mrightarrow{} \mBbbN{}b;P) \mwedge{} (\mforall{}f:\mBbbN{}n {}\mrightarrow{} \mBbbN{}b. (f \mmember{} P)))])
By
Latex:
(InstLemma `equipollent-exp` []\mcdot{}
THEN RepeatFor 2 (ParallelLast')
THEN (FLemma `equipollent-iff-list` [-1] THENA Auto)
THEN ParallelLast
THEN Auto)
Home
Index