---

Step * 1 of Lemma int_mag_well_founded


1. WellFnd{i}(ℤ;x,y.(λx.|x|) x < (λx.|x|) y)
⊢ WellFnd{i}(ℤ;x,y.|x| < |y|)
BY
{ (Reduce 1 THEN Auto) }

---

Latex:

---

Latex:

1.  WellFnd\{i\}(\mBbbZ{};x,y.(\mlambda{}x.|x|)  x  <  (\mlambda{}x.|x|)  y)
\mvdash{}  WellFnd\{i\}(\mBbbZ{};x,y.|x|  <  |y|)


By

---

Latex:
(Reduce  1  THEN  Auto)

---

Home Index