---

Step * of Lemma imax-imin-absorption

∀[x,y:ℤ].  (imax(x;imin(x;y)) = x ∈ ℤ)
BY
{ (Auto
   THEN RepUR ``imax imin`` 0
   THEN (CallByValueReduceOn ⌜x⌝ 0⋅ THENA Auto)
   THEN (CallByValueReduceOn ⌜y⌝ 0⋅ THENA Auto)
   THEN AutoSplit
   THEN (CallByValueReduceOn ⌜x⌝ 0⋅ THENA Auto)
   THEN (CallByValueReduceOn ⌜y⌝ 0⋅ THENA Auto)
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbZ{}].    (imax(x;imin(x;y))  =  x)


By

---

Latex:
(Auto
  THEN  RepUR  ``imax  imin``  0
  THEN  (CallByValueReduceOn  \mkleeneopen{}x\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduceOn  \mkleeneopen{}y\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  AutoSplit
  THEN  (CallByValueReduceOn  \mkleeneopen{}x\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduceOn  \mkleeneopen{}y\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  AutoSplit)

---

Home Index