linear-a

(defun pt-occur
  (n pt)
  (cond ((null pt) nil)
    ((consp pt) (or (pt-occur n (car pt)) (pt-occur n (cdr pt))))
    (t (= n pt))))

(defun pt-intersectp
  (pt1 pt2)
  (cond ((null pt1) nil)
    ((consp pt1) (or (pt-intersectp (car pt1) pt2)
        (pt-intersectp (cdr pt1) pt2)))
    (t (pt-occur pt1 pt2))))

(defun tag-tree-occur
  (tag val ttree)
  (let ((pair (assoc-eq tag ttree)))
    (and pair (member-equal val (cdr pair)))))

(defun remove-tag-from-tag-tree
  (tag ttree)
  (cond ((assoc-eq tag ttree) (remove1-assoc-eq tag ttree))
    (t ttree)))

(defun remove-tag-from-tag-tree!
  (tag ttree)
  (remove1-assoc-eq tag ttree))

(defun add-to-tag-tree
  (tag val ttree)
  (cond ((eq ttree nil) (list (list tag val)))
    (t (let ((pair (assoc-eq tag ttree)))
        (cond (pair (cond ((member-equal val (cdr pair)) ttree)
              (t (acons tag
                  (cons val (cdr pair))
                  (remove-tag-from-tag-tree! tag ttree)))))
          (t (acons tag (list val) ttree)))))))

(defun add-to-tag-tree!
  (tag val ttree)
  (extend-tag-tree tag (list val) ttree))

(defun remove1-assoc-eq-assoc-eq-1
  (alist1 alist2)
  (declare (xargs :guard (and (symbol-alistp alist1) (symbol-alistp alist2))))
  (cond ((endp alist2) (mv nil nil))
    (t (mv-let (changedp x)
        (remove1-assoc-eq-assoc-eq-1 alist1 (cdr alist2))
        (cond ((assoc-eq (caar alist2) alist1) (mv t x))
          (changedp (mv t (cons (car alist2) x)))
          (t (mv nil alist2)))))))

(defun remove1-assoc-eq-assoc-eq
  (alist1 alist2)
  (mv-let (changedp x)
    (remove1-assoc-eq-assoc-eq-1 alist1 alist2)
    (declare (ignore changedp))
    x))

(defun cons-tag-trees1
  (ttree1 ttree2 ttree3)
  (cond ((endp ttree1) ttree3)
    (t (let ((pair (assoc-eq (caar ttree1) ttree2)))
        (cond (pair (acons (caar ttree1)
              (union-equal (cdar ttree1) (cdr pair))
              (cons-tag-trees1 (cdr ttree1) ttree2 ttree3)))
          (t (cons (car ttree1)
              (cons-tag-trees1 (cdr ttree1) ttree2 ttree3))))))))

(defun cons-tag-trees
  (ttree1 ttree2)
  (cond ((null ttree1) ttree2)
    ((null ttree2) ttree1)
    ((null (cdr ttree2)) (let* ((pair2 (car ttree2)) (tag (car pair2))
          (pair1 (assoc-eq tag ttree1)))
        (cond (pair1 (acons tag
              (union-equal (cdr pair1) (cdr pair2))
              (remove1-assoc-eq tag ttree1)))
          (t (cons pair2 ttree1)))))
    (t (let ((ttree3 (remove1-assoc-eq-assoc-eq ttree1 ttree2)))
        (cons-tag-trees1 ttree1 ttree2 ttree3)))))

(defun tagged-object
  (tag ttree)
  (let ((objects (tagged-objects tag ttree)))
    (and objects (assert$ (null (cdr objects)) (car objects)))))

