---

Step * of Lemma qabs-abs

∀[x:ℤ]. (|x| ~ |x|)
BY
{ xxx(Auto
      THEN xxx(RepUR ``qabs qpositive qmul absval`` 0
               THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
               THEN (Reduce 0 THENA Auto)
               THEN RepeatFor 2 (AutoSplit)
               THEN Auto')xxx
      )xxx }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  (|x|  \msim{}  |x|)


By

---

Latex:
xxx(Auto
        THEN  xxx(RepUR  ``qabs  qpositive  qmul  absval``  0
                          THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
                          THEN  (Reduce  0  THENA  Auto)
                          THEN  RepeatFor  2  (AutoSplit)
                          THEN  Auto')xxx
        )xxx

---

Home Index