Step * of Lemma posint_well_fnd

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

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