---

Step * of Lemma imin-imax-distributive

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

---

Latex:

---

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


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  (CallByValueReduceOn  \mkleeneopen{}z\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (AutoSplit)
  THEN  (CallByValueReduceOn  \mkleeneopen{}x\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduceOn  \mkleeneopen{}y\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduceOn  \mkleeneopen{}z\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  AutoSplit
  THEN  Try  (AutoSplit)
  THEN  Try  (((CallByValueReduceOn  \mkleeneopen{}x\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                        THEN  (CallByValueReduceOn  \mkleeneopen{}y\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                        THEN  (CallByValueReduceOn  \mkleeneopen{}z\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                        THEN  AutoSplit)))

---

Home Index