		Search-engine friendly clone of the ACL2 documentation.

Basic-rational-identities

Basic cancellation rules for numerator and denominator terms.

See also more-rational-identities for additional reductions involving numerator and denominator terms.

Definitions and Theorems

Theorem: numerator-when-integerp

(defthm numerator-when-integerp
  (implies (integerp x)
           (equal (numerator x) x)))

Theorem: integerp==>denominator=1

(defthm integerp==>denominator=1
  (implies (integerp x)
           (equal (denominator x) 1)))

Theorem: equal-denominator-1

(defthm equal-denominator-1
  (equal (equal (denominator x) 1)
         (or (integerp x) (not (rationalp x)))))

Theorem: *-r-denominator-r

(defthm *-r-denominator-r
  (equal (* r (denominator r))
         (if (rationalp r)
             (numerator r)
           (fix r))))

Theorem: /r-when-abs-numerator=1

(defthm /r-when-abs-numerator=1
  (and (implies (equal (numerator r) 1)
                (equal (/ r) (denominator r)))
       (implies (equal (numerator r) -1)
                (equal (/ r) (- (denominator r))))))