• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • 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
            • Smtlink-hint-syntax
              • Smtlink-option-syntax-p
              • Smtlink-hint-syntax-p-helper
              • Smtlink-hint-syntax-fix
              • Smtlink-option-name-p
              • Smtlink-option-name-fix
              • Eval-smtlink-option-type
              • Smtlink-option-type-fix
              • Smtlink-option-type-p
              • Smtlink-hint-syntax-p
            • 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
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Taspi
    • Bitcoin
    • Riscv
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Axe
    • Bigmems
    • Builtins
    • Execloader
    • Aleo
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Smtlink-process-user-hint

Smtlink-hint-syntax

Definitions and Theorems

Function: smtlink-option-type-p

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

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

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

Function: smtlink-option-type-fix

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

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

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

Function: smtlink-option-name-p

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

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

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

Function: smtlink-option-name-fix

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

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

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

Function: smtlink-option-name-equiv$inline

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Function: smtlink-option-name-lst-p

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Function: eval-smtlink-option-type

(defun eval-smtlink-option-type (option-type term)
  (declare (xargs :guard (smtlink-option-type-p option-type)))
  (let ((acl2::__function__ 'eval-smtlink-option-type))
    (declare (ignorable acl2::__function__))
    (case option-type
      (function-lst-syntax-p (function-lst-syntax-p term))
      (hypothesis-lst-syntax-p (hypothesis-lst-syntax-p term))
      (hints-syntax-p (hints-syntax-p term))
      (symbol-listp (symbol-listp term))
      (booleanp (booleanp term))
      (stringp (stringp term))
      (smt-solver-params-p (smt-solver-params-p term))
      (custom-p (booleanp term))
      (t (natp term)))))

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

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

Function: smtlink-option-syntax-p

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

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

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

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

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

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

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

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

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

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

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

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

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

Function: smtlink-hint-syntax-p-helper

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

Theorem: booleanp-of-smtlink-hint-syntax-p-helper

(defthm booleanp-of-smtlink-hint-syntax-p-helper
  (b* ((syntax-good? (smtlink-hint-syntax-p-helper term used)))
    (booleanp syntax-good?))
  :rule-classes :rewrite)

Theorem: smtlink-hint-syntax-p-helper--monotonicity

(defthm smtlink-hint-syntax-p-helper--monotonicity
  (implies (and (subsetp used-1 used :test 'equal)
                (smtlink-hint-syntax-p-helper term used))
           (smtlink-hint-syntax-p-helper term used-1)))

Theorem: smtlink-hint-syntax-p-helper--congruence

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

Theorem: smtlink-hint-syntax-p-helper-preserve

(defthm smtlink-hint-syntax-p-helper-preserve
  (implies (and (smtlink-hint-syntax-p-helper term nil)
                (consp term))
           (smtlink-hint-syntax-p-helper (cddr term)
                                         nil)))

Function: smtlink-hint-syntax-p

(defun smtlink-hint-syntax-p (term)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'smtlink-hint-syntax-p))
    (declare (ignorable acl2::__function__))
    (smtlink-hint-syntax-p-helper term nil)))

Theorem: booleanp-of-smtlink-hint-syntax-p

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

Function: smtlink-hint-syntax-fix

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

Theorem: smtlink-hint-syntax-p-of-smtlink-hint-syntax-fix

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

Theorem: smtlink-hint-syntax-fix-when-smtlink-hint-syntax-p

(defthm smtlink-hint-syntax-fix-when-smtlink-hint-syntax-p
  (b* ((fixed-smtlink-hint-syntax (smtlink-hint-syntax-fix term)))
    (implies (smtlink-hint-syntax-p term)
             (equal fixed-smtlink-hint-syntax term)))
  :rule-classes :rewrite)

Theorem: everything-about-smtlink-syntax-p

(defthm everything-about-smtlink-syntax-p
 (implies
     (and (smtlink-hint-syntax-p term) term)
     (let* ((opt (car term))
            (val (cadr term))
            (rest (cddr term))
            (option-type (cdr (assoc-equal opt *smtlink-options*))))
       (and (true-listp term)
            (consp (cdr term))
            (equal (smtlink-hint-syntax-fix term)
                   term)
            (smtlink-hint-syntax-p rest)
            (member-equal opt *smtlink-option-names*)
            (member-equal option-type *smtlink-option-types*)
            (implies (equal option-type 'function-lst-syntax-p)
                     (function-lst-syntax-p val))
            (implies (equal option-type 'hypothesis-lst-syntax-p)
                     (hypothesis-lst-syntax-p val))
            (implies (equal option-type 'hints-syntax-p)
                     (hints-syntax-p val))
            (implies (equal option-type 'symbol-listp)
                     (symbol-listp val))
            (implies (equal option-type 'booleanp)
                     (booleanp val))
            (implies (equal option-type 'stringp)
                     (stringp val))
            (implies (equal option-type 'smt-solver-params-p)
                     (smt-solver-params-p val))
            (implies (equal option-type 'custom-p)
                     (booleanp val))
            (implies (equal option-type 'natp)
                     (natp val))))))

Function: smtlink-hint-syntax-equiv$inline

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

Theorem: smtlink-hint-syntax-equiv-is-an-equivalence

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

Theorem: smtlink-hint-syntax-equiv-implies-equal-smtlink-hint-syntax-fix-1

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

Theorem: smtlink-hint-syntax-fix-under-smtlink-hint-syntax-equiv

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

Theorem: equal-of-smtlink-hint-syntax-fix-1-forward-to-smtlink-hint-syntax-equiv

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

Theorem: equal-of-smtlink-hint-syntax-fix-2-forward-to-smtlink-hint-syntax-equiv

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

Theorem: smtlink-hint-syntax-equiv-of-smtlink-hint-syntax-fix-1-forward

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

Theorem: smtlink-hint-syntax-equiv-of-smtlink-hint-syntax-fix-2-forward

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

Subtopics

Smtlink-option-syntax-p

Recoginizer for smtlink-option-syntax.

Smtlink-hint-syntax-p-helper

Helper function for smtlink-hint-syntax-p.

Smtlink-hint-syntax-fix

Fixing function for smtlink-hint-syntax.

Smtlink-option-name-p

Recoginizer for an smtlink-option-name.

Smtlink-option-name-fix

Fixing function for smtlink-option-name.

Eval-smtlink-option-type

Evaluating types for smtlink option body.

Smtlink-option-type-fix

Fixing function for smtlink-option-type.

Smtlink-option-type-p

Recoginizer for smtlink-option-type.

Smtlink-hint-syntax-p

Recognizer for smtlink-hint-syntax.