• 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-lst
                    • Smtlink-option-name-lst-fix
                      • Smtlink-option-name-lst-equiv
                      • Smtlink-option-name-lst-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
        • Riscv
        • Taspi
        • Bitcoin
        • 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
        • Aleo
        • Bigmems
        • Builtins
        • Execloader
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Std
      • Community
      • Proof-automation
      • ACL2
      • Macro-libraries
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Smtlink-option-name-lst

    Smtlink-option-name-lst-fix

    (smtlink-option-name-lst-fix x) is a usual ACL2::fty list fixing function.

    Signature
    (smtlink-option-name-lst-fix x) → fty::newx
    Arguments
    x — Guard (smtlink-option-name-lst-p x).
    Returns
    fty::newx — Type (smtlink-option-name-lst-p fty::newx).

    In the logic, we apply smtlink-option-name-fix to each member of the x. In the execution, none of that is actually necessary and this is just an inlined identity function.

    Definitions and Theorems

    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))