---

Step * of Lemma code-seq-bijection

Bij(ℕ;k:ℕ × (ℕk ⟶ ℕ);λx.coded-seq(x))
BY
{ TACTIC:(RepeatFor 2 ((D 0 THEN Auto)) THEN All Reduce) }

1
1. a1 : ℕ@i
2. a2 : ℕ@i
3. coded-seq(a1) = coded-seq(a2) ∈ (k:ℕ × (ℕk ⟶ ℕ))
⊢ a1 = a2 ∈ ℕ

2
1. b : k:ℕ × (ℕk ⟶ ℕ)@i
⊢ ∃a:ℕ. (coded-seq(a) = b ∈ (k:ℕ × (ℕk ⟶ ℕ)))

---

Latex:

---

Latex:
Bij(\mBbbN{};k:\mBbbN{}  \mtimes{}  (\mBbbN{}k  {}\mrightarrow{}  \mBbbN{});\mlambda{}x.coded-seq(x))


By

---

Latex:
TACTIC:(RepeatFor  2  ((D  0  THEN  Auto))  THEN  All  Reduce)

---

Home Index