fty-alist

(in-package "FTY")

(include-book "database")

(include-book "fty-parseutils")

(program)

(define flexalist-fns
  (x)
  (b* (((flexalist x) x))
    (list x.pred x.fix)))

(define flexalist-collect-fix/pred-pairs
  (alist)
  (b* (((flexalist alist) alist))
    (append (and alist.key-type
        alist.key-fix
        (list (cons alist.key-fix alist.key-type)))
      (and alist.val-type
        alist.val-fix
        (list (cons alist.val-fix alist.val-type))))))

(defconst *flexalist-keywords*
  '(:pred :fix :equiv :count :get :get-fast :set :set-fast :key-type :val-type :measure :measure-debug :xvar :parents :short :long :no-count :true-listp :unique-keys :prepwork :strategy :keyp-of-nil :valp-of-nil :post-pred-events :post-fix-events :post-events :enable-rules :already-definedp :verbosep))

(define parse-flexalist
  (x xvar
    our-fixtypes
    fixtypes
    state)
  (b* (((cons name args) x) ((unless (symbolp name)) (raise "Malformed flexalist: ~x0: name must be a symbol"
          x))
      ((mv pre-/// post-///) (split-/// name args))
      ((mv kwd-alist rest) (extract-keywords name
          *flexalist-keywords*
          pre-///
          nil))
      (kwd-alist (append kwd-alist
          (table-alist 'defalist-defaults
            (w state))))
      ((when rest) (raise "Malformed flexalist: ~x0: after kind should be a keyword/value list."
          name))
      (key-type (getarg :key-type nil kwd-alist))
      ((unless (symbolp key-type)) (raise "Bad flexalist ~x0: Element type must be a symbol"
          name))
      ((mv key-type
         key-fix
         key-equiv
         key-recp) (get-pred/fix/equiv (getarg :key-type nil kwd-alist)
          our-fixtypes
          fixtypes))
      (val-type (getarg :val-type nil kwd-alist))
      ((unless (symbolp val-type)) (raise "Bad flexalist ~x0: Element type must be a symbol"
          name))
      ((mv val-type
         val-fix
         val-equiv
         val-recp) (get-pred/fix/equiv (getarg :val-type nil kwd-alist)
          our-fixtypes
          fixtypes))
      (pred (getarg! :pred (intern-in-package-of-symbol (cat (symbol-name name) "-P")
            name)
          kwd-alist))
      (fix (getarg! :fix (intern-in-package-of-symbol (cat (symbol-name name) "-FIX")
            name)
          kwd-alist))
      (equiv (getarg! :equiv (intern-in-package-of-symbol (cat (symbol-name name) "-EQUIV")
            name)
          kwd-alist))
      (count (flextype-get-count-fn name kwd-alist))
      (xvar (or (getarg :xvar xvar kwd-alist)
          (car (find-symbols-named-x (getarg :measure nil kwd-alist)))
          (intern-in-package-of-symbol "X" name)))
      (measure (getarg! :measure `(acl2-count ,FTY::XVAR)
          kwd-alist))
      (strategy (getarg :strategy :fix-keys kwd-alist))
      (- (and (not (member strategy '(:fix-keys :drop-keys)))
          (raise "In flexalist ~x0: invalid strategy ~x1~%"
            name
            strategy)))
      ((mv already-defined true-listp) (check-flexlist-already-defined pred
          kwd-alist
          our-fixtypes
          name
          state))
      (fix-already-defined (check-flexlist-fix-already-defined fix
          kwd-alist
          our-fixtypes
          name
          state)))
    (make-flexalist :name name
      :pred pred
      :fix fix
      :equiv equiv
      :count count
      :key-type key-type
      :key-fix key-fix
      :key-equiv key-equiv
      :val-type val-type
      :val-fix val-fix
      :val-equiv val-equiv
      :measure measure
      :strategy strategy
      :kwd-alist (if post-///
        (cons (cons :///-events post-///) kwd-alist)
        kwd-alist)
      :xvar xvar
      :true-listp true-listp
      :recp (or key-recp val-recp)
      :already-definedp already-defined
      :fix-already-definedp fix-already-defined
      :keyp-of-nil (getarg :keyp-of-nil :unknown kwd-alist)
      :valp-of-nil (getarg :valp-of-nil :unknown kwd-alist)
      :unique-keys (getarg :unique-keys nil kwd-alist))))

(define flexalist-predicate-def
  (alist)
  (b* (((flexalist alist) alist) (stdx (intern-in-package-of-symbol "X" alist.pred))
      (std-defalist-call (and (not alist.unique-keys)
          `((defalist ,FTY::ALIST.PRED
             (,FTY::STDX)
             ,@(AND FTY::ALIST.KEY-TYPE `(:KEY (,FTY::ALIST.KEY-TYPE ,FTY::STDX)))
             ,@(AND FTY::ALIST.VAL-TYPE `(:VAL (,FTY::ALIST.VAL-TYPE ,FTY::STDX)))
             :true-listp ,FTY::ALIST.TRUE-LISTP
             :keyp-of-nil ,FTY::ALIST.KEYP-OF-NIL
             :valp-of-nil ,FTY::ALIST.VALP-OF-NIL
             :already-definedp t
             :parents nil
             :short nil
             :long nil)))))
    (if alist.already-definedp
      `(progn (local (in-theory (disable ,FTY::ALIST.PRED))) . ,FTY::STD-DEFALIST-CALL)
      `(define ,FTY::ALIST.PRED
        (,FTY::ALIST.XVAR)
        :parents (,FTY::ALIST.NAME)
        :progn t
        :short ,(STR::CAT "Recognizer for @(see " (XDOC::FULL-ESCAPE-SYMBOL FTY::ALIST.NAME)
  ").")
        :measure ,FTY::ALIST.MEASURE
        ,@(AND (FTY::GETARG :MEASURE-DEBUG NIL FTY::ALIST.KWD-ALIST)
       `(:MEASURE-DEBUG T))
        (if (atom ,FTY::ALIST.XVAR)
          ,(IF FTY::ALIST.TRUE-LISTP
     `(EQ ,FTY::ALIST.XVAR NIL)
     T)
          (and (consp (car ,FTY::ALIST.XVAR))
            ,@(AND FTY::ALIST.UNIQUE-KEYS
       `((NOT
          (FTY::HONS-ASSOC-EQUAL (CAAR ,FTY::ALIST.XVAR)
           (CDR ,FTY::ALIST.XVAR)))))
            ,@(AND FTY::ALIST.KEY-TYPE `((,FTY::ALIST.KEY-TYPE (CAAR ,FTY::ALIST.XVAR))))
            ,@(AND FTY::ALIST.VAL-TYPE `((,FTY::ALIST.VAL-TYPE (CDAR ,FTY::ALIST.XVAR))))
            (,FTY::ALIST.PRED (cdr ,FTY::ALIST.XVAR))))
        ///
        (local (in-theory (disable ,FTY::ALIST.PRED)))
        ,@(AND FTY::ALIST.UNIQUE-KEYS
       `((FTY::DEFTHM
          ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
            (FTY::CAT (SYMBOL-NAME FTY::ALIST.PRED) "-OF-CDR") FTY::ALIST.PRED)
          (FTY::IMPLIES (,FTY::ALIST.PRED ,FTY::ALIST.XVAR)
           (,FTY::ALIST.PRED (CDR ,FTY::ALIST.XVAR)))
          :HINTS (("goal" :EXPAND ((,FTY::ALIST.PRED ,FTY::ALIST.XVAR)))))
         ,@(AND FTY::ALIST.KEY-TYPE
                `((FTY::DEFTHM
                   ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
                     (FTY::CAT (SYMBOL-NAME FTY::ALIST.KEY-TYPE)
                      "-OF-CAAR-WHEN-" (SYMBOL-NAME FTY::ALIST.PRED))
                     FTY::ALIST.PRED)
                   (FTY::IMPLIES
                    (AND (,FTY::ALIST.PRED ,FTY::ALIST.XVAR)
                         (CONSP ,FTY::ALIST.XVAR))
                    (,FTY::ALIST.KEY-TYPE (CAAR ,FTY::ALIST.XVAR)))
                   :HINTS
                   (("goal" :EXPAND ((,FTY::ALIST.PRED ,FTY::ALIST.XVAR)))))))
         ,@(AND FTY::ALIST.VAL-TYPE
                `((FTY::DEFTHM
                   ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
                     (FTY::CAT (SYMBOL-NAME FTY::ALIST.VAL-TYPE)
                      "-OF-CDAR-WHEN-" (SYMBOL-NAME FTY::ALIST.PRED))
                     FTY::ALIST.PRED)
                   (FTY::IMPLIES
                    (AND (,FTY::ALIST.PRED ,FTY::ALIST.XVAR)
                         (CONSP ,FTY::ALIST.XVAR))
                    (,FTY::ALIST.VAL-TYPE (CDAR ,FTY::ALIST.XVAR)))
                   :HINTS
                   (("goal" :EXPAND ((,FTY::ALIST.PRED ,FTY::ALIST.XVAR)))))))
         (FTY::DEFTHM
          ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
            (FTY::CAT (SYMBOL-NAME FTY::ALIST.PRED) "-OF-CONS")
            FTY::ALIST.PRED)
          (EQUAL (,FTY::ALIST.PRED (CONS FTY::A ,FTY::ALIST.XVAR))
                 (AND
                  (AND (CONSP FTY::A)
                       ,@(AND FTY::ALIST.KEY-TYPE
                              `((,FTY::ALIST.KEY-TYPE (CAR FTY::A))))
                       ,@(AND FTY::ALIST.VAL-TYPE
                              `((,FTY::ALIST.VAL-TYPE (CDR FTY::A))))
                       (NOT
                        (FTY::HONS-ASSOC-EQUAL (CAR FTY::A) ,FTY::ALIST.XVAR)))
                  (,FTY::ALIST.PRED ,FTY::ALIST.XVAR)))
          :HINTS
          (("goal" :EXPAND
            ((,FTY::ALIST.PRED (CONS FTY::A ,FTY::ALIST.XVAR)))))))) . ,FTY::STD-DEFALIST-CALL))))

(define flexalist-fix-def
  (x flagp)
  (b* (((flexalist x) x))
    (if x.fix-already-definedp
      '(progn)
      `(define ,FTY::X.FIX
        ((,FTY::X.XVAR ,FTY::X.PRED))
        :parents (,FTY::X.NAME)
        :short ,(FTY::CAT "@(call " (XDOC::FULL-ESCAPE-SYMBOL FTY::X.FIX)
  ") is an @(see fty::fty) alist fixing function that follows the "
  (STR::DOWNCASE-STRING (SYMBOL-NAME FTY::X.STRATEGY)) " strategy.")
        :long "<p>Note that in the execution this is just an inline
              identity function.</p>"
        :measure ,FTY::X.MEASURE
        ,@(AND (FTY::GETARG :MEASURE-DEBUG NIL FTY::X.KWD-ALIST) `(:MEASURE-DEBUG T))
        ,@(AND FTY::FLAGP `(:FLAG ,FTY::X.NAME))
        :returns (newx ,FTY::X.PRED
          :hints ('(:in-theory (disable ,FTY::X.FIX ,FTY::X.PRED)
             :expand ((,FTY::X.FIX ,FTY::X.XVAR) (:free (a b) (,FTY::X.PRED (cons a b)))
               (,FTY::X.PRED ,FTY::X.XVAR)
               (,FTY::X.PRED nil)))))
        :verify-guards nil
        :progn t
        :inline t
        (mbe :logic (if (atom ,FTY::X.XVAR)
            ,(IF FTY::X.TRUE-LISTP
     NIL
     FTY::X.XVAR)
            ,(IF (AND (OR (NOT FTY::X.KEY-FIX) (EQ FTY::X.STRATEGY :FIX-KEYS))
          (NOT FTY::X.UNIQUE-KEYS))
     `(IF (CONSP (CAR ,FTY::X.XVAR))
          (CONS
           (CONS
            ,(IF FTY::X.KEY-FIX
                 `(,FTY::X.KEY-FIX (CAAR ,FTY::X.XVAR))
                 `(CAAR ,FTY::X.XVAR))
            ,(IF FTY::X.VAL-FIX
                 `(,FTY::X.VAL-FIX (CDAR ,FTY::X.XVAR))
                 `(CDAR ,FTY::X.XVAR)))
           (,FTY::X.FIX (CDR ,FTY::X.XVAR)))
          (,FTY::X.FIX (CDR ,FTY::X.XVAR)))
     `(LET ((REST (,FTY::X.FIX (CDR ,FTY::X.XVAR))))
        (IF (AND (CONSP (CAR ,FTY::X.XVAR))
                 ,@(AND FTY::X.KEY-FIX (NOT (EQ FTY::X.STRATEGY :FIX-KEYS))
                        `((,FTY::X.KEY-TYPE (CAAR ,FTY::X.XVAR)))))
            (LET ((FTY::FIRST-KEY
                   ,(IF (AND FTY::X.KEY-FIX (EQ FTY::X.STRATEGY :FIX-KEYS))
                        `(,FTY::X.KEY-FIX (CAAR ,FTY::X.XVAR))
                        `(CAAR ,FTY::X.XVAR)))
                  (FTY::FIRST-VAL
                   ,(IF FTY::X.VAL-FIX
                        `(,FTY::X.VAL-FIX (CDAR ,FTY::X.XVAR))
                        `(CDAR ,FTY::X.XVAR))))
              ,(IF FTY::X.UNIQUE-KEYS
                   `(IF (FTY::HONS-ASSOC-EQUAL FTY::FIRST-KEY REST)
                        REST
                        (CONS (CONS FTY::FIRST-KEY FTY::FIRST-VAL) REST))
                   `(CONS (CONS FTY::FIRST-KEY FTY::FIRST-VAL) REST)))
            REST))))
          :exec ,FTY::X.XVAR)
        ///))))

