---

Step * 1 of Lemma functions-list-0


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)
BY
{ ((D 2 THEN Auto) THEN EqCD THEN Auto) }

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

---

Latex:

---

Latex:

1.  b  :  \mBbbN{}
2.  v  :  (\mBbbN{}0  {}\mrightarrow{}  \mBbbN{}b)  List
3.  no\_repeats(\mBbbN{}0  {}\mrightarrow{}  \mBbbN{}b;v)
4.  functions-list(0;b)  =  v
5.  (\mlambda{}x.x  \mmember{}  v)
\mvdash{}  v  =  [\mlambda{}x.x]


By

---

Latex:
((D  2  THEN  Auto)  THEN  EqCD  THEN  Auto)

---

Home Index