normalize

(defun factors-other-than-denominator
  (addend denominator)
  (declare (xargs :guard t))
  (cond ((and (true-listp addend) (eq (ffn-symb addend) 'binary-*)) (if (and (and (true-listp (arg1 addend))
            (eq (ffn-symb (arg1 addend)) 'unary-/))
          (equal (arg1 (arg1 addend)) denominator))
        (factors (arg2 addend))
        (cons (arg1 addend)
          (factors-other-than-denominator (arg2 addend) denominator))))
    ((and (true-listp addend)
       (eq (ffn-symb addend) 'unary-/)
       (equal (arg1 addend) denominator)) nil)
    (t (list addend))))

(defun number-of-addends
  (sum)
  (declare (xargs :guard t))
  (if (and (true-listp sum) (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 (integerp number-of-addends-in-sum)))
  (cond ((or (variablep addend) (fquotep addend)) denominator-list)
    ((and (true-listp addend) (eq (ffn-symb addend) 'binary-*)) (if (and (true-listp (arg1 addend))
          (eq (fn-symb (arg1 addend)) 'unary-/)
          (true-listp (arg1 (arg1 addend)))
          (eq (fn-symb (arg1 (arg1 addend))) 'binary-+)
          (<= (number-of-addends (arg1 (arg1 addend)))
            number-of-addends-in-sum))
        (find-denominators-with-sums (arg2 addend)
          (cons (arg1 (arg1 addend)) denominator-list)
          number-of-addends-in-sum)
        (find-denominators-with-sums (arg2 addend)
          denominator-list
          number-of-addends-in-sum)))
    ((and (true-listp addend)
       (eq (fn-symb addend) 'unary-/)
       (true-listp (arg1 addend))
       (eq (fn-symb (arg1 addend)) 'binary-+)
       (<= (number-of-addends (arg1 addend))
         number-of-addends-in-sum)) (cons (arg1 addend) denominator-list))
    (t denominator-list)))

(defun remainder-aaa
  (sum factors to-be-found remainder)
  (declare (xargs :guard (true-listp factors)))
  (cond ((atom to-be-found) (cond ((and remainder sum) (list 'binary-+ remainder sum))
        (remainder remainder)
        (sum sum)
        (t ''0)))
    ((null sum) nil)
    ((and (true-listp sum) (eq (fn-symb sum) 'binary-+)) (if (set-equal (factors (arg1 sum))
          (cons (car to-be-found) factors))
        (remainder-aaa (arg2 sum)
          factors
          (cdr to-be-found)
          remainder)
        (remainder-aaa (arg2 sum)
          factors
          to-be-found
          (if (null remainder)
            (arg1 sum)
            (list 'binary-+ (arg1 sum) remainder)))))
    ((null (cdr to-be-found)) (if (set-equal (factors sum) (cons (car to-be-found) factors))
        (if remainder
          remainder
          ''0)
        nil))
    (t nil)))

(defun normalize-terms-such-as-a/a+b-+-b/a+b-fn-2
  (denominator addend rest)
  (declare (xargs :guard (true-listp denominator)))
  (let ((factors1 (factors-other-than-denominator addend denominator)) (factors2 (factors (arg1 denominator))))
    (cond ((equal factors2 '('1)) (let* ((factors factors1) (remainder (remainder-aaa rest
                (cons (list 'unary-/ denominator) factors)
                (addends (arg2 denominator))
                nil)))
          (if remainder
            (list (cons 'factor (make-product factors))
              (cons 'denominator denominator)
              (cons 'remainder remainder)
              (cons 'a (fargn denominator 1)))
            nil)))
      ((intersectp-equal factors1 factors2) (let* ((factors (set-difference-equal factors1 factors2)) (remainder (remainder-aaa rest
                (cons (list 'unary-/ denominator) factors)
                (addends (arg2 denominator))
                nil)))
          (if remainder
            (list (cons 'factor (make-product factors))
              (cons 'denominator denominator)
              (cons 'remainder remainder)
              (cons 'a (fargn denominator 1)))
            nil)))
      (t nil))))

(defun normalize-terms-such-as-a/a+b-+-b/a+b-fn-1
  (denominator-list addend rest)
  (declare (xargs :guard (and (true-list-listp denominator-list))))
  (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 t))
  (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))

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

(defun normalize-terms-such-as-1/ax+bx-fn
  (sum)
  (declare (xargs :guard t))
  (if (and (true-listp sum) (eq (ffn-symb sum) 'binary-+))
    (let ((common-factors (common-factors (factors (arg1 sum)) (arg2 sum))))
      (if common-factors
        (let ((common (make-product common-factors)) (remainder (remainder common-factors sum)))
          (list (cons 'common common) (cons 'remainder remainder)))
        nil))
    nil))

(defun find-matching-addend
  (to-match x mfc state)
  (declare (xargs :guard t))
  (cond ((and (true-listp x) (eq (fn-symb x) 'binary-+)) (cond ((and (matching-addend-p to-match (arg1 x))
           (stable-under-rewriting-sums (arg1 x) mfc state)) (list (cons 'match (arg1 x))))
        ((eq (fn-symb (arg2 x)) 'binary-+) (find-matching-addend to-match (arg2 x) mfc state))
        ((and (matching-addend-p to-match (arg2 x))
           (stable-under-rewriting-sums (arg2 x) mfc state)) (list (cons 'match (arg2 x))))
        (t nil)))
    ((and (matching-addend-p to-match x)
       (stable-under-rewriting-sums x mfc state)) (list (cons 'match x)))
    (t nil)))

(defun find-matching-factor-gather-exponents
  (to-match x mfc state)
  (declare (xargs :guard t))
  (cond ((eq (fn-symb x) 'binary-*) (cond ((and (matching-factor-gather-exponents-p to-match (arg1 x))
           (stable-under-rewriting-products (arg1 x) mfc state)) (list (cons 'match (arg1 x))))
        ((eq (fn-symb (arg2 x)) 'binary-*) (find-matching-factor-gather-exponents to-match
            (arg2 x)
            mfc
            state))
        ((and (matching-factor-gather-exponents-p to-match (arg2 x))
           (stable-under-rewriting-products (arg2 x) mfc state)) (list (cons 'match (arg2 x))))
        (t nil)))
    ((and (matching-factor-gather-exponents-p to-match x)
       (stable-under-rewriting-products x mfc state)) (list (cons 'match x)))
    (t nil)))

(defun find-matching-factor-scatter-exponents
  (to-match x mfc state)
  (declare (xargs :guard t))
  (cond ((eq (fn-symb x) 'binary-*) (cond ((and (matching-factor-scatter-exponents-p to-match (arg1 x))
           (stable-under-rewriting-sums (arg1 x) mfc state)) (list (cons 'match (arg1 x))))
        ((eq (fn-symb (arg2 x)) 'binary-*) (find-matching-factor-scatter-exponents to-match
            (arg2 x)
            mfc
            state))
        ((and (matching-factor-scatter-exponents-p to-match (arg2 x))
           (stable-under-rewriting-sums (arg2 x) mfc state)) (list (cons 'match (arg2 x))))
        (t nil)))
    ((and (matching-factor-scatter-exponents-p to-match x)
       (stable-under-rewriting-sums x mfc state)) (list (cons 'match x)))
    (t nil)))