(defun pts-to-ttree-lst
  (pts)
  (cond ((null pts) nil)
    (t (cons (add-to-tag-tree! 'pt (car pts) nil)
        (pts-to-ttree-lst (cdr pts))))))

(defun marry-parents
  (parents1 parents2)
  (if (null parents1)
    parents2
    (marry-parents (cdr parents1)
      (add-to-set-eql (car parents1) parents2))))

(defun collect-parents1
  (pt ans)
  (cond ((null pt) ans)
    ((consp pt) (collect-parents1 (car pt) (collect-parents1 (cdr pt) ans)))
    (t (add-to-set-eql pt ans))))

(defun collect-parents0
  (pts ans)
  (cond ((null pts) ans)
    (t (collect-parents0 (cdr pts)
        (collect-parents1 (car pts) ans)))))

(defun collect-parents
  (ttree)
  (collect-parents0 (tagged-objects 'pt ttree) nil))

(defun ignore-polyp
  (parents pt)
  (if (null parents)
    nil
    (or (pt-occur (car parents) pt)
      (ignore-polyp (cdr parents) pt))))

(defun to-be-ignoredp1
  (pts pt)
  (cond ((endp pts) nil)
    (t (or (pt-intersectp (car pts) pt)
        (to-be-ignoredp1 (cdr pts) pt)))))

(defun to-be-ignoredp
  (ttree pt)
  (to-be-ignoredp1 (tagged-objects 'pt ttree) pt))

(defun remove-assumption-entries-from-type-alist
  (type-alist)
  (cond ((endp type-alist) nil)
    ((contains-assumptionp (cddar type-alist)) (remove-assumption-entries-from-type-alist (cdr type-alist)))
    (t (cons-with-hint (car type-alist)
        (remove-assumption-entries-from-type-alist (cdr type-alist))
        type-alist))))

(defun force-assumption1
  (rune target term type-alist rewrittenp immediatep ttree)
  (let* ((term (cond ((equal term *nil*) (er hard 'force-assumption "Attempt to force nil!"))
         ((null rune) (er hard 'force-assumption "Attempt to force the nil rune!"))
         (t term))))
    (cond ((not (member-eq immediatep '(t nil case-split))) (er hard
          'force-assumption1
          "The :immediatep of an ASSUMPTION record must be ~
                t, nil, or 'case-split, but we have tried to create ~
                one with ~x0."
          immediatep))
      (t (add-to-tag-tree 'assumption
          (make assumption
            :type-alist type-alist
            :term term
            :rewrittenp rewrittenp
            :immediatep immediatep
            :assumnotes (list (make assumnote :cl-id nil :rune rune :target target)))
          ttree)))))

(defun dumb-occur-in-type-alist
  (var type-alist)
  (cond ((null type-alist) nil)
    ((dumb-occur var (caar type-alist)) t)
    (t (dumb-occur-in-type-alist var (cdr type-alist)))))

(defun all-dumb-occur-in-type-alist
  (vars type-alist)
  (cond ((null vars) t)
    (t (and (dumb-occur-in-type-alist (car vars) type-alist)
        (all-dumb-occur-in-type-alist (cdr vars) type-alist)))))

(defun force-assumption
  (rune target
    term
    type-alist
    rewrittenp
    immediatep
    force-flg
    ttree)
  (let ((type-alist (remove-assumption-entries-from-type-alist type-alist)) (ttree (push-lemma *force-xrune* ttree)))
    (cond ((not force-flg) (mv force-flg
          (er hard
            'force-assumption
            "Force-assumption called with null force-flg!")))
      (t (mv force-flg
          (force-assumption1 rune
            target
            term
            type-alist
            rewrittenp
            immediatep
            ttree))))))

(defun tag-tree-occur-assumption-nil-1
  (lst)
  (cond ((endp lst) nil)
    ((equal (access assumption (car lst) :term) *nil*) t)
    (t (tag-tree-occur-assumption-nil-1 (cdr lst)))))

(defun tag-tree-occur-assumption-nil
  (ttree)
  (tag-tree-occur-assumption-nil-1 (tagged-objects 'assumption ttree)))

(defun assumption-free-ttreep
  (ttree)
  (cond ((tagged-objectsp 'assumption ttree) nil)
    ((tagged-objectsp 'fc-derivation ttree) nil)
    (t t)))

(defun fn-count-evg-rec
  (evg acc calls)
  (declare (xargs :measure (acl2-count evg) :ruler-extenders :all)
    (type (unsigned-byte 60) acc calls))
  (the (unsigned-byte 60)
    (cond ((or (>= calls (fn-count-evg-max-calls))
         (>= acc (fn-count-evg-max-val))) (fn-count-evg-max-val))
      ((atom evg) (cond ((rationalp evg) (cond ((integerp evg) (cond ((< evg 0) (cond ((<= evg (fn-count-evg-max-val-neg)) (fn-count-evg-max-val))
                      (t (min-fixnat (fn-count-evg-max-val) (+f 2 acc (-f evg))))))
                  (t (cond ((<= (fn-count-evg-max-val) evg) (fn-count-evg-max-val))
                      (t (min-fixnat (fn-count-evg-max-val) (+f 1 acc evg)))))))
              (t (fn-count-evg-rec (numerator evg)
                  (fn-count-evg-rec (denominator evg)
                    (1+f acc)
                    (1+f calls))
                  (+f 2 calls)))))
          ((complex-rationalp evg) (fn-count-evg-rec (realpart evg)
              (fn-count-evg-rec (imagpart evg) (1+f acc) (1+f calls))
              (+f 2 calls)))
          ((symbolp evg) (cond ((null evg) (min-fixnat (fn-count-evg-max-val) (+f 8 acc)))
              (t (let ((len (length (symbol-name evg))))
                  (cond ((<= (fn-count-evg-max-val) len) (fn-count-evg-max-val))
                    (t (min-fixnat (fn-count-evg-max-val) (+f 2 acc (*f 2 len)))))))))
          ((stringp evg) (let ((len (length evg)))
              (cond ((<= (fn-count-evg-max-val) len) (fn-count-evg-max-val))
                (t (min-fixnat (fn-count-evg-max-val) (+f 1 acc (*f 2 len)))))))
          (t (1+f acc))))
      (t (fn-count-evg-rec (cdr evg)
          (fn-count-evg-rec (car evg) (1+f acc) (1+f calls))
          (+f 2 calls))))))

(defun var-fn-count-1
  (flg x
    var-count-acc
    fn-count-acc
    p-fn-count-acc
    invisible-fns
    invisible-fns-table)
  (declare (xargs :guard (and (if flg
          (pseudo-term-listp x)
          (pseudo-termp x))
        (integerp var-count-acc)
        (integerp fn-count-acc)
        (integerp p-fn-count-acc)
        (symbol-listp invisible-fns)
        (alistp invisible-fns-table)
        (symbol-list-listp invisible-fns-table))
      :verify-guards nil))
  (cond (flg (cond ((atom x) (mv var-count-acc fn-count-acc p-fn-count-acc))
        (t (mv-let (var-cnt fn-cnt p-fn-cnt)
            (let* ((term (car x)) (fn (and (nvariablep term) (not (fquotep term)) (ffn-symb term)))
                (invp (and fn (not (flambdap fn)) (member-eq fn invisible-fns))))
              (cond (invp (var-fn-count-1 t
                    (fargs term)
                    var-count-acc
                    fn-count-acc
                    p-fn-count-acc
                    (cdr (assoc-eq fn invisible-fns-table))
                    invisible-fns-table))
                (t (var-fn-count-1 nil
                    term
                    var-count-acc
                    fn-count-acc
                    p-fn-count-acc
                    nil
                    invisible-fns-table))))
            (var-fn-count-1 t
              (cdr x)
              var-cnt
              fn-cnt
              p-fn-cnt
              invisible-fns
              invisible-fns-table)))))
    ((variablep x) (mv (1+ var-count-acc) fn-count-acc p-fn-count-acc))
    ((fquotep x) (mv var-count-acc
        fn-count-acc
        (+ p-fn-count-acc (fn-count-evg (cadr x)))))
    (t (var-fn-count-1 t
        (fargs x)
        var-count-acc
        (1+ fn-count-acc)
        p-fn-count-acc
        (and invisible-fns-table
          (let ((fn (ffn-symb x)))
            (and (symbolp fn) (cdr (assoc-eq fn invisible-fns-table)))))
        invisible-fns-table))))

(defun term-order1
  (term1 term2 invisible-fns-table)
  (declare (xargs :guard (and (pseudo-termp term1)
        (pseudo-termp term2)
        (alistp invisible-fns-table)
        (symbol-list-listp invisible-fns-table))))
  (mv-let (var-count1 fn-count1 p-fn-count1)
    (var-fn-count term1 invisible-fns-table)
    (mv-let (var-count2 fn-count2 p-fn-count2)
      (var-fn-count term2 invisible-fns-table)
      (cond ((< var-count1 var-count2) t)
        ((> var-count1 var-count2) nil)
        ((< fn-count1 fn-count2) t)
        ((> fn-count1 fn-count2) nil)
        ((< p-fn-count1 p-fn-count2) t)
        ((> p-fn-count1 p-fn-count2) nil)
        (t (lexorder term1 term2))))))

(defun arith-term-order
  (term1 term2)
  (term-order1 term1 term2 '((binary-* unary-/))))

(defun good-coefficient (c) (equal (abs c) 1))

(defun good-pot-varp
  (x)
  (and (not (quotep x))
    (not (equal (fn-symb x) 'binary-+))
    (not (and (equal (fn-symb x) 'binary-*)
        (quotep (fargn x 1))
        (real/rationalp (unquote (fargn x 1)))))
    (not (and (equal (fn-symb x) 'unary--)
        (quotep (fargn x 1))
        (real/rationalp (unquote (fargn x 1)))))))

(defun good-polyp
  (p)
  (and (good-coefficient (first-coefficient p))
    (good-pot-varp (first-var p))))

(defun logical-<
  (x y)
  (declare (xargs :guard (and (acl2-numberp x) (acl2-numberp y))))
  (cond ((and (real/rationalp x) (real/rationalp y)) (< x y))
    ((< (realpart x) (realpart y)) t)
    (t (and (= (realpart x) (realpart y))
        (< (imagpart x) (imagpart y))))))

(defun logical-<=
  (x y)
  (declare (xargs :guard (and (acl2-numberp x) (acl2-numberp y))))
  (cond ((and (real/rationalp x) (real/rationalp y)) (<= x y))
    ((< (realpart x) (realpart y)) t)
    (t (and (= (realpart x) (realpart y))
        (<= (imagpart x) (imagpart y))))))

(defun evaluate-ground-poly
  (p)
  (if (eq (access poly p :relation) '<)
    (logical-< 0 (access poly p :constant))
    (logical-<= 0 (access poly p :constant))))

(defun impossible-polyp
  (p)
  (and (null (access poly p :alist))
    (eq (evaluate-ground-poly p) nil)))

(defun true-polyp
  (p)
  (and (null (access poly p :alist)) (evaluate-ground-poly p)))

(defun silly-polyp
  (poly)
  (tag-tree-occur-assumption-nil (access poly poly :ttree)))

(defun impossible-poly
  (ttree)
  (make poly
    :alist nil
    :parents (collect-parents ttree)
    :rational-poly-p t
    :derived-from-not-equalityp nil
    :ttree ttree
    :constant -1
    :relation '<))

(defun base-poly0
  (ttree parents
    relation
    rational-poly-p
    derived-from-not-equalityp)
  (make poly
    :alist nil
    :parents parents
    :rational-poly-p rational-poly-p
    :derived-from-not-equalityp derived-from-not-equalityp
    :ttree ttree
    :constant 0
    :relation relation))

(defun base-poly
  (ttree relation rational-poly-p derived-from-not-equalityp)
  (make poly
    :alist nil
    :parents (collect-parents ttree)
    :rational-poly-p rational-poly-p
    :derived-from-not-equalityp derived-from-not-equalityp
    :ttree ttree
    :constant 0
    :relation relation))

(defun poly-alist-equal
  (alist1 alist2)
  (cond ((null alist1) (null alist2))
    ((null alist2) nil)
    (t (and (eql (cdar alist1) (cdar alist2))
        (equal (caar alist1) (caar alist2))
        (poly-alist-equal (cdr alist1) (cdr alist2))))))

(defun poly-equal
  (poly1 poly2)
  (and (eql (access poly poly1 :constant)
      (access poly poly2 :constant))
    (eql (access poly poly1 :relation)
      (access poly poly2 :relation))
    (poly-alist-equal (access poly poly1 :alist)
      (access poly poly2 :alist))))

(defun poly-weakerp
  (poly1 poly2 parents-check)
  (let ((c1 (access poly poly1 :constant)) (c2 (access poly poly2 :constant)))
    (and (or (logical-< c2 c1)
        (and (eql c1 c2)
          (or (eq (access poly poly1 :relation) '<=)
            (eq (access poly poly2 :relation) '<))))
      (poly-alist-equal (access poly poly1 :alist)
        (access poly poly2 :alist))
      (if parents-check
        (subsetp (access poly poly2 :parents)
          (access poly poly1 :parents))
        t))))

(defun poly-member
  (p lst)
  (and (consp lst)
    (or (poly-weakerp p (car lst) t) (poly-member p (cdr lst)))))

(defun new-and-ugly-linear-varsp
  (lst flag term)
  (cond ((not flag) nil)
    ((null lst) nil)
    ((arith-term-order term (first-var (car lst))) t)
    (t (new-and-ugly-linear-varsp (cdr lst) flag term))))

(defun filter-polys
  (lst ans)
  (cond ((null lst) (mv nil ans))
    ((impossible-polyp (car lst)) (mv (car lst) nil))
    ((true-polyp (car lst)) (filter-polys (cdr lst) ans))
    ((poly-member (car lst) ans) (filter-polys (cdr lst) ans))
    (t (filter-polys (cdr lst) (cons (car lst) ans)))))

(defun add-linear-variable1
  (n var alist)
  (cond ((null alist) (cons (cons var n) nil))
    ((arith-term-order var (caar alist)) (cond ((equal var (caar alist)) (let ((k (+ (cdar alist) n)))
            (cond ((= k 0) (cdr alist))
              (t (cons (cons var k) (cdr alist))))))
        (t (cons (car alist) (add-linear-variable1 n var (cdr alist))))))
    (t (cons (cons var n) alist))))

(defun zero-factor-p
  (term)
  (cond ((variablep term) nil)
    ((fquotep term) (equal term *0*))
    ((eq (ffn-symb term) 'binary-*) (or (zero-factor-p (fargn term 1))
        (zero-factor-p (fargn term 2))))
    (t nil)))

(defun get-coefficient
  (term acc)
  (if (and (eq (fn-symb term) 'binary-*)
      (quotep (fargn term 1))
      (real/rationalp (unquote (fargn term 1))))
    (get-coefficient (fargn term 2)
      (* (unquote (fargn term 1)) acc))
    (mv acc term)))

(defun add-linear-variable
  (term side p)
  (mv-let (n term)
    (cond ((zero-factor-p term) (mv 0 nil))
      ((and (eq (fn-symb term) 'binary-*)
         (quotep (fargn term 1))
         (real/rationalp (unquote (fargn term 1)))) (mv-let (coeff new-term)
          (get-coefficient term 1)
          (if (eq side 'lhs)
            (mv (- coeff) new-term)
            (mv coeff new-term))))
      ((eq side 'lhs) (mv -1 term))
      (t (mv 1 term)))
    (if (= n 0)
      p
      (change poly
        p
        :alist (add-linear-variable1 n term (access poly p :alist))))))

(defun dumb-eval-yields-quotep
  (term)
  (cond ((variablep term) nil)
    ((fquotep term) t)
    ((equal (ffn-symb term) 'binary-*) (and (dumb-eval-yields-quotep (fargn term 1))
        (dumb-eval-yields-quotep (fargn term 2))))
    ((equal (ffn-symb term) 'binary-+) (and (dumb-eval-yields-quotep (fargn term 1))
        (dumb-eval-yields-quotep (fargn term 2))))
    ((equal (ffn-symb term) 'unary--) (dumb-eval-yields-quotep (fargn term 1)))
    (t nil)))

(defun dumb-eval
  (term)
  (cond ((variablep term) (er hard
        'dumb-eval
        "Bad term. We were expecting a constant, but encountered
              the variable ~x0."
        term))
    ((fquotep term) (if (acl2-numberp (unquote term))
        (unquote term)
        0))
    ((equal (ffn-symb term) 'binary-*) (* (dumb-eval (fargn term 1)) (dumb-eval (fargn term 2))))
    ((equal (ffn-symb term) 'binary-+) (+ (dumb-eval (fargn term 1)) (dumb-eval (fargn term 2))))
    ((equal (ffn-symb term) 'unary--) (- (dumb-eval (fargn term 1))))
    (t (er hard
        'dumb-eval
        "Bad term. The term ~x0 was not as expected by dumb-eval."
        term))))

(defun add-linear-term
  (term side p)
  (cond ((variablep term) (add-linear-variable term side p))
    ((dumb-eval-yields-quotep term) (let ((temp (dumb-eval term)))
        (if (eq side 'lhs)
          (change poly
            p
            :constant (+ (access poly p :constant) (- temp)))
          (change poly p :constant (+ (access poly p :constant) temp)))))
    (t (let ((fn1 (ffn-symb term)))
        (case fn1
          (binary-+ (add-linear-term (fargn term 1)
              side
              (add-linear-term (fargn term 2) side p)))
          (unary-- (add-linear-term (fargn term 1)
              (if (eq side 'lhs)
                'rhs
                'lhs)
              p))
          (binary-* (cond ((and (quotep (fargn term 1))
                 (real/rationalp (unquote (fargn term 1)))
                 (equal (fn-symb (fargn term 2)) 'binary-+)) (add-linear-term (mcons-term* 'binary-+
                    (mcons-term* 'binary-*
                      (fargn term 1)
                      (fargn (fargn term 2) 1))
                    (mcons-term* 'binary-*
                      (fargn term 1)
                      (fargn (fargn term 2) 2)))
                  side
                  p))
              ((and (quotep (fargn term 1))
                 (real/rationalp (unquote (fargn term 1)))
                 (equal (fn-symb (fargn term 2)) 'binary-*)
                 (quotep (fargn (fargn term 2) 1))
                 (real/rationalp (unquote (fargn (fargn term 2) 1)))) (add-linear-term (mcons-term* 'binary-*
                    (kwote (* (unquote (fargn term 1))
                        (unquote (fargn (fargn term 2) 1))))
                    (fargn (fargn term 2) 2))
                  side
                  p))
              (t (add-linear-variable term side p))))
          (otherwise (add-linear-variable term side p)))))))

(defun add-linear-terms-fn
  (rst)
  (cond ((null (cdr rst)) (car rst))
    ((eq (car rst) :lhs) `(add-linear-term ,(CADR RST)
        'lhs
        ,(ADD-LINEAR-TERMS-FN (CDDR RST))))
    ((eq (car rst) :rhs) `(add-linear-term ,(CADR RST)
        'rhs
        ,(ADD-LINEAR-TERMS-FN (CDDR RST))))
    (t (er hard 'add-linear-terms-fn "Bad term ~x0" rst))))

(defun normalize-poly1
  (coeff alist)
  (cond ((null alist) nil)
    (t (acons (caar alist)
        (/ (cdar alist) coeff)
        (normalize-poly1 coeff (cdr alist))))))

(defun normalize-poly
  (p)
  (if (access poly p :alist)
    (let ((c (abs (first-coefficient p))))
      (cond ((eql c 1) p)
        (t (change poly
            p
            :alist (normalize-poly1 c (access poly p :alist))
            :constant (/ (access poly p :constant) c)))))
    p))

(defun normalize-poly-lst
  (poly-lst)
  (cond ((null poly-lst) nil)
    (t (cons (normalize-poly (car poly-lst))
        (normalize-poly-lst (cdr poly-lst))))))

(defun modify-linear-pot
  (pot pos neg)
  (if (equal neg (access linear-pot pot :negatives))
    (if (equal pos (access linear-pot pot :positives))
      pot
      (change linear-pot pot :positives pos))
    (if (equal pos (access linear-pot pot :positives))
      (change linear-pot pot :negatives neg)
      (change linear-pot pot :positives pos :negatives neg))))

(defun loop-stopper-value-of-var
  (var pot-lst)
  (cond ((null pot-lst) 0)
    ((equal var (access linear-pot (car pot-lst) :var)) (access linear-pot (car pot-lst) :loop-stopper-value))
    (t (loop-stopper-value-of-var var (cdr pot-lst)))))

(defun set-loop-stopper-values
  (new-vars new-pot-lst term value)
  (cond ((null new-vars) new-pot-lst)
    ((equal (car new-vars)
       (access linear-pot (car new-pot-lst) :var)) (cond ((arith-term-order term (car new-vars)) (cons (change linear-pot
              (car new-pot-lst)
              :loop-stopper-value (1+ value))
            (set-loop-stopper-values (cdr new-vars)
              (cdr new-pot-lst)
              term
              value)))
        (t (cons (change linear-pot
              (car new-pot-lst)
              :loop-stopper-value value)
            (set-loop-stopper-values (cdr new-vars)
              (cdr new-pot-lst)
              term
              value)))))
    (t (cons (car new-pot-lst)
        (set-loop-stopper-values new-vars
          (cdr new-pot-lst)
          term
          value)))))

(defun var-in-pot-lst-p
  (var pot-lst)
  (cond ((null pot-lst) nil)
    ((equal var (access linear-pot (car pot-lst) :var)) t)
    (t (var-in-pot-lst-p var (cdr pot-lst)))))

(defun bounds-poly-with-var
  (poly-lst pt bounds-poly)
  (cond ((null poly-lst) bounds-poly)
    ((and (null (cdr (access poly (car poly-lst) :alist)))
       (rationalp (access poly (car poly-lst) :constant))
       (not (ignore-polyp (access poly (car poly-lst) :parents) pt))) (bounds-poly-with-var (cdr poly-lst)
        pt
        (cond ((and bounds-poly
             (poly-weakerp (car poly-lst) bounds-poly nil)) bounds-poly)
          (t (car poly-lst)))))
    (t (bounds-poly-with-var (cdr poly-lst) pt bounds-poly))))

(defun bounds-polys-with-var
  (var pot-lst pt)
  (cond ((null pot-lst) nil)
    ((equal var (access linear-pot (car pot-lst) :var)) (let ((neg (bounds-poly-with-var (access linear-pot (car pot-lst) :negatives)
             pt
             nil)) (pos (bounds-poly-with-var (access linear-pot (car pot-lst) :positives)
              pt
              nil)))
        (cond (neg (if pos
              (list neg pos)
              (list neg)))
          (t (if pos
              (list pos)
              nil)))))
    (t (bounds-polys-with-var var (cdr pot-lst) pt))))

(defun polys-with-var1
  (var pot-lst)
  (cond ((null pot-lst) nil)
    ((equal var (access linear-pot (car pot-lst) :var)) (append (access linear-pot (car pot-lst) :negatives)
        (access linear-pot (car pot-lst) :positives)))
    (t (polys-with-var1 var (cdr pot-lst)))))

(defun polys-with-var
  (var pot-lst)
  (if (eq (fn-symb var) 'binary-+)
    nil
    (polys-with-var1 var pot-lst)))

(defun polys-with-pots
  (polys pot-lst ans)
  (cond ((null polys) ans)
    ((var-in-pot-lst-p (first-var (car polys)) pot-lst) (polys-with-pots (cdr polys) pot-lst (cons (car polys) ans)))
    (t (polys-with-pots (cdr polys) pot-lst ans))))

(defun new-vars-in-pot-lst
  (new-pot-lst old-pot-lst include-variableps)
  (cond ((null new-pot-lst) nil)
    ((or (null old-pot-lst)
       (not (equal (access linear-pot (car new-pot-lst) :var)
           (access linear-pot (car old-pot-lst) :var)))) (if (or include-variableps
          (not (variablep (access linear-pot (car new-pot-lst) :var))))
        (cons (access linear-pot (car new-pot-lst) :var)
          (new-vars-in-pot-lst (cdr new-pot-lst)
            old-pot-lst
            include-variableps))
        (new-vars-in-pot-lst (cdr new-pot-lst)
          old-pot-lst
          include-variableps)))
    (t (new-vars-in-pot-lst (cdr new-pot-lst)
        (cdr old-pot-lst)
        include-variableps))))

(defun changed-pot-vars
  (new-pot-lst old-pot-lst to-be-ignored-lst)
  (cond ((null new-pot-lst) nil)
    ((equal (access linear-pot (car new-pot-lst) :var)
       (access linear-pot (car old-pot-lst) :var)) (if (or (equal (car new-pot-lst) (car old-pot-lst))
          (member-equal (access linear-pot (car new-pot-lst) :var)
            to-be-ignored-lst))
        (changed-pot-vars (cdr new-pot-lst)
          (cdr old-pot-lst)
          to-be-ignored-lst)
        (cons (access linear-pot (car new-pot-lst) :var)
          (changed-pot-vars (cdr new-pot-lst)
            (cdr old-pot-lst)
            to-be-ignored-lst))))
    (t (cons (access linear-pot (car new-pot-lst) :var)
        (changed-pot-vars (cdr new-pot-lst)
          old-pot-lst
          to-be-ignored-lst)))))

(defun infect-polys
  (lst ttree parents)
  (cond ((null lst) nil)
    (t (cons (change poly
          (car lst)
          :ttree (cons-tag-trees ttree (access poly (car lst) :ttree))
          :parents (marry-parents parents (access poly (car lst) :parents)))
        (infect-polys (cdr lst) ttree parents)))))

(defun infect-first-n-polys
  (lst n ttree parents)
  (cond ((int= n 0) lst)
    (t (cons (change poly
          (car lst)
          :ttree (cons-tag-trees ttree (access poly (car lst) :ttree))
          :parents (marry-parents parents (access poly (car lst) :parents)))
        (infect-first-n-polys (cdr lst) (1- n) ttree parents)))))

(defun infect-new-polys
  (new-pot-lst old-pot-lst ttree)
  (cond ((null new-pot-lst) nil)
    ((or (null old-pot-lst)
       (not (equal (access linear-pot (car new-pot-lst) :var)
           (access linear-pot (car old-pot-lst) :var)))) (let ((new-new-pot-lst (infect-new-polys (cdr new-pot-lst) old-pot-lst ttree)))
        (cons (modify-linear-pot (car new-pot-lst)
            (infect-polys (access linear-pot (car new-pot-lst) :positives)
              ttree
              (collect-parents ttree))
            (infect-polys (access linear-pot (car new-pot-lst) :negatives)
              ttree
              (collect-parents ttree)))
          new-new-pot-lst)))
    (t (let ((new-new-pot-lst (infect-new-polys (cdr new-pot-lst) (cdr old-pot-lst) ttree)))
        (cons (modify-linear-pot (car new-pot-lst)
            (infect-first-n-polys (access linear-pot (car new-pot-lst) :positives)
              (- (length (access linear-pot (car new-pot-lst) :positives))
                (length (access linear-pot (car old-pot-lst) :positives)))
              ttree
              (collect-parents ttree))
            (infect-first-n-polys (access linear-pot (car new-pot-lst) :negatives)
              (- (length (access linear-pot (car new-pot-lst) :negatives))
                (length (access linear-pot (car old-pot-lst) :negatives)))
              ttree
              (collect-parents ttree)))
          new-new-pot-lst)))))

(defun fcomplementary-multiplep1
  (alist1 alist2)
  (cond ((null alist1) (null alist2))
    ((null alist2) nil)
    ((and (equal (caar alist1) (caar alist2))
       (= (cdar alist1) (- (cdar alist2)))) (fcomplementary-multiplep1 (cdr alist1) (cdr alist2)))
    (t nil)))

(defun fcomplementary-multiplep
  (poly1 poly2)
  (and (= (access poly poly1 :constant)
      (- (access poly poly2 :constant)))
    (fcomplementary-multiplep1 (cdr (access poly poly1 :alist))
      (cdr (access poly poly2 :alist)))))

(defun already-used-by-find-equational-polyp-lst
  (poly1 lst)
  (cond ((endp lst) nil)
    (t (or (poly-equal (car (car lst)) poly1)
        (already-used-by-find-equational-polyp-lst poly1 (cdr lst))))))

(defun already-used-by-find-equational-polyp
  (poly1 hist)
  (cond ((null hist) nil)
    ((and (eq (access history-entry (car hist) :processor)
         'simplify-clause)
       (already-used-by-find-equational-polyp-lst poly1
         (tagged-objects 'find-equational-poly
           (access history-entry (car hist) :ttree)))) t)
    (t (already-used-by-find-equational-polyp poly1 (cdr hist)))))

(defun cons-term-binary-+-constant
  (x term)
  (cond ((= x 0) term)
    ((quotep term) (kwote (+ x (cadr term))))
    (t (fcons-term* 'binary-+ (kwote x) term))))

(defun cons-term-unary--
  (term)
  (cond ((variablep term) (fcons-term* 'unary-- term))
    ((fquotep term) (kwote (- (cadr term))))
    ((eq (ffn-symb term) 'unary--) (fargn term 1))
    (t (fcons-term* 'unary-- term))))

(defun cons-term-binary-*-constant
  (x term)
  (cond ((= x 0) (kwote 0))
    ((= x 1) term)
    ((= x -1) (cons-term-unary-- term))
    ((quotep term) (kwote (* x (cadr term))))
    (t (fcons-term* 'binary-* (kwote x) term))))

(defun find-equational-poly-rhs1
  (alist)
  (cond ((null alist) *0*)
    ((null (cdr alist)) (cons-term-binary-*-constant (- (cdar alist)) (caar alist)))
    (t (cons-term 'binary-+
        (list (cons-term-binary-*-constant (- (cdar alist)) (caar alist))
          (find-equational-poly-rhs1 (cdr alist)))))))

(defun find-equational-poly-rhs
  (poly1)
  (cons-term-binary-+-constant (- (access poly poly1 :constant))
    (find-equational-poly-rhs1 (cdr (access poly poly1 :alist)))))

(defun find-equational-poly3
  (poly1 poly2 hist)
  (cond ((and (fcomplementary-multiplep poly1 poly2)
       (not (already-used-by-find-equational-polyp poly1 hist))) (mv (add-to-tag-tree 'find-equational-poly
          (cons poly1 poly2)
          (cons-tag-trees (access poly poly1 :ttree)
            (access poly poly2 :ttree)))
        (first-var poly1)
        (find-equational-poly-rhs poly1)))
    (t (mv nil nil nil))))

(defun find-equational-poly2
  (poly1 negatives hist)
  (cond ((null negatives) (mv nil nil nil))
    ((or (not (eq (access poly (car negatives) :relation) '<=))
       (access poly (car negatives) :derived-from-not-equalityp)) (find-equational-poly2 poly1 (cdr negatives) hist))
    (t (mv-let (msg lhs rhs)
        (find-equational-poly3 poly1 (car negatives) hist)
        (cond (msg (mv msg lhs rhs))
          (t (find-equational-poly2 poly1 (cdr negatives) hist)))))))

(defun find-equational-poly1
  (positives negatives hist)
  (cond ((null positives) (mv nil nil nil))
    ((or (not (eq (access poly (car positives) :relation) '<=))
       (access poly (car positives) :derived-from-not-equalityp)) (find-equational-poly1 (cdr positives) negatives hist))
    (t (mv-let (msg lhs rhs)
        (find-equational-poly2 (car positives) negatives hist)
        (cond (msg (mv msg lhs rhs))
          (t (find-equational-poly1 (cdr positives) negatives hist)))))))

(defun find-equational-poly
  (pot hist)
  (find-equational-poly1 (access linear-pot pot :positives)
    (access linear-pot pot :negatives)
    hist))

(defun get-coeff-for-cancel1
  (alist1 alist2)
  (cond ((null alist1) (if (null alist2)
        1
        (abs (cdar alist2))))
    ((null alist2) (abs (cdar alist1)))
    ((not (arith-term-order (caar alist1) (caar alist2))) (abs (cdar alist1)))
    ((equal (caar alist1) (caar alist2)) (let ((temp (+ (cdar alist1) (cdar alist2))))
        (if (eql temp 0)
          (get-coeff-for-cancel1 (cdr alist1) (cdr alist2))
          (abs temp))))
    (t (abs (cdar alist2)))))

(defun cancel2
  (alist coeff)
  (cond ((null alist) nil)
    (t (cons (cons (caar alist) (/ (cdar alist) coeff))
        (cancel2 (cdr alist) coeff)))))

(defun cancel1
  (alist1 alist2 coeff)
  (cond ((null alist1) (cancel2 alist2 coeff))
    ((null alist2) (cancel2 alist1 coeff))
    ((not (arith-term-order (caar alist1) (caar alist2))) (cons (cons (caar alist1) (/ (cdar alist1) coeff))
        (cancel1 (cdr alist1) alist2 coeff)))
    ((equal (caar alist1) (caar alist2)) (let ((temp (/ (+ (cdar alist1) (cdar alist2)) coeff)))
        (cond ((= temp 0) (cancel1 (cdr alist1) (cdr alist2) coeff))
          (t (cons (cons (caar alist1) temp)
              (cancel1 (cdr alist1) (cdr alist2) coeff))))))
    (t (cons (cons (caar alist2) (/ (cdar alist2) coeff))
        (cancel1 alist1 (cdr alist2) coeff)))))

(defun cancel
  (p1 p2)
  (let* ((alist1 (cdr (access poly p1 :alist))) (alist2 (cdr (access poly p2 :alist)))
      (coeff (get-coeff-for-cancel1 alist1 alist2))
      (p (make poly
          :constant (/ (+ (access poly p1 :constant) (access poly p2 :constant))
            coeff)
          :alist (cancel1 alist1 alist2 coeff)
          :relation (if (or (eq (access poly p1 :relation) '<)
              (eq (access poly p2 :relation) '<))
            '<
            '<=)
          :ttree (cons-tag-trees (access poly p1 :ttree)
            (access poly p2 :ttree))
          :rational-poly-p (and (access poly p1 :rational-poly-p)
            (access poly p2 :rational-poly-p))
          :parents (marry-parents (access poly p1 :parents)
            (access poly p2 :parents))
          :derived-from-not-equalityp nil)))
    (cond ((impossible-polyp p) (mv p nil))
      ((true-polyp p) (mv nil nil))
      (t (mv nil p)))))

(defun cancel-poly-against-all-polys
  (p polys pt ans)
  (cond ((null polys) (mv nil ans))
    ((ignore-polyp (access poly (car polys) :parents) pt) (cancel-poly-against-all-polys p (cdr polys) pt ans))
    (t (mv-let (contradictionp new-p)
        (cancel p (car polys))
        (cond (contradictionp (mv contradictionp nil))
          (t (cancel-poly-against-all-polys p
              (cdr polys)
              pt
              (if (and new-p (not (poly-member new-p ans)))
                (cons new-p ans)
                ans))))))))

(defun add-poly
  (p pot-lst to-do-next pt nonlinearp)
  (cond ((time-limit5-reached-p "Out of time in linear arithmetic (add-poly).") (mv nil nil nil))
    ((or (null pot-lst)
       (not (arith-term-order (access linear-pot (car pot-lst) :var)
           (first-var p)))) (mv nil
        (cons (if (< 0 (first-coefficient p))
            (make linear-pot
              :var (first-var p)
              :loop-stopper-value 0
              :positives (list p)
              :negatives nil)
            (make linear-pot
              :var (first-var p)
              :loop-stopper-value 0
              :positives nil
              :negatives (list p)))
          pot-lst)
        to-do-next))
    ((equal (access linear-pot (car pot-lst) :var) (first-var p)) (cond ((poly-member p
           (if (< 0 (first-coefficient p))
             (access linear-pot (car pot-lst) :positives)
             (access linear-pot (car pot-lst) :negatives))) (mv nil pot-lst to-do-next))
        (t (mv-let (contradictionp to-do-next)
            (cancel-poly-against-all-polys p
              (if (< 0 (first-coefficient p))
                (access linear-pot (car pot-lst) :negatives)
                (access linear-pot (car pot-lst) :positives))
              pt
              to-do-next)
            (cond (contradictionp (mv contradictionp nil nil))
              ((and nonlinearp
                 (>=-len (if (< 0 (first-coefficient p))
                     (access linear-pot (car pot-lst) :positives)
                     (access linear-pot (car pot-lst) :negatives))
                   21)) (mv nil pot-lst to-do-next))
              (t (mv nil
                  (cons (if (< 0 (first-coefficient p))
                      (change linear-pot
                        (car pot-lst)
                        :positives (cons p (access linear-pot (car pot-lst) :positives)))
                      (change linear-pot
                        (car pot-lst)
                        :negatives (cons p (access linear-pot (car pot-lst) :negatives))))
                    (cdr pot-lst))
                  to-do-next)))))))
    (t (mv-let (contradictionp cdr-pot-lst to-do-next)
        (add-poly p (cdr pot-lst) to-do-next pt nonlinearp)
        (cond (contradictionp (mv contradictionp nil nil))
          (t (mv nil (cons (car pot-lst) cdr-pot-lst) to-do-next)))))))

(defun prune-poly-lst
  (poly-lst ans)
  (cond ((null poly-lst) ans)
    ((endp (cddr (access poly (car poly-lst) :alist))) (prune-poly-lst (cdr poly-lst) (cons (car poly-lst) ans)))
    (t (prune-poly-lst (cdr poly-lst) ans))))

(defun add-polys1
  (lst pot-lst
    new-lst
    pt
    nonlinearp
    max-rounds
    rounds-completed)
  (cond ((eql max-rounds rounds-completed) (mv nil pot-lst))
    ((null lst) (cond ((null new-lst) (mv nil pot-lst))
        ((and (>=-len new-lst 101)) (add-polys1 (prune-poly-lst new-lst nil)
            pot-lst
            nil
            pt
            nonlinearp
            max-rounds
            (+ 1 rounds-completed)))
        (t (add-polys1 new-lst
            pot-lst
            nil
            pt
            nonlinearp
            max-rounds
            (+ 1 rounds-completed)))))
    (t (mv-let (contradictionp new-pot-lst new-lst)
        (add-poly (car lst) pot-lst new-lst pt nonlinearp)
        (cond (contradictionp (mv contradictionp nil))
          (t (add-polys1 (cdr lst)
              new-pot-lst
              new-lst
              pt
              nonlinearp
              max-rounds
              rounds-completed)))))))

(defun add-polys0
  (lst pot-lst pt nonlinearp max-rounds)
  (mv-let (contradictionp lst)
    (filter-polys lst nil)
    (cond (contradictionp (mv contradictionp nil))
      (t (add-polys1 lst pot-lst nil pt nonlinearp max-rounds 0)))))

(defun show-poly2
  (pair lst)
  (let ((n (abs (cdr pair))) (x (car pair)))
    (cond ((= n 1) (cond ((null lst) (list x)) (t (list* x '+ lst))))
      (t (cond ((null lst) (list n x)) (t (list* n x '+ lst)))))))

(defun show-poly1
  (alist lhs rhs)
  (cond ((null alist) (cons lhs rhs))
    ((logical-< 0 (cdar alist)) (show-poly1 (cdr alist) lhs (show-poly2 (car alist) rhs)))
    (t (show-poly1 (cdr alist) (show-poly2 (car alist) lhs) rhs))))

(defun show-poly-fn
  (poly parp)
  (let* ((pair (show-poly1 (cond ((null (access poly poly :alist)) nil)
           (t (cons (cons (if parp
                   (list (caar (access poly poly :alist)))
                   (caar (access poly poly :alist)))
                 (cdar (access poly poly :alist)))
               (cdr (access poly poly :alist)))))
         (cond ((= (access poly poly :constant) 0) nil)
           ((logical-< 0 (access poly poly :constant)) nil)
           (t (cons (- (access poly poly :constant)) nil)))
         (cond ((= (access poly poly :constant) 0) nil)
           ((logical-< 0 (access poly poly :constant)) (cons (access poly poly :constant) nil))
           (t nil)))) (lhs (car pair))
      (rhs (cdr pair)))
    (append (or lhs '(0))
      (cons (access poly poly :relation) (or rhs '(0))))))

(defun show-poly-lst-fn
  (poly-lst parp)
  (cond ((null poly-lst) nil)
    (t (cons (show-poly-fn (car poly-lst) parp)
        (show-poly-lst-fn (cdr poly-lst) parp)))))