• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
        • Preprocessor
        • Vl-loadconfig
        • Vl-loadstate
        • Lexer
        • Parser
        • Vl-load-merge-descriptions
        • Vl-find-basename/extension
        • Vl-load-file
        • Vl-loadresult
        • Scope-of-defines
        • Vl-find-file
        • Vl-flush-out-descriptions
        • Vl-description
          • Vl-description-p
          • Vl-sort-descriptions
          • Vl-description-fix
          • Vl-find-description
          • Vl-description-equiv
          • Vl-description->origname
          • Vl-description->name
          • Vl-design-from-descriptions
          • Vl-make-descalist
          • Vl-design-descriptions
          • Vl-fast-filter-descriptions
          • Vl-fast-find-description
          • Vl-descalist
          • Vl-slow-delete-descriptions
        • Vl-read-file
        • Vl-includeskips-report-gather
        • Vl-load-main
        • Extended-characters
        • Vl-load
        • Vl-load-description
        • Vl-descriptions-left-to-load
        • Inject-warnings
        • Vl-preprocess-debug
        • Vl-write-preprocessor-debug-file
        • Vl-read-file-report-gather
        • Vl-load-descriptions
        • Vl-load-files
        • Translate-off
        • Vl-load-read-file-hook
        • Vl-read-file-report
        • Vl-loadstate-pad
        • Vl-load-summary
        • Vl-collect-modules-from-descriptions
        • Vl-loadstate->warnings
        • Vl-iskips-report
        • Vl-descriptionlist
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-description

Vl-sort-descriptions

Signature

(vl-sort-descriptions x &key modules udps interfaces 
                      programs classes packages configs 
                      vardecls taskdecls fundecls paramdecls 
                      imports fwdtypedefs typedefs dpiimports 
                      dpiexports binds properties sequences) 
 
  → 
(mv modules udps interfaces 
    programs classes packages configs 
    vardecls taskdecls fundecls paramdecls 
    imports fwdtypedefs typedefs dpiimports 
    dpiexports binds properties sequences) 

Arguments

x — Guard (vl-descriptionlist-p x).

modules — Guard (vl-modulelist-p modules).

udps — Guard (vl-udplist-p udps).

interfaces — Guard (vl-interfacelist-p interfaces).

programs — Guard (vl-programlist-p programs).

classes — Guard (vl-classlist-p classes).

packages — Guard (vl-packagelist-p packages).

configs — Guard (vl-configlist-p configs).

vardecls — Guard (vl-vardecllist-p vardecls).

taskdecls — Guard (vl-taskdecllist-p taskdecls).

fundecls — Guard (vl-fundecllist-p fundecls).

paramdecls — Guard (vl-paramdecllist-p paramdecls).

imports — Guard (vl-importlist-p imports).

fwdtypedefs — Guard (vl-fwdtypedeflist-p fwdtypedefs).

typedefs — Guard (vl-typedeflist-p typedefs).

dpiimports — Guard (vl-dpiimportlist-p dpiimports).

dpiexports — Guard (vl-dpiexportlist-p dpiexports).

binds — Guard (vl-bindlist-p binds).

properties — Guard (vl-propertylist-p properties).

sequences — Guard (vl-sequencelist-p sequences).

Returns

modules — Type (vl-modulelist-p modules).

udps — Type (vl-udplist-p udps).

interfaces — Type (vl-interfacelist-p interfaces).

programs — Type (vl-programlist-p programs).

classes — Type (vl-classlist-p classes).

packages — Type (vl-packagelist-p packages).

configs — Type (vl-configlist-p configs).

vardecls — Type (vl-vardecllist-p vardecls).

taskdecls — Type (vl-taskdecllist-p taskdecls).

fundecls — Type (vl-fundecllist-p fundecls).

paramdecls — Type (vl-paramdecllist-p paramdecls).

imports — Type (vl-importlist-p imports).

fwdtypedefs — Type (vl-fwdtypedeflist-p fwdtypedefs).

typedefs — Type (vl-typedeflist-p typedefs).

dpiimports — Type (vl-dpiimportlist-p dpiimports).

dpiexports — Type (vl-dpiexportlist-p dpiexports).

binds — Type (vl-bindlist-p binds).

properties — Type (vl-propertylist-p properties).

sequences — Type (vl-sequencelist-p sequences).

Definitions and Theorems

Function: vl-sort-descriptions-fn

