---

Step * 1 1 of Lemma functions-list-0

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

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

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  b  :  \mBbbN{}
2.  u  :  \mBbbN{}0  {}\mrightarrow{}  \mBbbN{}b
3.  v  :  (\mBbbN{}0  {}\mrightarrow{}  \mBbbN{}b)  List
4.  no\_repeats(\mBbbN{}0  {}\mrightarrow{}  \mBbbN{}b;[u  /  v])
5.  functions-list(0;b)  =  [u  /  v]
6.  (\mlambda{}x.x  \mmember{}  [u  /  v])
\mvdash{}  v  =  []


By

---

Latex:
(D  3  THEN  Auto)

---

Home Index