---

Step * 2 1 1 1 1 1 of Lemma fun2listCantor


1. n : ℤ
2. 0 < n
3. ∀f:ℕn - 1 ⟶ 𝔹. ∃l:𝔹 List. ((||l|| = (n - 1) ∈ ℤ) ∧ (f = (λx.l[x]) ∈ (ℕn - 1 ⟶ 𝔹)))
4. f : ℕn ⟶ 𝔹
5. l : 𝔹 List
6. ||l|| = (n - 1) ∈ ℤ
7. f = (λx.l[x]) ∈ (ℕn - 1 ⟶ 𝔹)
8. x : ℕn
⊢ f x = l @ [f (n - 1)][x]
BY
{ TACTIC:(Decide ⌜x = (n - 1) ∈ ℤ⌝⋅ THENA Auto) }

1
1. n : ℤ
2. 0 < n
3. ∀f:ℕn - 1 ⟶ 𝔹. ∃l:𝔹 List. ((||l|| = (n - 1) ∈ ℤ) ∧ (f = (λx.l[x]) ∈ (ℕn - 1 ⟶ 𝔹)))
4. f : ℕn ⟶ 𝔹
5. l : 𝔹 List
6. ||l|| = (n - 1) ∈ ℤ
7. f = (λx.l[x]) ∈ (ℕn - 1 ⟶ 𝔹)
8. x : ℕn
9. x = (n - 1) ∈ ℤ
⊢ f x = l @ [f (n - 1)][x]

2
1. n : ℤ
2. 0 < n
3. ∀f:ℕn - 1 ⟶ 𝔹. ∃l:𝔹 List. ((||l|| = (n - 1) ∈ ℤ) ∧ (f = (λx.l[x]) ∈ (ℕn - 1 ⟶ 𝔹)))
4. f : ℕn ⟶ 𝔹
5. l : 𝔹 List
6. ||l|| = (n - 1) ∈ ℤ
7. f = (λx.l[x]) ∈ (ℕn - 1 ⟶ 𝔹)
8. x : ℕn
9. ¬(x = (n - 1) ∈ ℤ)
⊢ f x = l @ [f (n - 1)][x]

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}f:\mBbbN{}n  -  1  {}\mrightarrow{}  \mBbbB{}.  \mexists{}l:\mBbbB{}  List.  ((||l||  =  (n  -  1))  \mwedge{}  (f  =  (\mlambda{}x.l[x])))
4.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbB{}
5.  l  :  \mBbbB{}  List
6.  ||l||  =  (n  -  1)
7.  f  =  (\mlambda{}x.l[x])
8.  x  :  \mBbbN{}n
\mvdash{}  f  x  =  l  @  [f  (n  -  1)][x]


By

---

Latex:
TACTIC:(Decide  \mkleeneopen{}x  =  (n  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index