---

Step * 1 of Lemma posint_unit_dec


1. a : |<ℤ+,*>|@i
⊢ Dec(a = 1 ∈ ℤ)
BY
{ Auto }

---

Latex:

---

Latex:

1.  a  :  |<\mBbbZ{}\msupplus{},*>|@i
\mvdash{}  Dec(a  =  1)


By

---

Latex:
Auto

---

Home Index