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