normalize

(defun distribute-*
  (x y)
  (declare (xargs :guard (and (acl2-numberp x) (acl2-numberp y))))
  (* x y))

(defun factors
  (product)
  (declare (xargs :guard (pseudo-termp product)))
  (if (eq (fn-symb product) 'binary-*)
    (cons (fargn product 1) (factors (fargn product 2)))
    (list product)))

(defun factors-other-than-denominator
  (addend denominator)
  (declare (xargs :guard (and (pseudo-termp addend) (pseudo-termp denominator))))
  (if (eq (fn-symb addend) 'binary-*)
    (if (and (eq (fn-symb (fargn addend 1)) 'unary-/)
        (equal (fargn (fargn addend 1) 1) denominator))
      (factors-other-than-denominator (fargn addend 2)
        denominator)
      (cons (fargn addend 1)
        (factors-other-than-denominator (fargn addend 2)
          denominator)))
    (if (and (eq (fn-symb addend) 'unary-/)
        (equal (fargn addend 1) denominator))
      nil
      (list addend))))

(defun make-product
  (factors)
  (declare (xargs :guard (true-listp factors)))
  (cond ((null factors) ''1)
    ((null (cdr factors)) (car factors))
    ((null (cddr factors)) (list 'binary-* (car factors) (cadr factors)))
    (t (list 'binary-* (car factors) (make-product (cdr factors))))))

(defun number-of-addends
  (sum)
  (declare (xargs :guard (pseudo-termp sum)))
  (if (eq (fn-symb sum) 'binary-+)
    (+ 1 (number-of-addends (fargn sum 2)))
    1))

(defun find-denominators-with-sums
  (addend denominator-list number-of-addends-in-sum)
  (declare (xargs :guard (and (pseudo-termp addend)
        (integerp number-of-addends-in-sum))))
  (cond ((or (variablep addend) (fquotep addend)) denominator-list)
    ((eq (fn-symb addend) 'binary-*) (if (and (eq (fn-symb (fargn addend 1)) 'unary-/)
          (eq (fn-symb (fargn (fargn addend 1) 1)) 'binary-+)
          (consp (cdr (fargn (fargn addend 1) 1)))
          (<= (number-of-addends (fargn (fargn addend 1) 1))
            number-of-addends-in-sum))
        (find-denominators-with-sums (fargn addend 2)
          (cons (fargn (fargn addend 1) 1) denominator-list)
          number-of-addends-in-sum)
        (find-denominators-with-sums (fargn addend 2)
          denominator-list
          number-of-addends-in-sum)))
    ((and (eq (fn-symb addend) 'unary-/)
       (eq (fn-symb (fargn addend 1)) 'binary-+)
       (consp (cdr (fargn addend 1)))
       (<= (number-of-addends (fargn addend 1))
         number-of-addends-in-sum)) (cons (fargn addend 1) denominator-list))
    (t denominator-list)))

(defun to-be-found
  (denominator saved-denominator factors to-be-found)
  (declare (xargs :guard (and (pseudo-termp denominator)
        (true-listp factors)
        (true-listp to-be-found))))
  (if (eq (fn-symb denominator) 'binary-+)
    (let ((factors-2 (factors (fargn denominator 1))))
      (if (intersectp-equal factors factors-2)
        nil
        (to-be-found (fargn denominator 2)
          saved-denominator
          factors
          (cons (cons saved-denominator (append factors-2 factors))
            to-be-found))))
    (let ((factors-2 (factors denominator)))
      (if (intersectp-equal factors factors-2)
        nil
        (reverse (cons (cons saved-denominator (append factors-2 factors))
            to-be-found))))))

(defun set-equal
  (a b)
  (declare (xargs :guard (and (true-listp a) (true-listp b))))
  (and (subsetp-equal a b) (subsetp-equal b a)))

(defun remainder-aaa
  (to-be-found rest remainder)
  (declare (xargs :guard (and (true-list-listp to-be-found)
        (pseudo-termp rest)
        (pseudo-termp remainder))))
  (cond ((endp to-be-found) remainder)
    ((null rest) nil)
    ((eq (fn-symb rest) 'binary-+) (if (set-equal (factors (fargn rest 1)) (car to-be-found))
        (remainder-aaa (cdr to-be-found) (fargn rest 2) remainder)
        (remainder-aaa to-be-found
          (fargn rest 2)
          (if (null remainder)
            (fargn rest 1)
            (list 'binary-+ (fargn rest 1) remainder)))))
    ((null (cdr to-be-found)) (if (set-equal (factors rest) (car to-be-found))
        (if remainder
          remainder
          ''0)
        nil))
    (t nil)))

(defun denominatorp
  (denominator)
  (declare (xargs :guard t))
  (and (pseudo-termp denominator)
    (not (variablep denominator))
    (not (equal (car denominator) 'quote))
    (consp (cdr denominator))))

(defun normalize-terms-such-as-a/a+b-+-b/a+b-fn-2
  (denominator addend rest)
  (declare (xargs :guard (and (denominatorp denominator)
        (pseudo-termp addend)
        (pseudo-termp rest))))
  (let ((factors1 (factors-other-than-denominator addend denominator)) (factors2 (factors (fargn denominator 1))))
    (if (intersectp-equal factors1 factors2)
      (let* ((factors (set-difference-equal factors1 factors2)) (to-be-found (to-be-found (fargn denominator 2)
              (list 'unary-/ denominator)
              factors
              nil))
          (remainder (remainder-aaa to-be-found rest nil)))
        (if remainder
          (list (cons 'factor (make-product factors))
            (cons 'denominator denominator)
            (cons 'remainder remainder)
            (cons 'a (fargn denominator 1)))
          nil))
      nil)))

(defun denominator-list-p
  (denominator-list)
  (declare (xargs :guard t))
  (if (atom denominator-list)
    (equal denominator-list nil)
    (and (denominatorp (car denominator-list))
      (denominator-list-p (cdr denominator-list)))))

(defun normalize-terms-such-as-a/a+b-+-b/a+b-fn-1
  (denominator-list addend rest)
  (declare (xargs :guard (and (denominator-list-p denominator-list)
        (pseudo-termp addend)
        (pseudo-termp rest))))
  (if (endp denominator-list)
    nil
    (let ((binding-alist (normalize-terms-such-as-a/a+b-+-b/a+b-fn-2 (car denominator-list)
           addend
           rest)))
      (if binding-alist
        binding-alist
        (normalize-terms-such-as-a/a+b-+-b/a+b-fn-1 (cdr denominator-list)
          addend
          rest)))))

(defun normalize-terms-such-as-a/a+b-+-b/a+b-fn
  (x y)
  (declare (xargs :guard (and (pseudo-termp x) (pseudo-termp y))))
  (if (eq (fn-symb x) 'binary-*)
    (normalize-terms-such-as-a/a+b-+-b/a+b-fn-1 (find-denominators-with-sums x
        nil
        (+ 1 (number-of-addends y)))
      x
      y)
    nil))

(defun remainder-bbb
  (common-factors sum)
  (declare (xargs :guard (and (true-listp common-factors) (pseudo-termp sum))))
  (if (eq (fn-symb sum) 'binary-+)
    (let ((first (make-product (set-difference-equal (factors (fargn sum 1))
             common-factors))))
      (list 'binary-+
        first
        (remainder-bbb common-factors (fargn sum 2))))
    (make-product (set-difference-equal (factors sum) common-factors))))

(defun common-factors
  (factors sum)
  (declare (xargs :measure (acl2-count sum)
      :guard (and (pseudo-term-listp factors) (pseudo-termp sum))))
  (cond ((null factors) nil)
    ((eq (fn-symb sum) 'binary-+) (common-factors (intersection-equal factors (factors (fargn sum 1)))
        (fargn sum 2)))
    (t (intersection-equal factors (factors sum)))))

(defun normalize-terms-such-as-1/ax+bx-fn
  (sum)
  (declare (xargs :guard (pseudo-termp sum)))
  (if (and (eq (fn-symb sum) 'binary-+)
      (eq (fn-symb (fargn sum 1)) 'binary-*))
    (let ((common-factors (common-factors (factors (fargn sum 1)) (fargn sum 2))))
      (if common-factors
        (let ((common (make-product common-factors)) (remainder (remainder-bbb common-factors sum)))
          (list (cons 'common common) (cons 'remainder remainder)))
        nil))
    nil))

(defun find-matching-addend
  (to-match x)
  (declare (xargs :guard (pseudo-termp x)))
  (cond ((eq (fn-symb x) 'binary-+) (cond ((matching-addend-p to-match (arg1 x)) (list (cons 'match (arg1 x))))
        ((eq (fn-symb (arg2 x)) 'binary-+) (find-matching-addend to-match (arg2 x)))
        ((matching-addend-p to-match (arg2 x)) (list (cons 'match (arg2 x))))
        (t nil)))
    ((matching-addend-p to-match x) (list (cons 'match x)))
    (t nil)))

(defun find-matching-factor-gather-exponents
  (to-match x)
  (declare (xargs :guard (and (true-listp to-match) (pseudo-termp x))))
  (cond ((eq (fn-symb x) 'binary-*) (cond ((matching-factor-gather-exponents-p to-match (arg1 x)) (list (cons 'match (arg1 x))))
        ((eq (fn-symb (arg2 x)) 'binary-*) (find-matching-factor-gather-exponents to-match (arg2 x)))
        ((matching-factor-gather-exponents-p to-match (arg2 x)) (list (cons 'match (arg2 x))))
        (t nil)))
    ((matching-factor-gather-exponents-p to-match x) (list (cons 'match x)))
    (t nil)))

(defun find-matching-factor-scatter-exponents
  (to-match x)
  (declare (xargs :guard (and (true-listp to-match) (pseudo-termp x))))
  (cond ((eq (fn-symb x) 'binary-*) (cond ((matching-factor-scatter-exponents-p to-match (arg1 x)) (list (cons 'match (arg1 x))))
        ((eq (fn-symb (arg2 x)) 'binary-*) (find-matching-factor-scatter-exponents to-match (arg2 x)))
        ((matching-factor-scatter-exponents-p to-match (arg2 x)) (list (cons 'match (arg2 x))))
        (t nil)))
    ((matching-factor-scatter-exponents-p to-match x) (list (cons 'match x)))
    (t nil)))