• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
      • Z3-installation
      • Smt-hint
      • Tutorial
      • Status
      • Developer
        • Verified
          • Uninterpreted-fn-cp
          • Smt-hint-interface
          • Function-expansion
          • Smt-config
          • Fty-support
          • Smt-computed-hints
          • Add-hypo-cp
          • Smt-hint-please
          • Type-extract-cp
          • Smt-extract
          • Smtlink-process-user-hint
            • Process-smtlink-hints
            • Function-syntax
              • Function-option-name-list
              • Function-option-syntax-p
              • Function-option-lst-syntax-p-helper
              • Function-option-lst-syntax-fix
              • Function-option-type-fix
              • Eval-function-option-type
              • Function-lst-syntax-fix
              • Function-syntax-p
              • Function-option-type-p
              • Function-option-lst-syntax-p
              • Function-lst-syntax-p
              • Function-syntax-fix
            • Smtlink-hint-syntax
            • Argument-lst-syntax
            • Hypothesis-lst-syntax
            • Translate-cmp-smtlink
            • Process-hint-clause-processor
            • Smt-solver-params
            • Hints-syntax
            • True-set-equiv-relation
          • Smt-basics
          • Smt-type-hyp
          • Smt-magic-fix
        • Trusted
    • Aleobft
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • C
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Riscv
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Bigmems
    • Builtins
    • Axe
    • Execloader
    • Solidity
    • Leo
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Smtlink-process-user-hint

Function-syntax

Definitions and Theorems

Function: function-option-type-p

(defun function-option-type-p (option-type)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'function-option-type-p))
    (declare (ignorable acl2::__function__))
    (if (member-equal option-type *function-option-types*)
        t
      nil)))

Theorem: booleanp-of-function-option-type-p

(defthm booleanp-of-function-option-type-p
  (b* ((syntax-good? (function-option-type-p option-type)))
    (booleanp syntax-good?))
  :rule-classes :rewrite)

Function: function-option-type-fix

(defun function-option-type-fix (option-type)
  (declare (xargs :guard (function-option-type-p option-type)))
  (let ((acl2::__function__ 'function-option-type-fix))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (if (function-option-type-p option-type)
             option-type
           'natp)
         :exec option-type)))

Theorem: function-option-type-p-of-function-option-type-fix

(defthm function-option-type-p-of-function-option-type-fix
  (b* ((fixed-option-type (function-option-type-fix option-type)))
    (function-option-type-p fixed-option-type))
  :rule-classes :rewrite)

Function: function-option-name-p

(defun function-option-name-p (option-name)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'function-option-name-p))
    (declare (ignorable acl2::__function__))
    (if (member-equal option-name *function-option-names*)
        t
      nil)))

Theorem: booleanp-of-function-option-name-p

(defthm booleanp-of-function-option-name-p
  (b* ((syntax-good? (function-option-name-p option-name)))
    (booleanp syntax-good?))
  :rule-classes :rewrite)

Function: function-option-name-fix

(defun function-option-name-fix (option-name)
  (declare (xargs :guard (function-option-name-p option-name)))
  (let ((acl2::__function__ 'function-option-name-fix))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (if (function-option-name-p option-name)
             option-name
           ':formals)
         :exec option-name)))

Theorem: function-option-name-p-of-function-option-name-fix

(defthm function-option-name-p-of-function-option-name-fix
  (b* ((fixed-option-name (function-option-name-fix option-name)))
    (function-option-name-p fixed-option-name))
  :rule-classes :rewrite)

Function: function-option-name-equiv$inline

(defun function-option-name-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (function-option-name-p acl2::x)
                              (function-option-name-p acl2::y))))
  (equal (function-option-name-fix acl2::x)
         (function-option-name-fix acl2::y)))

Theorem: function-option-name-equiv-is-an-equivalence

(defthm function-option-name-equiv-is-an-equivalence
  (and (booleanp (function-option-name-equiv x y))
       (function-option-name-equiv x x)
       (implies (function-option-name-equiv x y)
                (function-option-name-equiv y x))
       (implies (and (function-option-name-equiv x y)
                     (function-option-name-equiv y z))
                (function-option-name-equiv x z)))
  :rule-classes (:equivalence))

Theorem: function-option-name-equiv-implies-equal-function-option-name-fix-1

(defthm
 function-option-name-equiv-implies-equal-function-option-name-fix-1
 (implies (function-option-name-equiv acl2::x x-equiv)
          (equal (function-option-name-fix acl2::x)
                 (function-option-name-fix x-equiv)))
 :rule-classes (:congruence))

Theorem: function-option-name-fix-under-function-option-name-equiv

