---

Step * 2 1 1 1 1 1 1 of Lemma equipollent-nat-powered


1. n : ℤ
2. 0 < n
3. f : ℕ ⟶ (ℕ^n)
4. Bij(ℕ;(ℕ^n);f)
5. (n - 1) + 1 ~ n
6. ¬((n + 1) = 0 ∈ ℤ)
7. (n + 1) - 1 ~ n
8. g : (ℕ^n) ⟶ ℕ
9. ∀b:(ℕ^n). ((f (g b)) = b ∈ (ℕ^n))
10. ∀a:ℕ. ((g (f a)) = a ∈ ℕ)
11. x : ℕ
12. let a,b = coded-pair(x) in code-pair(a;b) = x ∈ ℤ
13. v1 : ℕ
14. v2 : ℕ
15. coded-pair(x) = <v1, v2> ∈ (ℕ × ℕ)
⊢ code-pair(v1;g (f v2)) = x ∈ ℕ
BY
{ ((Assert g (f v2) ~ v2 BY Auto) THEN HypSubst' (-1) 0) }

1
1. n : ℤ
2. 0 < n
3. f : ℕ ⟶ (ℕ^n)
4. Bij(ℕ;(ℕ^n);f)
5. (n - 1) + 1 ~ n
6. ¬((n + 1) = 0 ∈ ℤ)
7. (n + 1) - 1 ~ n
8. g : (ℕ^n) ⟶ ℕ
9. ∀b:(ℕ^n). ((f (g b)) = b ∈ (ℕ^n))
10. ∀a:ℕ. ((g (f a)) = a ∈ ℕ)
11. x : ℕ
12. let a,b = coded-pair(x) in code-pair(a;b) = x ∈ ℤ
13. v1 : ℕ
14. v2 : ℕ
15. coded-pair(x) = <v1, v2> ∈ (ℕ × ℕ)
16. g (f v2) ~ v2
⊢ code-pair(v1;v2) = x ∈ ℕ

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  f  :  \mBbbN{}  {}\mrightarrow{}  (\mBbbN{}\^{}n)
4.  Bij(\mBbbN{};(\mBbbN{}\^{}n);f)
5.  (n  -  1)  +  1  \msim{}  n
6.  \mneg{}((n  +  1)  =  0)
7.  (n  +  1)  -  1  \msim{}  n
8.  g  :  (\mBbbN{}\^{}n)  {}\mrightarrow{}  \mBbbN{}
9.  \mforall{}b:(\mBbbN{}\^{}n).  ((f  (g  b))  =  b)
10.  \mforall{}a:\mBbbN{}.  ((g  (f  a))  =  a)
11.  x  :  \mBbbN{}
12.  let  a,b  =  coded-pair(x)  in  code-pair(a;b)  =  x
13.  v1  :  \mBbbN{}
14.  v2  :  \mBbbN{}
15.  coded-pair(x)  =  <v1,  v2>
\mvdash{}  code-pair(v1;g  (f  v2))  =  x


By

---

Latex:
((Assert  g  (f  v2)  \msim{}  v2  BY  Auto)  THEN  HypSubst'  (-1)  0)

---

Home Index