---

Step * 3 of Lemma equipollent-multiply


1. a : ℕ
2. b : ℕ
⊢ Bij(ℕa × ℕb;ℕa * b;λp.let x,y = p 
                        in (x * b) + y)
BY
{ (RepeatFor 2 (D 0) THEN Reduce 0 THEN Auto') }

1
1. a : ℕ
2. b : ℕ
3. a1 : ℕa × ℕb
4. a2 : ℕa × ℕb
5. let x,y = a1 in (x * b) + y = let x,y = a2 in (x * b) + y ∈ ℕa * b
⊢ a1 = a2 ∈ (ℕa × ℕb)

2
1. a : ℕ
2. b : ℕ
3. b@0 : ℕa * b
⊢ ∃a@0:ℕa × ℕb. (let x,y = a@0 in (x * b) + y = b@0 ∈ ℕa * b)

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}
2.  b  :  \mBbbN{}
\mvdash{}  Bij(\mBbbN{}a  \mtimes{}  \mBbbN{}b;\mBbbN{}a  *  b;\mlambda{}p.let  x,y  =  p 
                                                in  (x  *  b)  +  y)


By

---

Latex:
(RepeatFor  2  (D  0)  THEN  Reduce  0  THEN  Auto')

---

Home Index