---

Step * of Lemma qmax-imax

∀[x,y:ℤ].  (qmax(x;y) ~ imax(x;y))
BY
{ xxx(Auto
      THEN RepUR  ``qmax imax q_le`` 0
      THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
      THEN (RWO "qsub-sub" 0 THENA Auto)
      THEN AutoSplit
      THEN RWO "qless-int" (-1)
      THEN Auto
      THEN AutoBoolCase ⌜x ≤z y⌝⋅
      THEN Auto'
      THEN AutoSplit
      THEN All (RWO "qle-int" )
      THEN Auto')xxx }

1
1. x : ℤ
2. y : ℤ
3. ¬(x ≤ y)
4. ¬0 < y - x
5. x = y ∈ ℚ
⊢ y = x ∈ ℤ

---

Latex:

---

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


By

---

Latex:
xxx(Auto
        THEN  RepUR    ``qmax  imax  q\_le``  0
        THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
        THEN  (RWO  "qsub-sub"  0  THENA  Auto)
        THEN  AutoSplit
        THEN  RWO  "qless-int"  (-1)
        THEN  Auto
        THEN  AutoBoolCase  \mkleeneopen{}x  \mleq{}z  y\mkleeneclose{}\mcdot{}
        THEN  Auto'
        THEN  AutoSplit
        THEN  All  (RWO  "qle-int"  )
        THEN  Auto')xxx

---

Home Index