---

Step * of Lemma imax-imin-distributive

∀[x,y,z:ℤ].  (imax(imin(x;y);imin(x;z)) = imin(x;imax(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{}].    (imax(imin(x;y);imin(x;z))  =  imin(x;imax(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