---

Step * 1 1 1 of Lemma functions-list-0


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)
BY
{ (((D 5 With ⌜0⌝  THENA Auto) THEN Reduce -1) THEN (D -1 With ⌜1⌝  THENA Auto) THEN Reduce -1) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(((D  5  With  \mkleeneopen{}0\mkleeneclose{}    THENA  Auto)  THEN  Reduce  -1)  THEN  (D  -1  With  \mkleeneopen{}1\mkleeneclose{}    THENA  Auto)  THEN  Reduce  -1)

---

Home Index