(define flexalist-fix-postevents
  (x)
  (b* (((flexalist x) x) (stdx (intern-in-package-of-symbol "X" x.pred)))
    `(,@(AND FTY::X.KEY-TYPE (EQ FTY::X.STRATEGY :FIX-KEYS)
       `((FTY::DEFFIXCONG ,FTY::X.KEY-EQUIV ,FTY::X.EQUIV
          (CONS (CONS FTY::K FTY::V) FTY::X) FTY::K :PKG ,FTY::X.EQUIV :HINTS
          (("goal" :EXPAND
            ((:FREE (FTY::A FTY::B) (,FTY::X.FIX (CONS FTY::A FTY::B))))))))) ,@(AND FTY::X.VAL-TYPE
       `((FTY::DEFFIXCONG ,FTY::X.VAL-EQUIV ,FTY::X.EQUIV
          (CONS (CONS FTY::K FTY::V) FTY::X) FTY::V :PKG ,FTY::X.EQUIV :HINTS
          (("goal" :EXPAND
            ((:FREE (FTY::A FTY::B) (,FTY::X.FIX (CONS FTY::A FTY::B)))))))))
      (deffixcong ,FTY::X.EQUIV
        ,FTY::X.EQUIV
        (cons x y)
        y
        :pkg ,FTY::X.EQUIV
        :hints (("goal" :expand ((:free (a b) (,FTY::X.FIX (cons a b)))))))
      (defthm ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
  (FTY::CAT (SYMBOL-NAME FTY::X.FIX) "-OF-ACONS") FTY::X.FIX)
        (equal (,FTY::X.FIX (cons (cons a b) ,FTY::STDX))
          ,(IF (AND (OR (EQ FTY::X.STRATEGY :FIX-KEYS) (NOT FTY::X.KEY-FIX))
          (NOT FTY::X.UNIQUE-KEYS))
     `(CONS
       (CONS
        ,(IF FTY::X.KEY-FIX
             `(,FTY::X.KEY-FIX FTY::A)
             'FTY::A)
        ,(IF FTY::X.VAL-FIX
             `(,FTY::X.VAL-FIX FTY::B)
             'FTY::B))
       (,FTY::X.FIX ,FTY::STDX))
     `(LET ((REST (,FTY::X.FIX ,FTY::STDX)))
        (IF (AND
             ,@(AND FTY::X.KEY-FIX (NOT (EQ FTY::X.STRATEGY :FIX-KEYS))
                    `((,FTY::X.KEY-TYPE FTY::A))))
            (LET ((FTY::FIRST-KEY
                   ,(IF (AND FTY::X.KEY-FIX (EQ FTY::X.STRATEGY :FIX-KEYS))
                        `(,FTY::X.KEY-FIX FTY::A)
                        'FTY::A))
                  (FTY::FIRST-VAL
                   ,(IF FTY::X.VAL-FIX
                        `(,FTY::X.VAL-FIX FTY::B)
                        'FTY::B)))
              ,(IF FTY::X.UNIQUE-KEYS
                   `(IF (FTY::HONS-ASSOC-EQUAL FTY::FIRST-KEY REST)
                        REST
                        (CONS (CONS FTY::FIRST-KEY FTY::FIRST-VAL) REST))
                   `(CONS (CONS FTY::FIRST-KEY FTY::FIRST-VAL) REST)))
            REST))))
        :hints (("goal" :expand ((:free (a b) (,FTY::X.FIX (cons a b)))))))
      ,@(AND (NOT (EQ FTY::X.STRATEGY :FIX-KEYS)) (NOT FTY::X.UNIQUE-KEYS)
       `((FTY::DEFTHM
          ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
            (FTY::CAT "HONS-ASSOC-EQUAL-OF-" (SYMBOL-NAME FTY::X.FIX))
            FTY::X.FIX)
          (EQUAL (FTY::HONS-ASSOC-EQUAL FTY::K (,FTY::X.FIX FTY::X))
                 (LET ((FTY::PAIR (FTY::HONS-ASSOC-EQUAL FTY::K FTY::X)))
                   (AND ,@(AND FTY::X.KEY-FIX `((,FTY::X.KEY-TYPE FTY::K)))
                        FTY::PAIR
                        (CONS FTY::K
                              ,(IF FTY::X.VAL-FIX
                                   `(,FTY::X.VAL-FIX (CDR FTY::PAIR))
                                   `(CDR FTY::PAIR))))))
          :HINTS
          (("goal" :INDUCT (FTY::LEN FTY::X) :IN-THEORY
            (FTY::ENABLE (:I FTY::LEN)) :EXPAND
            ((,FTY::X.FIX FTY::X) (FTY::HONS-ASSOC-EQUAL FTY::K FTY::X)
             (:FREE (FTY::A FTY::B)
              (FTY::HONS-ASSOC-EQUAL FTY::K (CONS FTY::A FTY::B)))))))))
      ,@(AND (NOT FTY::X.UNIQUE-KEYS)
       `((FTY::DEFTHM
          ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
            (FTY::CAT (SYMBOL-NAME FTY::X.FIX) "-OF-APPEND") FTY::X.FIX)
          (EQUAL (,FTY::X.FIX (APPEND STD::A STD::B))
                 (APPEND (,FTY::X.FIX STD::A) (,FTY::X.FIX STD::B)))
          :HINTS
          (("goal" :INDUCT (APPEND STD::A STD::B) :EXPAND
            ((,FTY::X.FIX STD::A)
             (:FREE (FTY::A FTY::B) (,FTY::X.FIX (CONS FTY::A FTY::B)))
             (,FTY::X.FIX NIL) (:FREE (FTY::B) (APPEND STD::A FTY::B))
             (:FREE (FTY::B) (APPEND NIL FTY::B))
             (:FREE (FTY::A FTY::B FTY::C)
              (APPEND (CONS FTY::A FTY::B) FTY::C)))
            :IN-THEORY (FTY::ENABLE (:I APPEND)))))))
      (defthm ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
  (FTY::CAT "CONSP-CAR-OF-" (SYMBOL-NAME FTY::X.FIX)) FTY::X.FIX)
        (equal (consp (car (,FTY::X.FIX ,FTY::X.XVAR)))
          (consp (,FTY::X.FIX ,FTY::X.XVAR)))
        :hints (("goal" :induct (len ,FTY::X.XVAR)
           :expand ((,FTY::X.FIX ,FTY::X.XVAR))
           :in-theory (e/d ((:i len)) ((:d ,FTY::X.FIX)))))))))

(define flexalist-fix-when-pred-thm
  (x flagp)
  (b* (((flexalist x) x) (foo-fix-when-foo-p (intern-in-package-of-symbol (cat (symbol-name x.fix)
            "-WHEN-"
            (symbol-name x.pred))
          x.fix)))
    `(defthm ,FTY::FOO-FIX-WHEN-FOO-P
      (implies (,FTY::X.PRED ,FTY::X.XVAR)
        (equal (,FTY::X.FIX ,FTY::X.XVAR) ,FTY::X.XVAR))
      :hints ('(:expand ((,FTY::X.PRED ,FTY::X.XVAR) (,FTY::X.FIX ,FTY::X.XVAR))
         :in-theory (disable ,FTY::X.FIX ,FTY::X.PRED))) . ,(AND FTY::FLAGP `(:FLAG ,FTY::X.NAME)))))

(defun flexalist-count
  (x types)
  (b* (((flexalist x)) ((unless x.count) nil)
      (keycount (flextypes-find-count-for-pred x.key-type
          types))
      (valcount (flextypes-find-count-for-pred x.val-type
          types)))
    `((define ,FTY::X.COUNT
       ((,FTY::X.XVAR ,FTY::X.PRED))
       :returns (count natp
         :rule-classes :type-prescription :hints ('(:expand (,FTY::X.COUNT ,FTY::X.XVAR)
            :in-theory (disable ,FTY::X.COUNT))))
       :measure (let ((,FTY::X.XVAR (,FTY::X.FIX ,FTY::X.XVAR)))
         ,FTY::X.MEASURE)
       ,@(AND (FTY::GETARG :MEASURE-DEBUG NIL FTY::X.KWD-ALIST) `(:MEASURE-DEBUG T))
       :verify-guards nil
       :progn t
       (let ((,FTY::X.XVAR (mbe :logic (,FTY::X.FIX ,FTY::X.XVAR)
              :exec ,FTY::X.XVAR)))
         (if (atom ,FTY::X.XVAR)
           1
           (+ 1
             ,@(AND (OR FTY::KEYCOUNT FTY::VALCOUNT)
       (IF FTY::KEYCOUNT
           (IF FTY::VALCOUNT
               `((+ (,FTY::KEYCOUNT (CAAR ,FTY::X.XVAR))
                    (,FTY::VALCOUNT (CDAR ,FTY::X.XVAR))))
               `((,FTY::KEYCOUNT (CAAR ,FTY::X.XVAR))))
           `((,FTY::VALCOUNT (CDAR ,FTY::X.XVAR)))))
             (,FTY::X.COUNT (cdr ,FTY::X.XVAR)))))))))