(defthm function-option-name-fix-under-function-option-name-equiv
  (function-option-name-equiv (function-option-name-fix acl2::x)
                              acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-function-option-name-fix-1-forward-to-function-option-name-equiv

(defthm
 equal-of-function-option-name-fix-1-forward-to-function-option-name-equiv
 (implies (equal (function-option-name-fix acl2::x)
                 acl2::y)
          (function-option-name-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Theorem: equal-of-function-option-name-fix-2-forward-to-function-option-name-equiv

(defthm
 equal-of-function-option-name-fix-2-forward-to-function-option-name-equiv
 (implies (equal acl2::x
                 (function-option-name-fix acl2::y))
          (function-option-name-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Theorem: function-option-name-equiv-of-function-option-name-fix-1-forward

(defthm
   function-option-name-equiv-of-function-option-name-fix-1-forward
 (implies
      (function-option-name-equiv (function-option-name-fix acl2::x)
                                  acl2::y)
      (function-option-name-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Theorem: function-option-name-equiv-of-function-option-name-fix-2-forward

(defthm
   function-option-name-equiv-of-function-option-name-fix-2-forward
 (implies
     (function-option-name-equiv acl2::x
                                 (function-option-name-fix acl2::y))
     (function-option-name-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Function: function-option-name-lst-p

(defun function-option-name-lst-p (x)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'function-option-name-lst-p))
    (declare (ignorable acl2::__function__))
    (if (atom x)
        (eq x nil)
      (and (function-option-name-p (car x))
           (function-option-name-lst-p (cdr x))))))

Theorem: function-option-name-lst-p-of-cons

(defthm function-option-name-lst-p-of-cons
  (equal (function-option-name-lst-p (cons acl2::a acl2::x))
         (and (function-option-name-p acl2::a)
              (function-option-name-lst-p acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-cdr-when-function-option-name-lst-p

(defthm
  function-option-name-lst-p-of-cdr-when-function-option-name-lst-p
  (implies (function-option-name-lst-p (double-rewrite acl2::x))
           (function-option-name-lst-p (cdr acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-when-not-consp

(defthm function-option-name-lst-p-when-not-consp
  (implies (not (consp acl2::x))
           (equal (function-option-name-lst-p acl2::x)
                  (not acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-p-of-car-when-function-option-name-lst-p

(defthm
      function-option-name-p-of-car-when-function-option-name-lst-p
  (implies (function-option-name-lst-p acl2::x)
           (iff (function-option-name-p (car acl2::x))
                (or (consp acl2::x)
                    (function-option-name-p nil))))
  :rule-classes ((:rewrite)))

Theorem: true-listp-when-function-option-name-lst-p-compound-recognizer

(defthm
     true-listp-when-function-option-name-lst-p-compound-recognizer
  (implies (function-option-name-lst-p acl2::x)
           (true-listp acl2::x))
  :rule-classes :compound-recognizer)

Theorem: function-option-name-lst-p-of-list-fix

(defthm function-option-name-lst-p-of-list-fix
  (implies (function-option-name-lst-p acl2::x)
           (function-option-name-lst-p (acl2::list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-sfix

(defthm function-option-name-lst-p-of-sfix
  (iff (function-option-name-lst-p (set::sfix acl2::x))
       (or (function-option-name-lst-p acl2::x)
           (not (set::setp acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-insert

(defthm function-option-name-lst-p-of-insert
  (iff (function-option-name-lst-p (set::insert acl2::a acl2::x))
       (and (function-option-name-lst-p (set::sfix acl2::x))
            (function-option-name-p acl2::a)))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-delete

(defthm function-option-name-lst-p-of-delete
  (implies
       (function-option-name-lst-p acl2::x)
       (function-option-name-lst-p (set::delete acl2::k acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-mergesort

(defthm function-option-name-lst-p-of-mergesort
  (iff (function-option-name-lst-p (set::mergesort acl2::x))
       (function-option-name-lst-p (acl2::list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-union

(defthm function-option-name-lst-p-of-union
  (iff (function-option-name-lst-p (set::union acl2::x acl2::y))
       (and (function-option-name-lst-p (set::sfix acl2::x))
            (function-option-name-lst-p (set::sfix acl2::y))))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-intersect-1

(defthm function-option-name-lst-p-of-intersect-1
 (implies
      (function-option-name-lst-p acl2::x)
      (function-option-name-lst-p (set::intersect acl2::x acl2::y)))
 :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-intersect-2

(defthm function-option-name-lst-p-of-intersect-2
 (implies
      (function-option-name-lst-p acl2::y)
      (function-option-name-lst-p (set::intersect acl2::x acl2::y)))
 :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-difference

(defthm function-option-name-lst-p-of-difference
 (implies
     (function-option-name-lst-p acl2::x)
     (function-option-name-lst-p (set::difference acl2::x acl2::y)))
 :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-duplicated-members

(defthm function-option-name-lst-p-of-duplicated-members
 (implies
    (function-option-name-lst-p acl2::x)
    (function-option-name-lst-p (acl2::duplicated-members acl2::x)))
 :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-rev

(defthm function-option-name-lst-p-of-rev
  (equal (function-option-name-lst-p (acl2::rev acl2::x))
         (function-option-name-lst-p (acl2::list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-append

(defthm function-option-name-lst-p-of-append
  (equal (function-option-name-lst-p (append acl2::a acl2::b))
         (and (function-option-name-lst-p (acl2::list-fix acl2::a))
              (function-option-name-lst-p acl2::b)))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-rcons

(defthm function-option-name-lst-p-of-rcons
  (iff (function-option-name-lst-p (acl2::rcons acl2::a acl2::x))
       (and (function-option-name-p acl2::a)
            (function-option-name-lst-p (acl2::list-fix acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-p-when-member-equal-of-function-option-name-lst-p

(defthm
 function-option-name-p-when-member-equal-of-function-option-name-lst-p
 (and (implies (and (member-equal acl2::a acl2::x)
                    (function-option-name-lst-p acl2::x))
               (function-option-name-p acl2::a))
      (implies (and (function-option-name-lst-p acl2::x)
                    (member-equal acl2::a acl2::x))
               (function-option-name-p acl2::a)))
 :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-when-subsetp-equal

(defthm function-option-name-lst-p-when-subsetp-equal
  (and (implies (and (subsetp-equal acl2::x acl2::y)
                     (function-option-name-lst-p acl2::y))
                (equal (function-option-name-lst-p acl2::x)
                       (true-listp acl2::x)))
       (implies (and (function-option-name-lst-p acl2::y)
                     (subsetp-equal acl2::x acl2::y))
                (equal (function-option-name-lst-p acl2::x)
                       (true-listp acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-set-difference-equal

(defthm function-option-name-lst-p-of-set-difference-equal
  (implies (function-option-name-lst-p acl2::x)
           (function-option-name-lst-p
                (set-difference-equal acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-intersection-equal-1

(defthm function-option-name-lst-p-of-intersection-equal-1
 (implies
  (function-option-name-lst-p (double-rewrite acl2::x))
  (function-option-name-lst-p (intersection-equal acl2::x acl2::y)))
 :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-intersection-equal-2

(defthm function-option-name-lst-p-of-intersection-equal-2
 (implies
  (function-option-name-lst-p (double-rewrite acl2::y))
  (function-option-name-lst-p (intersection-equal acl2::x acl2::y)))
 :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-union-equal

(defthm function-option-name-lst-p-of-union-equal
 (equal (function-option-name-lst-p (union-equal acl2::x acl2::y))
        (and (function-option-name-lst-p (acl2::list-fix acl2::x))
             (function-option-name-lst-p (double-rewrite acl2::y))))
 :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-take

(defthm function-option-name-lst-p-of-take
  (implies (function-option-name-lst-p (double-rewrite acl2::x))
           (iff (function-option-name-lst-p (take acl2::n acl2::x))
                (or (function-option-name-p nil)
                    (<= (nfix acl2::n) (len acl2::x)))))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-repeat

(defthm function-option-name-lst-p-of-repeat
  (iff (function-option-name-lst-p (acl2::repeat acl2::n acl2::x))
       (or (function-option-name-p acl2::x)
           (zp acl2::n)))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-p-of-nth-when-function-option-name-lst-p

(defthm
      function-option-name-p-of-nth-when-function-option-name-lst-p
  (implies (and (function-option-name-lst-p acl2::x)
                (< (nfix acl2::n) (len acl2::x)))
           (function-option-name-p (nth acl2::n acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-update-nth

(defthm function-option-name-lst-p-of-update-nth
 (implies
  (function-option-name-lst-p (double-rewrite acl2::x))
  (iff
   (function-option-name-lst-p (update-nth acl2::n acl2::y acl2::x))
   (and (function-option-name-p acl2::y)
        (or (<= (nfix acl2::n) (len acl2::x))
            (function-option-name-p nil)))))
 :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-butlast

(defthm function-option-name-lst-p-of-butlast
  (implies (function-option-name-lst-p (double-rewrite acl2::x))
           (function-option-name-lst-p (butlast acl2::x acl2::n)))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-nthcdr

(defthm function-option-name-lst-p-of-nthcdr
  (implies (function-option-name-lst-p (double-rewrite acl2::x))
           (function-option-name-lst-p (nthcdr acl2::n acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-last

(defthm function-option-name-lst-p-of-last
  (implies (function-option-name-lst-p (double-rewrite acl2::x))
           (function-option-name-lst-p (last acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-remove

(defthm function-option-name-lst-p-of-remove
  (implies (function-option-name-lst-p acl2::x)
           (function-option-name-lst-p (remove acl2::a acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: function-option-name-lst-p-of-revappend

(defthm function-option-name-lst-p-of-revappend
  (equal (function-option-name-lst-p (revappend acl2::x acl2::y))
         (and (function-option-name-lst-p (acl2::list-fix acl2::x))
              (function-option-name-lst-p acl2::y)))
  :rule-classes ((:rewrite)))

Function: function-option-name-lst-fix$inline

(defun function-option-name-lst-fix$inline (x)
  (declare (xargs :guard (function-option-name-lst-p x)))
  (let ((acl2::__function__ 'function-option-name-lst-fix))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (if (atom x)
             nil
           (cons (function-option-name-fix (car x))
                 (function-option-name-lst-fix (cdr x))))
         :exec x)))

Theorem: function-option-name-lst-p-of-function-option-name-lst-fix

(defthm function-option-name-lst-p-of-function-option-name-lst-fix
  (b* ((fty::newx (function-option-name-lst-fix$inline x)))
    (function-option-name-lst-p fty::newx))
  :rule-classes :rewrite)

Theorem: function-option-name-lst-fix-when-function-option-name-lst-p

(defthm function-option-name-lst-fix-when-function-option-name-lst-p
  (implies (function-option-name-lst-p x)
           (equal (function-option-name-lst-fix x)
                  x)))

Function: function-option-name-lst-equiv$inline

(defun function-option-name-lst-equiv$inline (acl2::x acl2::y)
 (declare (xargs :guard (and (function-option-name-lst-p acl2::x)
                             (function-option-name-lst-p acl2::y))))
 (equal (function-option-name-lst-fix acl2::x)
        (function-option-name-lst-fix acl2::y)))

Theorem: function-option-name-lst-equiv-is-an-equivalence

(defthm function-option-name-lst-equiv-is-an-equivalence
  (and (booleanp (function-option-name-lst-equiv x y))
       (function-option-name-lst-equiv x x)
       (implies (function-option-name-lst-equiv x y)
                (function-option-name-lst-equiv y x))
       (implies (and (function-option-name-lst-equiv x y)
                     (function-option-name-lst-equiv y z))
                (function-option-name-lst-equiv x z)))
  :rule-classes (:equivalence))

Theorem: function-option-name-lst-equiv-implies-equal-function-option-name-lst-fix-1

(defthm
 function-option-name-lst-equiv-implies-equal-function-option-name-lst-fix-1
 (implies (function-option-name-lst-equiv acl2::x x-equiv)
          (equal (function-option-name-lst-fix acl2::x)
                 (function-option-name-lst-fix x-equiv)))
 :rule-classes (:congruence))

Theorem: function-option-name-lst-fix-under-function-option-name-lst-equiv

(defthm
  function-option-name-lst-fix-under-function-option-name-lst-equiv
  (function-option-name-lst-equiv
       (function-option-name-lst-fix acl2::x)
       acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-function-option-name-lst-fix-1-forward-to-function-option-name-lst-equiv

(defthm
 equal-of-function-option-name-lst-fix-1-forward-to-function-option-name-lst-equiv
 (implies (equal (function-option-name-lst-fix acl2::x)
                 acl2::y)
          (function-option-name-lst-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Theorem: equal-of-function-option-name-lst-fix-2-forward-to-function-option-name-lst-equiv

(defthm
 equal-of-function-option-name-lst-fix-2-forward-to-function-option-name-lst-equiv
 (implies (equal acl2::x
                 (function-option-name-lst-fix acl2::y))
          (function-option-name-lst-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Theorem: function-option-name-lst-equiv-of-function-option-name-lst-fix-1-forward

(defthm
 function-option-name-lst-equiv-of-function-option-name-lst-fix-1-forward
 (implies (function-option-name-lst-equiv
               (function-option-name-lst-fix acl2::x)
               acl2::y)
          (function-option-name-lst-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Theorem: function-option-name-lst-equiv-of-function-option-name-lst-fix-2-forward

(defthm
 function-option-name-lst-equiv-of-function-option-name-lst-fix-2-forward
 (implies (function-option-name-lst-equiv
               acl2::x
               (function-option-name-lst-fix acl2::y))
          (function-option-name-lst-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Theorem: car-of-function-option-name-lst-fix-x-under-function-option-name-equiv

(defthm
 car-of-function-option-name-lst-fix-x-under-function-option-name-equiv
 (function-option-name-equiv
      (car (function-option-name-lst-fix acl2::x))
      (car acl2::x)))

Theorem: car-function-option-name-lst-equiv-congruence-on-x-under-function-option-name-equiv

(defthm
 car-function-option-name-lst-equiv-congruence-on-x-under-function-option-name-equiv
 (implies (function-option-name-lst-equiv acl2::x x-equiv)
          (function-option-name-equiv (car acl2::x)
                                      (car x-equiv)))
 :rule-classes :congruence)

Theorem: cdr-of-function-option-name-lst-fix-x-under-function-option-name-lst-equiv

(defthm
 cdr-of-function-option-name-lst-fix-x-under-function-option-name-lst-equiv
 (function-option-name-lst-equiv
      (cdr (function-option-name-lst-fix acl2::x))
      (cdr acl2::x)))

Theorem: cdr-function-option-name-lst-equiv-congruence-on-x-under-function-option-name-lst-equiv

(defthm
 cdr-function-option-name-lst-equiv-congruence-on-x-under-function-option-name-lst-equiv
 (implies (function-option-name-lst-equiv acl2::x x-equiv)
          (function-option-name-lst-equiv (cdr acl2::x)
                                          (cdr x-equiv)))
 :rule-classes :congruence)

Theorem: cons-of-function-option-name-fix-x-under-function-option-name-lst-equiv

(defthm
 cons-of-function-option-name-fix-x-under-function-option-name-lst-equiv
 (function-option-name-lst-equiv
      (cons (function-option-name-fix acl2::x)
            acl2::y)
      (cons acl2::x acl2::y)))

Theorem: cons-function-option-name-equiv-congruence-on-x-under-function-option-name-lst-equiv

(defthm
 cons-function-option-name-equiv-congruence-on-x-under-function-option-name-lst-equiv
 (implies (function-option-name-equiv acl2::x x-equiv)
          (function-option-name-lst-equiv (cons acl2::x acl2::y)
                                          (cons x-equiv acl2::y)))
 :rule-classes :congruence)

Theorem: cons-of-function-option-name-lst-fix-y-under-function-option-name-lst-equiv

(defthm
 cons-of-function-option-name-lst-fix-y-under-function-option-name-lst-equiv
 (function-option-name-lst-equiv
      (cons acl2::x
            (function-option-name-lst-fix acl2::y))
      (cons acl2::x acl2::y)))

Theorem: cons-function-option-name-lst-equiv-congruence-on-y-under-function-option-name-lst-equiv

(defthm
 cons-function-option-name-lst-equiv-congruence-on-y-under-function-option-name-lst-equiv
 (implies (function-option-name-lst-equiv acl2::y y-equiv)
          (function-option-name-lst-equiv (cons acl2::x acl2::y)
                                          (cons acl2::x y-equiv)))
 :rule-classes :congruence)

Theorem: consp-of-function-option-name-lst-fix

(defthm consp-of-function-option-name-lst-fix
  (equal (consp (function-option-name-lst-fix acl2::x))
         (consp acl2::x)))

Theorem: function-option-name-lst-fix-under-iff

(defthm function-option-name-lst-fix-under-iff
  (iff (function-option-name-lst-fix acl2::x)
       (consp acl2::x)))

Theorem: function-option-name-lst-fix-of-cons

(defthm function-option-name-lst-fix-of-cons
  (equal (function-option-name-lst-fix (cons a x))
         (cons (function-option-name-fix a)
               (function-option-name-lst-fix x))))

Theorem: len-of-function-option-name-lst-fix

(defthm len-of-function-option-name-lst-fix
  (equal (len (function-option-name-lst-fix acl2::x))
         (len acl2::x)))

Theorem: function-option-name-lst-fix-of-append

(defthm function-option-name-lst-fix-of-append
  (equal (function-option-name-lst-fix (append std::a std::b))
         (append (function-option-name-lst-fix std::a)
                 (function-option-name-lst-fix std::b))))

Theorem: function-option-name-lst-fix-of-repeat

(defthm function-option-name-lst-fix-of-repeat
  (equal
       (function-option-name-lst-fix (acl2::repeat acl2::n acl2::x))
       (acl2::repeat acl2::n
                     (function-option-name-fix acl2::x))))

Theorem: list-equiv-refines-function-option-name-lst-equiv

(defthm list-equiv-refines-function-option-name-lst-equiv
  (implies (acl2::list-equiv acl2::x acl2::y)
           (function-option-name-lst-equiv acl2::x acl2::y))
  :rule-classes :refinement)

Theorem: nth-of-function-option-name-lst-fix

(defthm nth-of-function-option-name-lst-fix
  (equal (nth acl2::n
              (function-option-name-lst-fix acl2::x))
         (if (< (nfix acl2::n) (len acl2::x))
             (function-option-name-fix (nth acl2::n acl2::x))
           nil)))

Theorem: function-option-name-lst-equiv-implies-function-option-name-lst-equiv-append-1

(defthm
 function-option-name-lst-equiv-implies-function-option-name-lst-equiv-append-1
 (implies
     (function-option-name-lst-equiv acl2::x fty::x-equiv)
     (function-option-name-lst-equiv (append acl2::x acl2::y)
                                     (append fty::x-equiv acl2::y)))
 :rule-classes (:congruence))

Theorem: function-option-name-lst-equiv-implies-function-option-name-lst-equiv-append-2

(defthm
 function-option-name-lst-equiv-implies-function-option-name-lst-equiv-append-2
 (implies
     (function-option-name-lst-equiv acl2::y fty::y-equiv)
     (function-option-name-lst-equiv (append acl2::x acl2::y)
                                     (append acl2::x fty::y-equiv)))
 :rule-classes (:congruence))

Theorem: function-option-name-lst-equiv-implies-function-option-name-lst-equiv-nthcdr-2

(defthm
 function-option-name-lst-equiv-implies-function-option-name-lst-equiv-nthcdr-2
 (implies (function-option-name-lst-equiv acl2::l l-equiv)
          (function-option-name-lst-equiv (nthcdr acl2::n acl2::l)
                                          (nthcdr acl2::n l-equiv)))
 :rule-classes (:congruence))

Theorem: function-option-name-lst-equiv-implies-function-option-name-lst-equiv-take-2

(defthm
 function-option-name-lst-equiv-implies-function-option-name-lst-equiv-take-2
 (implies (function-option-name-lst-equiv acl2::l l-equiv)
          (function-option-name-lst-equiv (take acl2::n acl2::l)
                                          (take acl2::n l-equiv)))
 :rule-classes (:congruence))

Theorem: function-option-name-fix-preserves-member

(defthm function-option-name-fix-preserves-member
  (implies (member x used :test 'equal)
           (member (function-option-name-fix x)
                   (function-option-name-lst-fix used)
                   :test 'equal)))

Theorem: function-option-name-lst-fix-preserves-subsetp

(defthm function-option-name-lst-fix-preserves-subsetp
  (implies (subsetp used-1 used-2 :test 'equal)
           (subsetp (function-option-name-lst-fix used-1)
                    (function-option-name-lst-fix used-2)
                    :test 'equal)))

Theorem: function-option-name-lst-fix-preserves-set-equiv

(defthm function-option-name-lst-fix-preserves-set-equiv
  (implies (acl2::set-equiv used-1 used-2)
           (acl2::set-equiv (function-option-name-lst-fix used-1)
                            (function-option-name-lst-fix used-2)))
  :rule-classes (:congruence))

Theorem: function-option-name-lst-p-and-member

(defthm function-option-name-lst-p-and-member
  (implies (and (member x used)
                (not (function-option-name-p x)))
           (not (function-option-name-lst-p used))))

Theorem: function-option-name-lst-p--monotonicity

(defthm function-option-name-lst-p--monotonicity
  (implies (and (equal (true-listp used-1)
                       (true-listp used-2))
                (subsetp used-1 used-2 :test 'equal)
                (function-option-name-lst-p used-2))
           (function-option-name-lst-p used-1)))

Theorem: function-option-name-lst-p--congruence

(defthm function-option-name-lst-p--congruence
  (implies (true-set-equiv used-1 used-2)
           (equal (function-option-name-lst-p used-1)
                  (function-option-name-lst-p used-2)))
  :rule-classes (:congruence))

Function: eval-function-option-type

(defun eval-function-option-type (option-type term)
  (declare (xargs :guard (function-option-type-p option-type)))
  (let ((acl2::__function__ 'eval-function-option-type))
    (declare (ignorable acl2::__function__))
    (b* ((option-type (function-option-type-fix option-type)))
      (case option-type
        (argument-lst-syntax-p (argument-lst-syntax-p term))
        (natp (natp term))
        (hypothesis-syntax-p (hypothesis-syntax-p term))
        (t (hypothesis-lst-syntax-p term))))))

Theorem: booleanp-of-eval-function-option-type

(defthm booleanp-of-eval-function-option-type
  (b* ((type-correct? (eval-function-option-type option-type term)))
    (booleanp type-correct?))
  :rule-classes :rewrite)

Function: function-option-syntax-p

(defun function-option-syntax-p (term used)
 (declare (xargs :guard (function-option-name-lst-p used)))
 (let ((acl2::__function__ 'function-option-syntax-p))
  (declare (ignorable acl2::__function__))
  (b* ((used (function-option-name-lst-fix used))
       ((unless (true-listp term))
        (mv nil used))
       ((unless (consp term)) (mv t used))
       ((unless (and (car term)
                     (cdr term)
                     (not (cddr term))))
        (mv nil used))
       ((cons option body-lst) term)
       ((unless (function-option-name-p option))
        (mv nil used))
       (option-type (cdr (assoc-equal option *function-options*))))
    (mv (and (not (member-equal option used))
             (eval-function-option-type option-type (car body-lst)))
        (cons option used)))))

Theorem: booleanp-of-function-option-syntax-p.ok

(defthm booleanp-of-function-option-syntax-p.ok
  (b* (((mv ?ok ?new-used)
        (function-option-syntax-p term used)))
    (booleanp ok))
  :rule-classes :rewrite)

Theorem: function-option-name-lst-p-of-function-option-syntax-p.new-used

(defthm
    function-option-name-lst-p-of-function-option-syntax-p.new-used
  (b* (((mv ?ok ?new-used)
        (function-option-syntax-p term used)))
    (function-option-name-lst-p new-used))
  :rule-classes :rewrite)

Theorem: function-option-syntax-p--monotonicity.ok

(defthm function-option-syntax-p--monotonicity.ok
  (b* (((mv ?ok ?new-used)
        (function-option-syntax-p term used)))
    (implies (and (subsetp used-1 used :test 'equal)
                  ok)
             (mv-nth 0
                     (function-option-syntax-p term used-1))))
  :rule-classes :rewrite)

Theorem: function-option-syntax-p--ok-congruence.ok

(defthm function-option-syntax-p--ok-congruence.ok
  (b* (((mv ?ok ?new-used)
        (function-option-syntax-p term used)))
    (implies (acl2::set-equiv used-1 used)
             (equal (mv-nth 0
                            (function-option-syntax-p term used-1))
                    ok)))
  :rule-classes (:congruence))

Theorem: function-option-syntax-p--monotonicity.new-used

(defthm function-option-syntax-p--monotonicity.new-used
 (b* (((mv ?ok ?new-used)
       (function-option-syntax-p term used)))
   (implies (and (subsetp used-1 used :test 'equal)
                 ok)
            (subsetp (mv-nth 1
                             (function-option-syntax-p term used-1))
                     new-used
                     :test 'equal)))
 :rule-classes :rewrite)

Theorem: function-option-syntax-p--new-used-when-ok

(defthm function-option-syntax-p--new-used-when-ok
  (b* (((mv ?ok ?new-used)
        (function-option-syntax-p term used)))
    (implies (and term ok)
             (equal new-used
                    (cons (car term)
                          (function-option-name-lst-fix used)))))
  :rule-classes :rewrite)

Function: function-option-lst-syntax-p-helper

(defun function-option-lst-syntax-p-helper (term used)
  (declare (xargs :guard (function-option-name-lst-p used)))
  (let ((acl2::__function__ 'function-option-lst-syntax-p-helper))
    (declare (ignorable acl2::__function__))
    (b* (((unless (true-listp term)) nil)
         ((unless term) t)
         ((unless (cdr term)) nil)
         ((list* first second rest) term)
         ((mv res new-used)
          (function-option-syntax-p (list first second)
                                    used)))
      (and res
           (function-option-lst-syntax-p-helper rest new-used)))))

Theorem: booleanp-of-function-option-lst-syntax-p-helper

(defthm booleanp-of-function-option-lst-syntax-p-helper
  (b* ((ok (function-option-lst-syntax-p-helper term used)))
    (booleanp ok))
  :rule-classes :rewrite)

Theorem: function-option-lst-syntax-p-helper--monotonicity

(defthm function-option-lst-syntax-p-helper--monotonicity
  (implies (and (subsetp used-1 used :test 'equal)
                (function-option-lst-syntax-p-helper term used))
           (function-option-lst-syntax-p-helper term used-1)))

Theorem: function-option-lst-syntax-p-helper--congruence

(defthm function-option-lst-syntax-p-helper--congruence
 (b* ((ok (function-option-lst-syntax-p-helper term used)))
   (implies (acl2::set-equiv used-1 used)
            (equal (function-option-lst-syntax-p-helper term used-1)
                   ok)))
 :rule-classes (:congruence))

Theorem: function-option-lst-syntax-p-helper--head

(defthm function-option-lst-syntax-p-helper--head
  (implies
       (and (function-option-lst-syntax-p-helper term used)
            term)
       (and (<= 2 (len term))
            (function-option-syntax-p (list (car term) (cadr term))
                                      used))))

Theorem: function-option-lst-syntax-p-helper-preserve

(defthm function-option-lst-syntax-p-helper-preserve
  (implies (and (function-option-lst-syntax-p-helper term nil)
                (consp term))
           (function-option-lst-syntax-p-helper (cddr term)
                                                nil)))

Function: function-option-lst-syntax-p

(defun function-option-lst-syntax-p (term)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'function-option-lst-syntax-p))
    (declare (ignorable acl2::__function__))
    (function-option-lst-syntax-p-helper term nil)))

Theorem: booleanp-of-function-option-lst-syntax-p

(defthm booleanp-of-function-option-lst-syntax-p
  (b* ((syntax-good? (function-option-lst-syntax-p term)))
    (booleanp syntax-good?))
  :rule-classes :rewrite)

Function: function-option-lst-syntax-fix

(defun function-option-lst-syntax-fix (term)
  (declare (xargs :guard (function-option-lst-syntax-p term)))
  (let ((acl2::__function__ 'function-option-lst-syntax-fix))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (if (function-option-lst-syntax-p term)
             term
           nil)
         :exec term)))

Theorem: function-option-lst-syntax-p-of-function-option-lst-syntax-fix

(defthm
     function-option-lst-syntax-p-of-function-option-lst-syntax-fix
  (b* ((fixed-term (function-option-lst-syntax-fix term)))
    (function-option-lst-syntax-p fixed-term))
  :rule-classes :rewrite)

Theorem: function-option-lst-syntax-fix-when-function-option-lst-syntaxp

(defthm
    function-option-lst-syntax-fix-when-function-option-lst-syntaxp
  (b* ((fixed-term (function-option-lst-syntax-fix term)))
    (implies (function-option-lst-syntax-p term)
             (equal fixed-term term)))
  :rule-classes :rewrite)

Function: function-option-lst-syntax-equiv$inline

(defun function-option-lst-syntax-equiv$inline (acl2::x acl2::y)
  (declare
       (xargs :guard (and (function-option-lst-syntax-p acl2::x)
                          (function-option-lst-syntax-p acl2::y))))
  (equal (function-option-lst-syntax-fix acl2::x)
         (function-option-lst-syntax-fix acl2::y)))

Theorem: function-option-lst-syntax-equiv-is-an-equivalence

(defthm function-option-lst-syntax-equiv-is-an-equivalence
  (and (booleanp (function-option-lst-syntax-equiv x y))
       (function-option-lst-syntax-equiv x x)
       (implies (function-option-lst-syntax-equiv x y)
                (function-option-lst-syntax-equiv y x))
       (implies (and (function-option-lst-syntax-equiv x y)
                     (function-option-lst-syntax-equiv y z))
                (function-option-lst-syntax-equiv x z)))
  :rule-classes (:equivalence))

Theorem: function-option-lst-syntax-equiv-implies-equal-function-option-lst-syntax-fix-1

(defthm
 function-option-lst-syntax-equiv-implies-equal-function-option-lst-syntax-fix-1
 (implies (function-option-lst-syntax-equiv acl2::x x-equiv)
          (equal (function-option-lst-syntax-fix acl2::x)
                 (function-option-lst-syntax-fix x-equiv)))
 :rule-classes (:congruence))

Theorem: function-option-lst-syntax-fix-under-function-option-lst-syntax-equiv

(defthm
 function-option-lst-syntax-fix-under-function-option-lst-syntax-equiv
 (function-option-lst-syntax-equiv
      (function-option-lst-syntax-fix acl2::x)
      acl2::x)
 :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-function-option-lst-syntax-fix-1-forward-to-function-option-lst-syntax-equiv

(defthm
 equal-of-function-option-lst-syntax-fix-1-forward-to-function-option-lst-syntax-equiv
 (implies (equal (function-option-lst-syntax-fix acl2::x)
                 acl2::y)
          (function-option-lst-syntax-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Theorem: equal-of-function-option-lst-syntax-fix-2-forward-to-function-option-lst-syntax-equiv

(defthm
 equal-of-function-option-lst-syntax-fix-2-forward-to-function-option-lst-syntax-equiv
 (implies (equal acl2::x
                 (function-option-lst-syntax-fix acl2::y))
          (function-option-lst-syntax-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Theorem: function-option-lst-syntax-equiv-of-function-option-lst-syntax-fix-1-forward

(defthm
 function-option-lst-syntax-equiv-of-function-option-lst-syntax-fix-1-forward
 (implies (function-option-lst-syntax-equiv
               (function-option-lst-syntax-fix acl2::x)
               acl2::y)
          (function-option-lst-syntax-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Theorem: function-option-lst-syntax-equiv-of-function-option-lst-syntax-fix-2-forward

(defthm
 function-option-lst-syntax-equiv-of-function-option-lst-syntax-fix-2-forward
 (implies (function-option-lst-syntax-equiv
               acl2::x
               (function-option-lst-syntax-fix acl2::y))
          (function-option-lst-syntax-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Theorem: everything-about-function-option-lst-syntax-p

(defthm everything-about-function-option-lst-syntax-p
 (implies
    (and (function-option-lst-syntax-p term)
         term)
    (let* ((opt (car term))
           (val (cadr term))
           (rest (cddr term))
           (option-type (cdr (assoc-equal opt *function-options*))))
      (and (true-listp term)
           (consp (cdr term))
           (equal (function-option-lst-syntax-fix term)
                  term)
           (function-option-lst-syntax-p rest)
           (member-equal opt *function-option-names*)
           (member-equal option-type *function-option-types*)
           (implies (equal option-type 'argument-lst-syntax-p)
                    (argument-lst-syntax-p val))
           (implies (equal option-type 'natp)
                    (and (integerp val) (<= 0 val)))
           (implies (equal option-type 'hypothesis-syntax-p)
                    (hypothesis-syntax-p val))
           (implies (equal option-type 'hypothesis-lst-syntax-p)
                    (hypothesis-lst-syntax-p val))))))

Function: function-syntax-p

(defun function-syntax-p (term)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'function-syntax-p))
    (declare (ignorable acl2::__function__))
    (b* (((unless (true-listp term)) nil)
         ((unless (consp term)) t)
         ((cons fname function-options) term))
      (and (symbolp fname)
           (function-option-lst-syntax-p function-options)))))

Theorem: booleanp-of-function-syntax-p

(defthm booleanp-of-function-syntax-p
  (b* ((syntax-good? (function-syntax-p term)))
    (booleanp syntax-good?))
  :rule-classes :rewrite)

Function: function-syntax-fix

(defun function-syntax-fix (term)
  (declare (xargs :guard (function-syntax-p term)))
  (let ((acl2::__function__ 'function-syntax-fix))
    (declare (ignorable acl2::__function__))
    (mbe :logic (if (function-syntax-p term) term nil)
         :exec term)))

Theorem: function-syntax-p-of-function-syntax-fix

(defthm function-syntax-p-of-function-syntax-fix
  (b* ((fixed-term (function-syntax-fix term)))
    (function-syntax-p fixed-term))
  :rule-classes :rewrite)

Function: function-syntax-equiv$inline

(defun function-syntax-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (function-syntax-p acl2::x)
                              (function-syntax-p acl2::y))))
  (equal (function-syntax-fix acl2::x)
         (function-syntax-fix acl2::y)))

Theorem: function-syntax-equiv-is-an-equivalence

(defthm function-syntax-equiv-is-an-equivalence
  (and (booleanp (function-syntax-equiv x y))
       (function-syntax-equiv x x)
       (implies (function-syntax-equiv x y)
                (function-syntax-equiv y x))
       (implies (and (function-syntax-equiv x y)
                     (function-syntax-equiv y z))
                (function-syntax-equiv x z)))
  :rule-classes (:equivalence))

Theorem: function-syntax-equiv-implies-equal-function-syntax-fix-1

(defthm function-syntax-equiv-implies-equal-function-syntax-fix-1
  (implies (function-syntax-equiv acl2::x x-equiv)
           (equal (function-syntax-fix acl2::x)
                  (function-syntax-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: function-syntax-fix-under-function-syntax-equiv

(defthm function-syntax-fix-under-function-syntax-equiv
  (function-syntax-equiv (function-syntax-fix acl2::x)
                         acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-function-syntax-fix-1-forward-to-function-syntax-equiv

(defthm
    equal-of-function-syntax-fix-1-forward-to-function-syntax-equiv
  (implies (equal (function-syntax-fix acl2::x)
                  acl2::y)
           (function-syntax-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: equal-of-function-syntax-fix-2-forward-to-function-syntax-equiv

(defthm
    equal-of-function-syntax-fix-2-forward-to-function-syntax-equiv
  (implies (equal acl2::x (function-syntax-fix acl2::y))
           (function-syntax-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: function-syntax-equiv-of-function-syntax-fix-1-forward

(defthm function-syntax-equiv-of-function-syntax-fix-1-forward
  (implies (function-syntax-equiv (function-syntax-fix acl2::x)
                                  acl2::y)
           (function-syntax-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: function-syntax-equiv-of-function-syntax-fix-2-forward

(defthm function-syntax-equiv-of-function-syntax-fix-2-forward
  (implies
       (function-syntax-equiv acl2::x (function-syntax-fix acl2::y))
       (function-syntax-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Function: function-lst-syntax-p

(defun function-lst-syntax-p (term)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'function-lst-syntax-p))
    (declare (ignorable acl2::__function__))
    (b* (((if (atom term)) (equal term nil))
         ((cons first rest) term))
      (and (function-syntax-p first)
           (function-lst-syntax-p rest)))))

Theorem: booleanp-of-function-lst-syntax-p

(defthm booleanp-of-function-lst-syntax-p
  (b* ((syntax-good? (function-lst-syntax-p term)))
    (booleanp syntax-good?))
  :rule-classes :rewrite)

Function: function-lst-syntax-fix

(defun function-lst-syntax-fix (term)
  (declare (xargs :guard (function-lst-syntax-p term)))
  (let ((acl2::__function__ 'function-lst-syntax-fix))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (if (consp term)
             (cons (function-syntax-fix (car term))
                   (function-lst-syntax-fix (cdr term)))
           nil)
         :exec term)))

Theorem: function-lst-syntax-p-of-function-lst-syntax-fix

(defthm function-lst-syntax-p-of-function-lst-syntax-fix
  (b* ((fixed-term (function-lst-syntax-fix term)))
    (function-lst-syntax-p fixed-term))
  :rule-classes :rewrite)

Function: function-lst-syntax-equiv$inline

(defun function-lst-syntax-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (function-lst-syntax-p acl2::x)
                              (function-lst-syntax-p acl2::y))))
  (equal (function-lst-syntax-fix acl2::x)
         (function-lst-syntax-fix acl2::y)))

Theorem: function-lst-syntax-equiv-is-an-equivalence

(defthm function-lst-syntax-equiv-is-an-equivalence
  (and (booleanp (function-lst-syntax-equiv x y))
       (function-lst-syntax-equiv x x)
       (implies (function-lst-syntax-equiv x y)
                (function-lst-syntax-equiv y x))
       (implies (and (function-lst-syntax-equiv x y)
                     (function-lst-syntax-equiv y z))
                (function-lst-syntax-equiv x z)))
  :rule-classes (:equivalence))

Theorem: function-lst-syntax-equiv-implies-equal-function-lst-syntax-fix-1

(defthm
  function-lst-syntax-equiv-implies-equal-function-lst-syntax-fix-1
  (implies (function-lst-syntax-equiv acl2::x x-equiv)
           (equal (function-lst-syntax-fix acl2::x)
                  (function-lst-syntax-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: function-lst-syntax-fix-under-function-lst-syntax-equiv

(defthm function-lst-syntax-fix-under-function-lst-syntax-equiv
  (function-lst-syntax-equiv (function-lst-syntax-fix acl2::x)
                             acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-function-lst-syntax-fix-1-forward-to-function-lst-syntax-equiv

(defthm
 equal-of-function-lst-syntax-fix-1-forward-to-function-lst-syntax-equiv
 (implies (equal (function-lst-syntax-fix acl2::x)
                 acl2::y)
          (function-lst-syntax-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Theorem: equal-of-function-lst-syntax-fix-2-forward-to-function-lst-syntax-equiv

(defthm
 equal-of-function-lst-syntax-fix-2-forward-to-function-lst-syntax-equiv
 (implies (equal acl2::x
                 (function-lst-syntax-fix acl2::y))
          (function-lst-syntax-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Theorem: function-lst-syntax-equiv-of-function-lst-syntax-fix-1-forward

(defthm
     function-lst-syntax-equiv-of-function-lst-syntax-fix-1-forward
  (implies
       (function-lst-syntax-equiv (function-lst-syntax-fix acl2::x)
                                  acl2::y)
       (function-lst-syntax-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: function-lst-syntax-equiv-of-function-lst-syntax-fix-2-forward

(defthm
     function-lst-syntax-equiv-of-function-lst-syntax-fix-2-forward
  (implies
       (function-lst-syntax-equiv acl2::x
                                  (function-lst-syntax-fix acl2::y))
       (function-lst-syntax-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Subtopics

Function-option-name-list

Function-option-syntax-p

Recoginizer for function-option-syntax.

Function-option-lst-syntax-p-helper

Helper for function-option-lst-syntax-p.

Function-option-lst-syntax-fix

Recogizer for function-option-lst-syntax

Function-option-type-fix

Fixing function for function-option-type.

Eval-function-option-type

Evaluating types for function option body.

Function-lst-syntax-fix

Fixing function for function-lst-syntax-fix

Function-syntax-p

Recognizer for function-syntax.

Function-option-type-p

Recoginizer for function-option-type.

Function-option-lst-syntax-p

Recogizer for function-option-lst-syntax

Function-lst-syntax-p

Recognizer for function-lst-syntax

Function-syntax-fix

Fixing function for function-syntax-p