---

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


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)
BY
{ ((Assert ¬(u = u1 ∈ (ℕ0 ⟶ ℕb)) BY (BHyp -1  THEN Auto)) THEN D -1 THEN Auto) }

---

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.  functions-list(0;b)  =  [u;  [u1  /  v]]
6.  (\mlambda{}x.x  \mmember{}  [u;  [u1  /  v]])
7.  (\mneg{}(u  =  u1))  supposing  ((\mneg{}(0  =  1))  and  1  <  (||v||  +  1)  +  1  and  0  <  (||v||  +  1)  +  1)
\mvdash{}  [u1  /  v]  =  []


By

---

Latex:
((Assert  \mneg{}(u  =  u1)  BY  (BHyp  -1    THEN  Auto))  THEN  D  -1  THEN  Auto)

---

Home Index