(defun vl-sort-descriptions-fn
       (x modules udps interfaces
          programs classes packages configs
          vardecls taskdecls fundecls paramdecls
          imports fwdtypedefs typedefs dpiimports
          dpiexports binds properties sequences)
  (declare (xargs :guard (and (vl-descriptionlist-p x)
                              (vl-modulelist-p modules)
                              (vl-udplist-p udps)
                              (vl-interfacelist-p interfaces)
                              (vl-programlist-p programs)
                              (vl-classlist-p classes)
                              (vl-packagelist-p packages)
                              (vl-configlist-p configs)
                              (vl-vardecllist-p vardecls)
                              (vl-taskdecllist-p taskdecls)
                              (vl-fundecllist-p fundecls)
                              (vl-paramdecllist-p paramdecls)
                              (vl-importlist-p imports)
                              (vl-fwdtypedeflist-p fwdtypedefs)
                              (vl-typedeflist-p typedefs)
                              (vl-dpiimportlist-p dpiimports)
                              (vl-dpiexportlist-p dpiexports)
                              (vl-bindlist-p binds)
                              (vl-propertylist-p properties)
                              (vl-sequencelist-p sequences))))
  (let ((__function__ 'vl-sort-descriptions))
    (declare (ignorable __function__))
    (b* (((when (atom x))
          (mv (vl-modulelist-fix modules)
              (vl-udplist-fix udps)
              (vl-interfacelist-fix interfaces)
              (vl-programlist-fix programs)
              (vl-classlist-fix classes)
              (vl-packagelist-fix packages)
              (vl-configlist-fix configs)
              (vl-vardecllist-fix vardecls)
              (vl-taskdecllist-fix taskdecls)
              (vl-fundecllist-fix fundecls)
              (vl-paramdecllist-fix paramdecls)
              (vl-importlist-fix imports)
              (vl-fwdtypedeflist-fix fwdtypedefs)
              (vl-typedeflist-fix typedefs)
              (vl-dpiimportlist-fix dpiimports)
              (vl-dpiexportlist-fix dpiexports)
              (vl-bindlist-fix binds)
              (vl-propertylist-fix properties)
              (vl-sequencelist-fix sequences)))
         (x1 (vl-description-fix (car x)))
         (tag (tag x1)))
      (vl-sort-descriptions (cdr x)
                            :modules
                            (if (eq tag :vl-module)
                                (cons x1 modules)
                              modules)
                            :udps
                            (if (eq tag :vl-udp)
                                (cons x1 udps)
                              udps)
                            :interfaces
                            (if (eq tag :vl-interface)
                                (cons x1 interfaces)
                              interfaces)
                            :programs
                            (if (eq tag :vl-program)
                                (cons x1 programs)
                              programs)
                            :classes
                            (if (eq tag :vl-class)
                                (cons x1 classes)
                              classes)
                            :packages
                            (if (eq tag :vl-package)
                                (cons x1 packages)
                              packages)
                            :configs
                            (if (eq tag :vl-config)
                                (cons x1 configs)
                              configs)
                            :vardecls
                            (if (eq tag :vl-vardecl)
                                (cons x1 vardecls)
                              vardecls)
                            :taskdecls
                            (if (eq tag :vl-taskdecl)
                                (cons x1 taskdecls)
                              taskdecls)
                            :fundecls
                            (if (eq tag :vl-fundecl)
                                (cons x1 fundecls)
                              fundecls)
                            :paramdecls
                            (if (eq tag :vl-paramdecl)
                                (cons x1 paramdecls)
                              paramdecls)
                            :imports
                            (if (eq tag :vl-import)
                                (cons x1 imports)
                              imports)
                            :fwdtypedefs
                            (if (eq tag :vl-fwdtypedef)
                                (cons x1 fwdtypedefs)
                              fwdtypedefs)
                            :typedefs
                            (if (eq tag :vl-typedef)
                                (cons x1 typedefs)
                              typedefs)
                            :dpiimports
                            (if (eq tag :vl-dpiimport)
                                (cons x1 dpiimports)
                              dpiimports)
                            :dpiexports
                            (if (eq tag :vl-dpiexport)
                                (cons x1 dpiexports)
                              dpiexports)
                            :binds
                            (if (eq tag :vl-bind)
                                (cons x1 binds)
                              binds)
                            :properties
                            (if (eq tag :vl-property)
                                (cons x1 properties)
                              properties)
                            :sequences
                            (if (eq tag :vl-sequence)
                                (cons x1 sequences)
                              sequences)))))

Theorem: vl-modulelist-p-of-vl-sort-descriptions.modules

(defthm vl-modulelist-p-of-vl-sort-descriptions.modules
  (b* (((mv ?modules ?udps
            ?interfaces ?programs ?classes ?packages
            ?configs ?vardecls ?taskdecls ?fundecls
            ?paramdecls ?imports ?fwdtypedefs
            ?typedefs ?dpiimports ?dpiexports
            ?binds ?properties ?sequences)
        (vl-sort-descriptions-fn
             x modules udps interfaces
             programs classes packages configs
             vardecls taskdecls fundecls paramdecls
             imports fwdtypedefs typedefs dpiimports
             dpiexports binds properties sequences)))
    (vl-modulelist-p modules))
  :rule-classes :rewrite)

Theorem: vl-udplist-p-of-vl-sort-descriptions.udps

(defthm vl-udplist-p-of-vl-sort-descriptions.udps
  (b* (((mv ?modules ?udps
            ?interfaces ?programs ?classes ?packages
            ?configs ?vardecls ?taskdecls ?fundecls
            ?paramdecls ?imports ?fwdtypedefs
            ?typedefs ?dpiimports ?dpiexports
            ?binds ?properties ?sequences)
        (vl-sort-descriptions-fn
             x modules udps interfaces
             programs classes packages configs
             vardecls taskdecls fundecls paramdecls
             imports fwdtypedefs typedefs dpiimports
             dpiexports binds properties sequences)))
    (vl-udplist-p udps))
  :rule-classes :rewrite)

Theorem: vl-interfacelist-p-of-vl-sort-descriptions.interfaces

(defthm vl-interfacelist-p-of-vl-sort-descriptions.interfaces
  (b* (((mv ?modules ?udps
            ?interfaces ?programs ?classes ?packages
            ?configs ?vardecls ?taskdecls ?fundecls
            ?paramdecls ?imports ?fwdtypedefs
            ?typedefs ?dpiimports ?dpiexports
            ?binds ?properties ?sequences)
        (vl-sort-descriptions-fn
             x modules udps interfaces
             programs classes packages configs
             vardecls taskdecls fundecls paramdecls
             imports fwdtypedefs typedefs dpiimports
             dpiexports binds properties sequences)))
    (vl-interfacelist-p interfaces))
  :rule-classes :rewrite)

Theorem: vl-programlist-p-of-vl-sort-descriptions.programs

(defthm vl-programlist-p-of-vl-sort-descriptions.programs
  (b* (((mv ?modules ?udps
            ?interfaces ?programs ?classes ?packages
            ?configs ?vardecls ?taskdecls ?fundecls
            ?paramdecls ?imports ?fwdtypedefs
            ?typedefs ?dpiimports ?dpiexports
            ?binds ?properties ?sequences)
        (vl-sort-descriptions-fn
             x modules udps interfaces
             programs classes packages configs
             vardecls taskdecls fundecls paramdecls
             imports fwdtypedefs typedefs dpiimports
             dpiexports binds properties sequences)))
    (vl-programlist-p programs))
  :rule-classes :rewrite)

Theorem: vl-classlist-p-of-vl-sort-descriptions.classes

(defthm vl-classlist-p-of-vl-sort-descriptions.classes
  (b* (((mv ?modules ?udps
            ?interfaces ?programs ?classes ?packages
            ?configs ?vardecls ?taskdecls ?fundecls
            ?paramdecls ?imports ?fwdtypedefs
            ?typedefs ?dpiimports ?dpiexports
            ?binds ?properties ?sequences)
        (vl-sort-descriptions-fn
             x modules udps interfaces
             programs classes packages configs
             vardecls taskdecls fundecls paramdecls
             imports fwdtypedefs typedefs dpiimports
             dpiexports binds properties sequences)))
    (vl-classlist-p classes))
  :rule-classes :rewrite)

Theorem: vl-packagelist-p-of-vl-sort-descriptions.packages

(defthm vl-packagelist-p-of-vl-sort-descriptions.packages
  (b* (((mv ?modules ?udps
            ?interfaces ?programs ?classes ?packages
            ?configs ?vardecls ?taskdecls ?fundecls
            ?paramdecls ?imports ?fwdtypedefs
            ?typedefs ?dpiimports ?dpiexports
            ?binds ?properties ?sequences)
        (vl-sort-descriptions-fn
             x modules udps interfaces
             programs classes packages configs
             vardecls taskdecls fundecls paramdecls
             imports fwdtypedefs typedefs dpiimports
             dpiexports binds properties sequences)))
    (vl-packagelist-p packages))
  :rule-classes :rewrite)

Theorem: vl-configlist-p-of-vl-sort-descriptions.configs

(defthm vl-configlist-p-of-vl-sort-descriptions.configs
  (b* (((mv ?modules ?udps
            ?interfaces ?programs ?classes ?packages
            ?configs ?vardecls ?taskdecls ?fundecls
            ?paramdecls ?imports ?fwdtypedefs
            ?typedefs ?dpiimports ?dpiexports
            ?binds ?properties ?sequences)
        (vl-sort-descriptions-fn
             x modules udps interfaces
             programs classes packages configs
             vardecls taskdecls fundecls paramdecls
             imports fwdtypedefs typedefs dpiimports
             dpiexports binds properties sequences)))
    (vl-configlist-p configs))
  :rule-classes :rewrite)

Theorem: vl-vardecllist-p-of-vl-sort-descriptions.vardecls

(defthm vl-vardecllist-p-of-vl-sort-descriptions.vardecls
  (b* (((mv ?modules ?udps
            ?interfaces ?programs ?classes ?packages
            ?configs ?vardecls ?taskdecls ?fundecls
            ?paramdecls ?imports ?fwdtypedefs
            ?typedefs ?dpiimports ?dpiexports
            ?binds ?properties ?sequences)
        (vl-sort-descriptions-fn
             x modules udps interfaces
             programs classes packages configs
             vardecls taskdecls fundecls paramdecls
             imports fwdtypedefs typedefs dpiimports
             dpiexports binds properties sequences)))
    (vl-vardecllist-p vardecls))
  :rule-classes :rewrite)

Theorem: vl-taskdecllist-p-of-vl-sort-descriptions.taskdecls

(defthm vl-taskdecllist-p-of-vl-sort-descriptions.taskdecls
  (b* (((mv ?modules ?udps
            ?interfaces ?programs ?classes ?packages
            ?configs ?vardecls ?taskdecls ?fundecls
            ?paramdecls ?imports ?fwdtypedefs
            ?typedefs ?dpiimports ?dpiexports
            ?binds ?properties ?sequences)
        (vl-sort-descriptions-fn
             x modules udps interfaces
             programs classes packages configs
             vardecls taskdecls fundecls paramdecls
             imports fwdtypedefs typedefs dpiimports
             dpiexports binds properties sequences)))
    (vl-taskdecllist-p taskdecls))
  :rule-classes :rewrite)

Theorem: vl-fundecllist-p-of-vl-sort-descriptions.fundecls

(defthm vl-fundecllist-p-of-vl-sort-descriptions.fundecls
  (b* (((mv ?modules ?udps
            ?interfaces ?programs ?classes ?packages
            ?configs ?vardecls ?taskdecls ?fundecls
            ?paramdecls ?imports ?fwdtypedefs
            ?typedefs ?dpiimports ?dpiexports
            ?binds ?properties ?sequences)
        (vl-sort-descriptions-fn
             x modules udps interfaces
             programs classes packages configs
             vardecls taskdecls fundecls paramdecls
             imports fwdtypedefs typedefs dpiimports
             dpiexports binds properties sequences)))
    (vl-fundecllist-p fundecls))
  :rule-classes :rewrite)

Theorem: vl-paramdecllist-p-of-vl-sort-descriptions.paramdecls

(defthm vl-paramdecllist-p-of-vl-sort-descriptions.paramdecls
  (b* (((mv ?modules ?udps
            ?interfaces ?programs ?classes ?packages
            ?configs ?vardecls ?taskdecls ?fundecls
            ?paramdecls ?imports ?fwdtypedefs
            ?typedefs ?dpiimports ?dpiexports
            ?binds ?properties ?sequences)
        (vl-sort-descriptions-fn
             x modules udps interfaces
             programs classes packages configs
             vardecls taskdecls fundecls paramdecls
             imports fwdtypedefs typedefs dpiimports
             dpiexports binds properties sequences)))
    (vl-paramdecllist-p paramdecls))
  :rule-classes :rewrite)

Theorem: vl-importlist-p-of-vl-sort-descriptions.imports

(defthm vl-importlist-p-of-vl-sort-descriptions.imports
  (b* (((mv ?modules ?udps
            ?interfaces ?programs ?classes ?packages
            ?configs ?vardecls ?taskdecls ?fundecls
            ?paramdecls ?imports ?fwdtypedefs
            ?typedefs ?dpiimports ?dpiexports
            ?binds ?properties ?sequences)
        (vl-sort-descriptions-fn
             x modules udps interfaces
             programs classes packages configs
             vardecls taskdecls fundecls paramdecls
             imports fwdtypedefs typedefs dpiimports
             dpiexports binds properties sequences)))
    (vl-importlist-p imports))
  :rule-classes :rewrite)

Theorem: vl-fwdtypedeflist-p-of-vl-sort-descriptions.fwdtypedefs

(defthm vl-fwdtypedeflist-p-of-vl-sort-descriptions.fwdtypedefs
  (b* (((mv ?modules ?udps
            ?interfaces ?programs ?classes ?packages
            ?configs ?vardecls ?taskdecls ?fundecls
            ?paramdecls ?imports ?fwdtypedefs
            ?typedefs ?dpiimports ?dpiexports
            ?binds ?properties ?sequences)
        (vl-sort-descriptions-fn
             x modules udps interfaces
             programs classes packages configs
             vardecls taskdecls fundecls paramdecls
             imports fwdtypedefs typedefs dpiimports
             dpiexports binds properties sequences)))
    (vl-fwdtypedeflist-p fwdtypedefs))
  :rule-classes :rewrite)

Theorem: vl-typedeflist-p-of-vl-sort-descriptions.typedefs

(defthm vl-typedeflist-p-of-vl-sort-descriptions.typedefs
  (b* (((mv ?modules ?udps
            ?interfaces ?programs ?classes ?packages
            ?configs ?vardecls ?taskdecls ?fundecls
            ?paramdecls ?imports ?fwdtypedefs
            ?typedefs ?dpiimports ?dpiexports
            ?binds ?properties ?sequences)
        (vl-sort-descriptions-fn
             x modules udps interfaces
             programs classes packages configs
             vardecls taskdecls fundecls paramdecls
             imports fwdtypedefs typedefs dpiimports
             dpiexports binds properties sequences)))
    (vl-typedeflist-p typedefs))
  :rule-classes :rewrite)

Theorem: vl-dpiimportlist-p-of-vl-sort-descriptions.dpiimports

(defthm vl-dpiimportlist-p-of-vl-sort-descriptions.dpiimports
  (b* (((mv ?modules ?udps
            ?interfaces ?programs ?classes ?packages
            ?configs ?vardecls ?taskdecls ?fundecls
            ?paramdecls ?imports ?fwdtypedefs
            ?typedefs ?dpiimports ?dpiexports
            ?binds ?properties ?sequences)
        (vl-sort-descriptions-fn
             x modules udps interfaces
             programs classes packages configs
             vardecls taskdecls fundecls paramdecls
             imports fwdtypedefs typedefs dpiimports
             dpiexports binds properties sequences)))
    (vl-dpiimportlist-p dpiimports))
  :rule-classes :rewrite)

Theorem: vl-dpiexportlist-p-of-vl-sort-descriptions.dpiexports

(defthm vl-dpiexportlist-p-of-vl-sort-descriptions.dpiexports
  (b* (((mv ?modules ?udps
            ?interfaces ?programs ?classes ?packages
            ?configs ?vardecls ?taskdecls ?fundecls
            ?paramdecls ?imports ?fwdtypedefs
            ?typedefs ?dpiimports ?dpiexports
            ?binds ?properties ?sequences)
        (vl-sort-descriptions-fn
             x modules udps interfaces
             programs classes packages configs
             vardecls taskdecls fundecls paramdecls
             imports fwdtypedefs typedefs dpiimports
             dpiexports binds properties sequences)))
    (vl-dpiexportlist-p dpiexports))
  :rule-classes :rewrite)

Theorem: vl-bindlist-p-of-vl-sort-descriptions.binds

(defthm vl-bindlist-p-of-vl-sort-descriptions.binds
  (b* (((mv ?modules ?udps
            ?interfaces ?programs ?classes ?packages
            ?configs ?vardecls ?taskdecls ?fundecls
            ?paramdecls ?imports ?fwdtypedefs
            ?typedefs ?dpiimports ?dpiexports
            ?binds ?properties ?sequences)
        (vl-sort-descriptions-fn
             x modules udps interfaces
             programs classes packages configs
             vardecls taskdecls fundecls paramdecls
             imports fwdtypedefs typedefs dpiimports
             dpiexports binds properties sequences)))
    (vl-bindlist-p binds))
  :rule-classes :rewrite)

Theorem: vl-propertylist-p-of-vl-sort-descriptions.properties

(defthm vl-propertylist-p-of-vl-sort-descriptions.properties
  (b* (((mv ?modules ?udps
            ?interfaces ?programs ?classes ?packages
            ?configs ?vardecls ?taskdecls ?fundecls
            ?paramdecls ?imports ?fwdtypedefs
            ?typedefs ?dpiimports ?dpiexports
            ?binds ?properties ?sequences)
        (vl-sort-descriptions-fn
             x modules udps interfaces
             programs classes packages configs
             vardecls taskdecls fundecls paramdecls
             imports fwdtypedefs typedefs dpiimports
             dpiexports binds properties sequences)))
    (vl-propertylist-p properties))
  :rule-classes :rewrite)

Theorem: vl-sequencelist-p-of-vl-sort-descriptions.sequences

(defthm vl-sequencelist-p-of-vl-sort-descriptions.sequences
  (b* (((mv ?modules ?udps
            ?interfaces ?programs ?classes ?packages
            ?configs ?vardecls ?taskdecls ?fundecls
            ?paramdecls ?imports ?fwdtypedefs
            ?typedefs ?dpiimports ?dpiexports
            ?binds ?properties ?sequences)
        (vl-sort-descriptions-fn
             x modules udps interfaces
             programs classes packages configs
             vardecls taskdecls fundecls paramdecls
             imports fwdtypedefs typedefs dpiimports
             dpiexports binds properties sequences)))
    (vl-sequencelist-p sequences))
  :rule-classes :rewrite)

Theorem: vl-sort-descriptions-fn-of-vl-descriptionlist-fix-x

(defthm vl-sort-descriptions-fn-of-vl-descriptionlist-fix-x
 (equal
   (vl-sort-descriptions-fn (vl-descriptionlist-fix x)
                            modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))

Theorem: vl-sort-descriptions-fn-vl-descriptionlist-equiv-congruence-on-x

(defthm
   vl-sort-descriptions-fn-vl-descriptionlist-equiv-congruence-on-x
 (implies
  (vl-descriptionlist-equiv x x-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x-equiv modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-modulelist-fix-modules

(defthm vl-sort-descriptions-fn-of-vl-modulelist-fix-modules
 (equal
   (vl-sort-descriptions-fn x (vl-modulelist-fix modules)
                            udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))

Theorem: vl-sort-descriptions-fn-vl-modulelist-equiv-congruence-on-modules

(defthm
  vl-sort-descriptions-fn-vl-modulelist-equiv-congruence-on-modules
 (implies
  (vl-modulelist-equiv modules modules-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules-equiv udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-udplist-fix-udps

(defthm vl-sort-descriptions-fn-of-vl-udplist-fix-udps
 (equal
   (vl-sort-descriptions-fn x modules (vl-udplist-fix udps)
                            interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))

Theorem: vl-sort-descriptions-fn-vl-udplist-equiv-congruence-on-udps

(defthm vl-sort-descriptions-fn-vl-udplist-equiv-congruence-on-udps
 (implies
  (vl-udplist-equiv udps udps-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps-equiv interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-interfacelist-fix-interfaces

(defthm vl-sort-descriptions-fn-of-vl-interfacelist-fix-interfaces
 (equal
   (vl-sort-descriptions-fn x modules
                            udps (vl-interfacelist-fix interfaces)
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))

Theorem: vl-sort-descriptions-fn-vl-interfacelist-equiv-congruence-on-interfaces

(defthm
 vl-sort-descriptions-fn-vl-interfacelist-equiv-congruence-on-interfaces
 (implies
  (vl-interfacelist-equiv interfaces interfaces-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces-equiv
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-programlist-fix-programs

(defthm vl-sort-descriptions-fn-of-vl-programlist-fix-programs
 (equal
   (vl-sort-descriptions-fn x modules udps
                            interfaces (vl-programlist-fix programs)
                            classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))

Theorem: vl-sort-descriptions-fn-vl-programlist-equiv-congruence-on-programs

(defthm
 vl-sort-descriptions-fn-vl-programlist-equiv-congruence-on-programs
 (implies
  (vl-programlist-equiv programs programs-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs-equiv classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-classlist-fix-classes

(defthm vl-sort-descriptions-fn-of-vl-classlist-fix-classes
 (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs (vl-classlist-fix classes)
                            packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))

Theorem: vl-sort-descriptions-fn-vl-classlist-equiv-congruence-on-classes

(defthm
   vl-sort-descriptions-fn-vl-classlist-equiv-congruence-on-classes
 (implies
  (vl-classlist-equiv classes classes-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes-equiv packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-packagelist-fix-packages

(defthm vl-sort-descriptions-fn-of-vl-packagelist-fix-packages
 (equal
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            classes (vl-packagelist-fix packages)
                            configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))

Theorem: vl-sort-descriptions-fn-vl-packagelist-equiv-congruence-on-packages

(defthm
 vl-sort-descriptions-fn-vl-packagelist-equiv-congruence-on-packages
 (implies
  (vl-packagelist-equiv packages packages-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages-equiv configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-configlist-fix-configs

(defthm vl-sort-descriptions-fn-of-vl-configlist-fix-configs
 (equal
   (vl-sort-descriptions-fn x
                            modules udps interfaces programs classes
                            packages (vl-configlist-fix configs)
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))

Theorem: vl-sort-descriptions-fn-vl-configlist-equiv-congruence-on-configs

(defthm
  vl-sort-descriptions-fn-vl-configlist-equiv-congruence-on-configs
 (implies
  (vl-configlist-equiv configs configs-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs-equiv
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-vardecllist-fix-vardecls

(defthm vl-sort-descriptions-fn-of-vl-vardecllist-fix-vardecls
 (equal
   (vl-sort-descriptions-fn x modules udps
                            interfaces programs classes packages
                            configs (vl-vardecllist-fix vardecls)
                            taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))

Theorem: vl-sort-descriptions-fn-vl-vardecllist-equiv-congruence-on-vardecls

(defthm
 vl-sort-descriptions-fn-vl-vardecllist-equiv-congruence-on-vardecls
 (implies
  (vl-vardecllist-equiv vardecls vardecls-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            classes packages configs vardecls-equiv
                            taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-taskdecllist-fix-taskdecls

(defthm vl-sort-descriptions-fn-of-vl-taskdecllist-fix-taskdecls
 (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls (vl-taskdecllist-fix taskdecls)
                            fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))

Theorem: vl-sort-descriptions-fn-vl-taskdecllist-equiv-congruence-on-taskdecls

(defthm
 vl-sort-descriptions-fn-vl-taskdecllist-equiv-congruence-on-taskdecls
 (implies
  (vl-taskdecllist-equiv taskdecls taskdecls-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            classes packages configs vardecls
                            taskdecls-equiv fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-fundecllist-fix-fundecls

(defthm vl-sort-descriptions-fn-of-vl-fundecllist-fix-fundecls
 (equal
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            classes packages configs vardecls
                            taskdecls (vl-fundecllist-fix fundecls)
                            paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))

Theorem: vl-sort-descriptions-fn-vl-fundecllist-equiv-congruence-on-fundecls

(defthm
 vl-sort-descriptions-fn-vl-fundecllist-equiv-congruence-on-fundecls
 (implies
  (vl-fundecllist-equiv fundecls fundecls-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            classes packages configs vardecls
                            taskdecls fundecls-equiv paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-paramdecllist-fix-paramdecls

(defthm vl-sort-descriptions-fn-of-vl-paramdecllist-fix-paramdecls
 (equal
   (vl-sort-descriptions-fn x modules udps
                            interfaces programs classes packages
                            configs vardecls taskdecls fundecls
                            (vl-paramdecllist-fix paramdecls)
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))

Theorem: vl-sort-descriptions-fn-vl-paramdecllist-equiv-congruence-on-paramdecls

(defthm
 vl-sort-descriptions-fn-vl-paramdecllist-equiv-congruence-on-paramdecls
 (implies
  (vl-paramdecllist-equiv paramdecls paramdecls-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            classes packages configs vardecls
                            taskdecls fundecls paramdecls-equiv
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-importlist-fix-imports

(defthm vl-sort-descriptions-fn-of-vl-importlist-fix-imports
 (equal
   (vl-sort-descriptions-fn x modules udps
                            interfaces programs classes packages
                            configs vardecls taskdecls fundecls
                            paramdecls (vl-importlist-fix imports)
                            fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))

Theorem: vl-sort-descriptions-fn-vl-importlist-equiv-congruence-on-imports

(defthm
  vl-sort-descriptions-fn-vl-importlist-equiv-congruence-on-imports
 (implies
  (vl-importlist-equiv imports imports-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x
                            modules udps interfaces programs classes
                            packages configs vardecls taskdecls
                            fundecls paramdecls imports-equiv
                            fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-fwdtypedeflist-fix-fwdtypedefs

(defthm vl-sort-descriptions-fn-of-vl-fwdtypedeflist-fix-fwdtypedefs
 (equal
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            classes packages configs vardecls
                            taskdecls fundecls paramdecls imports
                            (vl-fwdtypedeflist-fix fwdtypedefs)
                            typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))

Theorem: vl-sort-descriptions-fn-vl-fwdtypedeflist-equiv-congruence-on-fwdtypedefs

(defthm
 vl-sort-descriptions-fn-vl-fwdtypedeflist-equiv-congruence-on-fwdtypedefs
 (implies
  (vl-fwdtypedeflist-equiv fwdtypedefs fwdtypedefs-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            classes packages configs vardecls
                            taskdecls fundecls paramdecls imports
                            fwdtypedefs-equiv typedefs dpiimports
                            dpiexports binds properties sequences)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-typedeflist-fix-typedefs

(defthm vl-sort-descriptions-fn-of-vl-typedeflist-fix-typedefs
 (equal
   (vl-sort-descriptions-fn x
                            modules udps interfaces programs classes
                            packages configs vardecls taskdecls
                            fundecls paramdecls imports fwdtypedefs
                            (vl-typedeflist-fix typedefs)
                            dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))

Theorem: vl-sort-descriptions-fn-vl-typedeflist-equiv-congruence-on-typedefs

(defthm
 vl-sort-descriptions-fn-vl-typedeflist-equiv-congruence-on-typedefs
 (implies
  (vl-typedeflist-equiv typedefs typedefs-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            classes packages configs vardecls
                            taskdecls fundecls paramdecls imports
                            fwdtypedefs typedefs-equiv dpiimports
                            dpiexports binds properties sequences)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-dpiimportlist-fix-dpiimports

(defthm vl-sort-descriptions-fn-of-vl-dpiimportlist-fix-dpiimports
 (equal
   (vl-sort-descriptions-fn x modules udps
                            interfaces programs classes packages
                            configs vardecls taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs
                            (vl-dpiimportlist-fix dpiimports)
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))

Theorem: vl-sort-descriptions-fn-vl-dpiimportlist-equiv-congruence-on-dpiimports

(defthm
 vl-sort-descriptions-fn-vl-dpiimportlist-equiv-congruence-on-dpiimports
 (implies
  (vl-dpiimportlist-equiv dpiimports dpiimports-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            classes packages configs vardecls
                            taskdecls fundecls paramdecls imports
                            fwdtypedefs typedefs dpiimports-equiv
                            dpiexports binds properties sequences)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-dpiexportlist-fix-dpiexports

(defthm vl-sort-descriptions-fn-of-vl-dpiexportlist-fix-dpiexports
 (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            (vl-dpiexportlist-fix dpiexports)
                            binds properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))

Theorem: vl-sort-descriptions-fn-vl-dpiexportlist-equiv-congruence-on-dpiexports

(defthm
 vl-sort-descriptions-fn-vl-dpiexportlist-equiv-congruence-on-dpiexports
 (implies
  (vl-dpiexportlist-equiv dpiexports dpiexports-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x
                            modules udps interfaces programs classes
                            packages configs vardecls taskdecls
                            fundecls paramdecls imports fwdtypedefs
                            typedefs dpiimports dpiexports-equiv
                            binds properties sequences)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-bindlist-fix-binds

(defthm vl-sort-descriptions-fn-of-vl-bindlist-fix-binds
 (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports (vl-bindlist-fix binds)
                            properties sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))

Theorem: vl-sort-descriptions-fn-vl-bindlist-equiv-congruence-on-binds

(defthm
      vl-sort-descriptions-fn-vl-bindlist-equiv-congruence-on-binds
 (implies
  (vl-bindlist-equiv binds binds-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x
                            modules udps interfaces programs classes
                            packages configs vardecls taskdecls
                            fundecls paramdecls imports fwdtypedefs
                            typedefs dpiimports dpiexports
                            binds-equiv properties sequences)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-propertylist-fix-properties

(defthm vl-sort-descriptions-fn-of-vl-propertylist-fix-properties
 (equal
   (vl-sort-descriptions-fn x
                            modules udps interfaces programs classes
                            packages configs vardecls taskdecls
                            fundecls paramdecls imports fwdtypedefs
                            typedefs dpiimports dpiexports
                            binds (vl-propertylist-fix properties)
                            sequences)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))

Theorem: vl-sort-descriptions-fn-vl-propertylist-equiv-congruence-on-properties

(defthm
 vl-sort-descriptions-fn-vl-propertylist-equiv-congruence-on-properties
 (implies
  (vl-propertylist-equiv properties properties-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x
                            modules udps interfaces programs classes
                            packages configs vardecls taskdecls
                            fundecls paramdecls imports fwdtypedefs
                            typedefs dpiimports dpiexports
                            binds properties-equiv sequences)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-sequencelist-fix-sequences

(defthm vl-sort-descriptions-fn-of-vl-sequencelist-fix-sequences
 (equal
   (vl-sort-descriptions-fn x modules udps
                            interfaces programs classes packages
                            configs vardecls taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs
                            dpiimports dpiexports binds properties
                            (vl-sequencelist-fix sequences))
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)))

Theorem: vl-sort-descriptions-fn-vl-sequencelist-equiv-congruence-on-sequences

(defthm
 vl-sort-descriptions-fn-vl-sequencelist-equiv-congruence-on-sequences
 (implies
  (vl-sequencelist-equiv sequences sequences-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs classes packages configs
                            vardecls taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs dpiimports
                            dpiexports binds properties sequences)
   (vl-sort-descriptions-fn x
                            modules udps interfaces programs classes
                            packages configs vardecls taskdecls
                            fundecls paramdecls imports fwdtypedefs
                            typedefs dpiimports dpiexports
                            binds properties sequences-equiv)))
 :rule-classes :congruence)