---

Step * 3 1 of Lemma equipollent-multiply


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)
BY
{ ((D (-3) THEN D -2 THEN All Reduce) THEN Assert ⌜a3 = a5 ∈ ℤ⌝⋅) }

1
.....assertion..... 
1. a : ℕ
2. b : ℕ
3. a3 : ℕa
4. a4 : ℕb
5. a5 : ℕa
6. a6 : ℕb
7. ((a3 * b) + a4) = ((a5 * b) + a6) ∈ ℕa * b
⊢ a3 = a5 ∈ ℤ

2
1. a : ℕ
2. b : ℕ
3. a3 : ℕa
4. a4 : ℕb
5. a5 : ℕa
6. a6 : ℕb
7. ((a3 * b) + a4) = ((a5 * b) + a6) ∈ ℕa * b
8. a3 = a5 ∈ ℤ
⊢ <a3, a4> = <a5, a6> ∈ (ℕa × ℕb)

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}
2.  b  :  \mBbbN{}
3.  a1  :  \mBbbN{}a  \mtimes{}  \mBbbN{}b
4.  a2  :  \mBbbN{}a  \mtimes{}  \mBbbN{}b
5.  let  x,y  =  a1  in  (x  *  b)  +  y  =  let  x,y  =  a2  in  (x  *  b)  +  y
\mvdash{}  a1  =  a2


By

---

Latex:
((D  (-3)  THEN  D  -2  THEN  All  Reduce)  THEN  Assert  \mkleeneopen{}a3  =  a5\mkleeneclose{}\mcdot{})

---

Home Index