(defun flexalist-count-post-events
  (x types)
  (b* (((flexalist x)) ((unless x.count) nil)
      (keycount (flextypes-find-count-for-pred x.key-type
          types))
      (valcount (flextypes-find-count-for-pred x.val-type
          types))
      (foo-count-of-cons (intern-in-package-of-symbol (cat (symbol-name x.count) "-OF-CONS")
          x.count))
      (foo-count-of-acons (intern-in-package-of-symbol (cat (symbol-name x.count) "-OF-ACONS")
          x.count)))
    `((defthm ,FTY::FOO-COUNT-OF-CONS
       (>= (,FTY::X.COUNT (cons a b))
         (,FTY::X.COUNT b))
       :hints (("goal" :expand ((:free (a b) (,FTY::X.COUNT (cons a b))) (,FTY::X.FIX (cons a b)))) (and stable-under-simplificationp
           '(:expand ((,FTY::X.COUNT b)))))
       :rule-classes :linear) ,@(AND (OR FTY::KEYCOUNT FTY::VALCOUNT)
       `((FTY::DEFTHM ,FTY::FOO-COUNT-OF-ACONS
          ,(IF (AND (OR (EQ FTY::X.STRATEGY :FIX-KEYS) (NOT FTY::X.KEY-FIX))
                    (NOT FTY::X.UNIQUE-KEYS))
               `(> (,FTY::X.COUNT (CONS (CONS FTY::A FTY::B) FTY::C))
                   (+
                    ,@(IF FTY::KEYCOUNT
                          (IF FTY::VALCOUNT
                              `((,FTY::KEYCOUNT FTY::A)
                                (,FTY::VALCOUNT FTY::B))
                              `((,FTY::KEYCOUNT FTY::A)))
                          `((,FTY::VALCOUNT FTY::B)))
                    (,FTY::X.COUNT FTY::C)))
               `(FTY::IMPLIES
                 (AND
                  ,@(AND FTY::X.KEY-TYPE (NOT (EQ FTY::X.STRATEGY :FIX-KEYS))
                         `((,FTY::X.KEY-TYPE FTY::A)))
                  ,@(AND FTY::X.UNIQUE-KEYS
                         `((NOT
                            (FTY::HONS-ASSOC-EQUAL
                             ,(IF (AND FTY::X.KEY-TYPE
                                       (EQ FTY::X.STRATEGY :FIX-KEYS))
                                  `(,FTY::X.KEY-FIX FTY::A)
                                  'FTY::A)
                             (,FTY::X.FIX FTY::C))))))
                 (> (,FTY::X.COUNT (CONS (CONS FTY::A FTY::B) FTY::C))
                    (+
                     ,@(IF FTY::KEYCOUNT
                           (IF FTY::VALCOUNT
                               `((,FTY::KEYCOUNT FTY::A)
                                 (,FTY::VALCOUNT FTY::B))
                               `((,FTY::KEYCOUNT FTY::A)))
                           `((,FTY::VALCOUNT FTY::B)))
                     (,FTY::X.COUNT FTY::C)))))
          :HINTS
          (("goal" :EXPAND
            ((:FREE (FTY::A FTY::B) (,FTY::X.COUNT (CONS FTY::A FTY::B))))))
          :RULE-CLASSES :LINEAR)))
      ,@(AND FTY::KEYCOUNT
       `((FTY::DEFTHM
          ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
            (FTY::CAT (SYMBOL-NAME FTY::KEYCOUNT) "-OF-CAAR-"
             (SYMBOL-NAME FTY::X.COUNT))
            FTY::X.COUNT)
          (FTY::IMPLIES
           (AND (CONSP ,FTY::X.XVAR)
                (OR (CONSP (CAR ,FTY::X.XVAR)) (,FTY::X.PRED ,FTY::X.XVAR))
                ,@(AND (NOT (EQ FTY::X.STRATEGY :FIX-KEYS))
                       `((,FTY::X.KEY-TYPE (CAAR ,FTY::X.XVAR)))))
           (< (,FTY::KEYCOUNT (CAAR ,FTY::X.XVAR))
              (,FTY::X.COUNT ,FTY::X.XVAR)))
          :RULE-CLASSES :LINEAR)))
      ,@(AND FTY::VALCOUNT
       `((FTY::DEFTHM
          ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
            (FTY::CAT (SYMBOL-NAME FTY::VALCOUNT) "-OF-CDAR-"
             (SYMBOL-NAME FTY::X.COUNT))
            FTY::X.COUNT)
          (FTY::IMPLIES
           (AND (CONSP ,FTY::X.XVAR)
                (OR (CONSP (CAR ,FTY::X.XVAR)) (,FTY::X.PRED ,FTY::X.XVAR))
                ,@(AND (NOT (EQ FTY::X.STRATEGY :FIX-KEYS)) FTY::X.KEY-FIX
                       `((,FTY::X.KEY-TYPE (CAAR ,FTY::X.XVAR))))
                ,@(AND FTY::X.UNIQUE-KEYS
                       `((NOT
                          (FTY::HONS-ASSOC-EQUAL
                           ,(IF (AND FTY::X.KEY-FIX
                                     (EQ FTY::X.STRATEGY :FIX-KEYS))
                                `(,FTY::X.KEY-FIX (CAAR ,FTY::X.XVAR))
                                `(CAAR ,FTY::X.XVAR))
                           (,FTY::X.FIX (CDR ,FTY::X.XVAR)))))))
           (< (,FTY::VALCOUNT (CDAR ,FTY::X.XVAR))
              (,FTY::X.COUNT ,FTY::X.XVAR)))
          :RULE-CLASSES :LINEAR)))
      (defthm ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
  (FTY::CAT (SYMBOL-NAME FTY::X.COUNT) "-OF-CDR") FTY::X.COUNT)
        (<= (,FTY::X.COUNT (cdr ,FTY::X.XVAR))
          (,FTY::X.COUNT ,FTY::X.XVAR))
        :hints (("goal" :expand ((,FTY::X.FIX ,FTY::X.XVAR) (,FTY::X.COUNT ,FTY::X.XVAR)
             (,FTY::X.COUNT (cdr ,FTY::X.XVAR))
             (:free (a b) (,FTY::X.COUNT (cons a b))))
           :in-theory (enable default-cdr)))
        :rule-classes :linear)
      (defthm ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
  (FTY::CAT (SYMBOL-NAME FTY::X.COUNT) "-OF-CDR-STRONG") FTY::X.COUNT)
        (implies (and (,FTY::X.PRED ,FTY::X.XVAR) (consp ,FTY::X.XVAR))
          (< (,FTY::X.COUNT (cdr ,FTY::X.XVAR))
            (,FTY::X.COUNT ,FTY::X.XVAR)))
        :hints (("goal" :expand ((,FTY::X.FIX ,FTY::X.XVAR) (,FTY::X.COUNT ,FTY::X.XVAR)
             (,FTY::X.COUNT (cdr ,FTY::X.XVAR))
             (:free (a b) (,FTY::X.COUNT (cons a b))))
           :in-theory (enable default-cdr)))
        :rule-classes :linear))))