inverted-factor

(defun find-inverted-factor
  (term)
  (declare (xargs :guard (pseudo-termp term)))
  (if (not (consp term))
    nil
    (case (car term)
      '(if (integerp (cadr term))
        nil
        (if (rationalp (cadr term))
          `((k quote ,(DENOMINATOR (CADR TERM))))
          nil))
      (binary-+ (or (find-inverted-factor (cadr term))
          (find-inverted-factor (caddr term))))
      (binary-* (or (find-inverted-factor (cadr term))
          (find-inverted-factor (caddr term))))
      (unary-/ (list (cons 'k (cadr term))))
      (otherwise nil))))

(defun is-a-factor
  (factor term)
  (declare (xargs :guard (pseudo-termp term)))
  (if (not (consp term))
    (equal factor term)
    (case (car term)
      (binary-* (if (equal factor (cadr term))
          t
          (is-a-factor factor (caddr term))))
      (otherwise (equal factor term)))))

(defun factor-syntaxp
  (term can-be-a-constant)
  (declare (xargs :guard (pseudo-termp term)))
  (if (not (consp term))
    t
    (case (car term)
      (binary-* nil)
      (binary-+ nil)
      (unary-/ (and (consp (cdr term)) (factor-syntaxp (cadr term) nil)))
      'can-be-a-constant
      (otherwise t))))

(defun product-syntaxp
  (term first-factor-can-be-a-constant)
  (declare (xargs :guard (pseudo-termp term)))
  (if (not (consp term))
    t
    (case (car term)
      (binary-* (and (factor-syntaxp (cadr term) first-factor-can-be-a-constant)
          (product-syntaxp (caddr term) nil)))
      (otherwise (factor-syntaxp term first-factor-can-be-a-constant)))))

(defun sum-of-products-syntaxp
  (term)
  (declare (xargs :guard (pseudo-termp term)))
  (if (not (consp term))
    t
    (case (car term)
      (binary-+ (and (product-syntaxp (cadr term) t)
          (sum-of-products-syntaxp (caddr term))))
      (otherwise (product-syntaxp term t)))))