---

Step * of Lemma posint_well_fnd

WellFnd{i}(|<ℤ+,*>|;x,y.x p| y)
BY
{ RepUnfolds ``mdivides mpdivides`` 0 
THEN AbReduce 0 }

1
WellFnd{i}(ℕ+;x,y.(∃c:ℕ+. (y = (x * c) ∈ ℕ+)) ∧ (¬(∃c:ℕ+. (x = (y * c) ∈ ℕ+))))

---

Latex:

---

Latex:
WellFnd\{i\}(|<\mBbbZ{}\msupplus{},*>|;x,y.x  p|  y)


By

---

Latex:
RepUnfolds  ``mdivides  mpdivides``  0 
THEN  AbReduce  0

---

Home Index