---

Step * of Lemma qabs-as-qmax

∀[q:ℚ]. (|q| = qmax(q;-(q)) ∈ ℚ)
BY
{ (Auto
   THEN xxx((Unfolds ``qabs qmax`` 0 THEN (CallByValueReduce 0 THENA Auto))
            THEN (SplitOnConclITE THENA Auto)
            THEN Try (((RWO "qless_complement_qorder" (-1)) THENA Auto))
            THEN (SplitOnConclITE THENA Auto)
            THEN Try (((RWO "qle_complement_qorder" (-1)) THENA Auto))
            THEN Auto
            THEN QAdd ⌜q⌝ (-1)⋅
            THEN QMul ⌜(1/2)⌝ (-1)⋅
            THEN RelRST
            THEN Auto)xxx
   ) }

---

Latex:

---

Latex:
\mforall{}[q:\mBbbQ{}].  (|q|  =  qmax(q;-(q)))


By

---

Latex:
(Auto
  THEN  xxx((Unfolds  ``qabs  qmax``  0  THEN  (CallByValueReduce  0  THENA  Auto))
                    THEN  (SplitOnConclITE  THENA  Auto)
                    THEN  Try  (((RWO  "qless\_complement\_qorder"  (-1))  THENA  Auto))
                    THEN  (SplitOnConclITE  THENA  Auto)
                    THEN  Try  (((RWO  "qle\_complement\_qorder"  (-1))  THENA  Auto))
                    THEN  Auto
                    THEN  QAdd  \mkleeneopen{}q\mkleeneclose{}  (-1)\mcdot{}
                    THEN  QMul  \mkleeneopen{}(1/2)\mkleeneclose{}  (-1)\mcdot{}
                    THEN  RelRST
                    THEN  Auto)xxx
  )

---

Home Index