---

Step * 2 1 of Lemma fun2listCantor


1. n : ℤ
2. [%1] : 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 ⟶ 𝔹)
⊢ ∃l:𝔹 List. ((||l|| = n ∈ ℤ) ∧ (f = (λx.l[x]) ∈ (ℕn ⟶ 𝔹)))
BY
{ TACTIC:(InstConcl [⌜l @ [f (n - 1)]⌝]⋅ THENA Auto) }

1
1. n : ℤ
2. [%1] : 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 ⟶ 𝔹)
⊢ (||l @ [f (n - 1)]|| = n ∈ ℤ) ∧ (f = (λx.l @ [f (n - 1)][x]) ∈ (ℕn ⟶ 𝔹))

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  [\%1]  :  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])
\mvdash{}  \mexists{}l:\mBbbB{}  List.  ((||l||  =  n)  \mwedge{}  (f  =  (\mlambda{}x.l[x])))


By

---

Latex:
TACTIC:(InstConcl  [\mkleeneopen{}l  @  [f  (n  -  1)]\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index