---

Step * of Lemma functions-list-0

∀[b:ℕ]. (functions-list(0;b) = [λx.x] ∈ ((ℕ0 ⟶ ℕb) List))
BY
{ (Auto
   THEN (GenConclTerm ⌜functions-list(0;b)⌝⋅ THENA Auto)
   THEN RepeatFor 2 (D -2)
   THEN (D -2 With ⌜λx.x⌝  THENA Auto)) }

1
1. b : ℕ
2. v : (ℕ0 ⟶ ℕb) List
3. no_repeats(ℕ0 ⟶ ℕb;v)
4. functions-list(0;b) = v ∈ {P:(ℕ0 ⟶ ℕb) List| no_repeats(ℕ0 ⟶ ℕb;P) ∧ (∀f:ℕ0 ⟶ ℕb. (f ∈ P))} 
5. (λx.x ∈ v)
⊢ v = [λx.x] ∈ ((ℕ0 ⟶ ℕb) List)

---

Latex:

---

Latex:
\mforall{}[b:\mBbbN{}].  (functions-list(0;b)  =  [\mlambda{}x.x])


By

---

Latex:
(Auto
  THEN  (GenConclTerm  \mkleeneopen{}functions-list(0;b)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  -2)
  THEN  (D  -2  With  \mkleeneopen{}\mlambda{}x.x\mkleeneclose{}    THENA  Auto))

---

Home Index