• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
    • Gl
    • Witness-cp
    • Ccg
    • Install-not-normalized
    • Rewrite$
    • Removable-runes
    • Efficiency
    • Rewrite-bounds
    • Bash
    • Def-dag-measure
    • Fgl
      • Fgl-rewrite-rules
      • Fgl-function-mode
        • !fgl-function-mode->dont-rewrite-under-if-test
        • !fgl-function-mode->dont-primitive-exec
        • !fgl-function-mode->dont-concrete-exec
        • !fgl-function-mode->dont-expand-def
        • !fgl-function-mode->dont-rewrite
        • !fgl-function-mode->split-ifs
        • Fgl-function-mode->dont-rewrite-under-if-test
        • Fgl-function-mode->dont-primitive-exec
        • Fgl-function-mode->dont-concrete-exec
        • Fgl-function-mode-p
        • Fgl-function-mode->dont-expand-def
        • Fgl-function-mode->dont-rewrite
        • Fgl-function-mode-fix
        • Fgl-function-mode->split-ifs
      • Fgl-object
      • Fgl-solving
      • Fgl-handling-if-then-elses
      • Fgl-getting-bits-from-objects
      • Fgl-primitive-and-meta-rules
      • Fgl-interpreter-overview
      • Fgl-counterexamples
      • Fgl-correctness-of-binding-free-variables
      • Fgl-debugging
      • Fgl-testbenches
      • Def-fgl-boolean-constraint
      • Fgl-stack
      • Fgl-rewrite-tracing
      • Def-fgl-param-thm
      • Def-fgl-thm
      • Fgl-fast-alist-support
      • Advanced-equivalence-checking-with-fgl
      • Fgl-array-support
      • Fgl-internals
    • Bdd
    • Remove-hyps
    • Contextual-rewriting
    • Simp
    • Rewrite$-hyps
    • Bash-term-to-dnf
    • Use-trivial-ancestors-check
    • Minimal-runes
    • Clause-processor-tools
    • Fn-is-body
    • Without-subsumption
    • Rewrite-equiv-hint
    • Def-bounds
    • Rewrite$-context
    • Try-gl-concls
    • Hint-utils
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Fgl

Fgl-function-mode

Limitations on what the FGL interpreter will do to resolve a call of a given function.

This is a bitstruct type introduced by fty::defbitstruct, represented as a unsigned 6-bit integer.

Fields

split-ifs — boolean

If true, when the function is applied to arguments represented as g-ite objects, the FGL interpreter will first split into cases for all combinations of g-ite branches. Generally this should be set for functions that resolve via rewrite rules and false for functions that resolve via definition expansion.

dont-concrete-exec — boolean

If true, skip attempting to concretely execute the function in the case when all the arguments are explicit.

dont-expand-def — boolean

If true, skip expanding the function's definition after attempting ~ rewrites and primitive execution.

dont-rewrite — boolean

If true, skip applying rewrite rules to calls of the function.

dont-rewrite-under-if-test — boolean

If true, skip applying rewrite rules to calls of the function when trying to resolve an IF test to a Boolean formula.

dont-primitive-exec — boolean

If true, skip applying primitives to calls of the function.

Definitions and Theorems

Function: fgl-function-mode-p

(defun fgl-function-mode-p (x)
       (declare (xargs :guard t))
       (let ((__function__ 'fgl-function-mode-p))
            (declare (ignorable __function__))
            (mbe :logic (unsigned-byte-p 6 x)
                 :exec (and (natp x) (< x 64)))))

Theorem: fgl-function-mode-p-when-unsigned-byte-p

(defthm fgl-function-mode-p-when-unsigned-byte-p
        (implies (unsigned-byte-p 6 x)
                 (fgl-function-mode-p x)))

Theorem: unsigned-byte-p-when-fgl-function-mode-p

(defthm unsigned-byte-p-when-fgl-function-mode-p
        (implies (fgl-function-mode-p x)
                 (unsigned-byte-p 6 x)))

Theorem: fgl-function-mode-p-compound-recognizer

(defthm fgl-function-mode-p-compound-recognizer
        (implies (fgl-function-mode-p x)
                 (natp x))
        :rule-classes :compound-recognizer)

Function: fgl-function-mode-fix

(defun fgl-function-mode-fix (x)
       (declare (xargs :guard (fgl-function-mode-p x)))
       (let ((__function__ 'fgl-function-mode-fix))
            (declare (ignorable __function__))
            (mbe :logic (loghead 6 x) :exec x)))

Theorem: fgl-function-mode-p-of-fgl-function-mode-fix

(defthm fgl-function-mode-p-of-fgl-function-mode-fix
        (b* ((fty::fixed (fgl-function-mode-fix x)))
            (fgl-function-mode-p fty::fixed))
        :rule-classes :rewrite)

Theorem: fgl-function-mode-fix-when-fgl-function-mode-p

(defthm fgl-function-mode-fix-when-fgl-function-mode-p
        (implies (fgl-function-mode-p x)
                 (equal (fgl-function-mode-fix x) x)))

Function: fgl-function-mode-equiv$inline

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

Theorem: fgl-function-mode-equiv-is-an-equivalence

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

Theorem: fgl-function-mode-equiv-implies-equal-fgl-function-mode-fix-1

(defthm
     fgl-function-mode-equiv-implies-equal-fgl-function-mode-fix-1
     (implies (fgl-function-mode-equiv x x-equiv)
              (equal (fgl-function-mode-fix x)
                     (fgl-function-mode-fix x-equiv)))
     :rule-classes (:congruence))

Theorem: fgl-function-mode-fix-under-fgl-function-mode-equiv

(defthm fgl-function-mode-fix-under-fgl-function-mode-equiv
        (fgl-function-mode-equiv (fgl-function-mode-fix x)
                                 x)
        :rule-classes (:rewrite :rewrite-quoted-constant))

Function: fgl-function-mode

(defun
 fgl-function-mode
 (split-ifs dont-concrete-exec dont-expand-def
            dont-rewrite dont-rewrite-under-if-test
            dont-primitive-exec)
 (declare (xargs :guard (and (booleanp split-ifs)
                             (booleanp dont-concrete-exec)
                             (booleanp dont-expand-def)
                             (booleanp dont-rewrite)
                             (booleanp dont-rewrite-under-if-test)
                             (booleanp dont-primitive-exec))))
 (let
  ((__function__ 'fgl-function-mode))
  (declare (ignorable __function__))
  (b*
   ((split-ifs (bool->bit split-ifs))
    (dont-concrete-exec (bool->bit dont-concrete-exec))
    (dont-expand-def (bool->bit dont-expand-def))
    (dont-rewrite (bool->bit dont-rewrite))
    (dont-rewrite-under-if-test
         (bool->bit dont-rewrite-under-if-test))
    (dont-primitive-exec (bool->bit dont-primitive-exec)))
   (logapp
        1 split-ifs
        (logapp 1 dont-concrete-exec
                (logapp 1 dont-expand-def
                        (logapp 1 dont-rewrite
                                (logapp 1 dont-rewrite-under-if-test
                                        dont-primitive-exec))))))))

Theorem: fgl-function-mode-p-of-fgl-function-mode

(defthm
 fgl-function-mode-p-of-fgl-function-mode
 (b*
    ((fgl-function-mode
          (fgl-function-mode split-ifs
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec)))
    (fgl-function-mode-p fgl-function-mode))
 :rule-classes :rewrite)

Theorem: fgl-function-mode-of-bool-fix-split-ifs

(defthm
   fgl-function-mode-of-bool-fix-split-ifs
   (equal (fgl-function-mode (bool-fix split-ifs)
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec)
          (fgl-function-mode split-ifs
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec)))

Theorem: fgl-function-mode-iff-congruence-on-split-ifs

(defthm
 fgl-function-mode-iff-congruence-on-split-ifs
 (implies
   (iff split-ifs split-ifs-equiv)
   (equal (fgl-function-mode split-ifs
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec)
          (fgl-function-mode split-ifs-equiv
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec)))
 :rule-classes :congruence)

Theorem: fgl-function-mode-of-bool-fix-dont-concrete-exec

(defthm
   fgl-function-mode-of-bool-fix-dont-concrete-exec
   (equal (fgl-function-mode split-ifs (bool-fix dont-concrete-exec)
                             dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec)
          (fgl-function-mode split-ifs
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec)))

Theorem: fgl-function-mode-iff-congruence-on-dont-concrete-exec

(defthm
 fgl-function-mode-iff-congruence-on-dont-concrete-exec
 (implies
  (iff dont-concrete-exec
       dont-concrete-exec-equiv)
  (equal (fgl-function-mode split-ifs
                            dont-concrete-exec dont-expand-def
                            dont-rewrite dont-rewrite-under-if-test
                            dont-primitive-exec)
         (fgl-function-mode split-ifs
                            dont-concrete-exec-equiv dont-expand-def
                            dont-rewrite dont-rewrite-under-if-test
                            dont-primitive-exec)))
 :rule-classes :congruence)

Theorem: fgl-function-mode-of-bool-fix-dont-expand-def

(defthm
   fgl-function-mode-of-bool-fix-dont-expand-def
   (equal (fgl-function-mode split-ifs dont-concrete-exec
                             (bool-fix dont-expand-def)
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec)
          (fgl-function-mode split-ifs
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec)))

Theorem: fgl-function-mode-iff-congruence-on-dont-expand-def

(defthm
 fgl-function-mode-iff-congruence-on-dont-expand-def
 (implies
  (iff dont-expand-def dont-expand-def-equiv)
  (equal (fgl-function-mode split-ifs
                            dont-concrete-exec dont-expand-def
                            dont-rewrite dont-rewrite-under-if-test
                            dont-primitive-exec)
         (fgl-function-mode split-ifs
                            dont-concrete-exec dont-expand-def-equiv
                            dont-rewrite dont-rewrite-under-if-test
                            dont-primitive-exec)))
 :rule-classes :congruence)

Theorem: fgl-function-mode-of-bool-fix-dont-rewrite

(defthm
   fgl-function-mode-of-bool-fix-dont-rewrite
   (equal (fgl-function-mode split-ifs dont-concrete-exec
                             dont-expand-def (bool-fix dont-rewrite)
                             dont-rewrite-under-if-test
                             dont-primitive-exec)
          (fgl-function-mode split-ifs
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec)))

Theorem: fgl-function-mode-iff-congruence-on-dont-rewrite

(defthm
 fgl-function-mode-iff-congruence-on-dont-rewrite
 (implies
   (iff dont-rewrite dont-rewrite-equiv)
   (equal (fgl-function-mode split-ifs
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec)
          (fgl-function-mode split-ifs dont-concrete-exec
                             dont-expand-def dont-rewrite-equiv
                             dont-rewrite-under-if-test
                             dont-primitive-exec)))
 :rule-classes :congruence)

Theorem: fgl-function-mode-of-bool-fix-dont-rewrite-under-if-test

(defthm
   fgl-function-mode-of-bool-fix-dont-rewrite-under-if-test
   (equal (fgl-function-mode split-ifs dont-concrete-exec
                             dont-expand-def dont-rewrite
                             (bool-fix dont-rewrite-under-if-test)
                             dont-primitive-exec)
          (fgl-function-mode split-ifs
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec)))

Theorem: fgl-function-mode-iff-congruence-on-dont-rewrite-under-if-test

(defthm
 fgl-function-mode-iff-congruence-on-dont-rewrite-under-if-test
 (implies
   (iff dont-rewrite-under-if-test
        dont-rewrite-under-if-test-equiv)
   (equal (fgl-function-mode split-ifs
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec)
          (fgl-function-mode split-ifs dont-concrete-exec
                             dont-expand-def dont-rewrite
                             dont-rewrite-under-if-test-equiv
                             dont-primitive-exec)))
 :rule-classes :congruence)

Theorem: fgl-function-mode-of-bool-fix-dont-primitive-exec

(defthm
   fgl-function-mode-of-bool-fix-dont-primitive-exec
   (equal (fgl-function-mode split-ifs
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             (bool-fix dont-primitive-exec))
          (fgl-function-mode split-ifs
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec)))

Theorem: fgl-function-mode-iff-congruence-on-dont-primitive-exec

(defthm
 fgl-function-mode-iff-congruence-on-dont-primitive-exec
 (implies
   (iff dont-primitive-exec
        dont-primitive-exec-equiv)
   (equal (fgl-function-mode split-ifs
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec)
          (fgl-function-mode split-ifs
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec-equiv)))
 :rule-classes :congruence)

Function: fgl-function-mode-equiv-under-mask

(defun fgl-function-mode-equiv-under-mask
       (x x1 mask)
       (declare (xargs :guard (and (fgl-function-mode-p x)
                                   (fgl-function-mode-p x1)
                                   (integerp mask))))
       (let ((__function__ 'fgl-function-mode-equiv-under-mask))
            (declare (ignorable __function__))
            (fty::int-equiv-under-mask (fgl-function-mode-fix x)
                                       (fgl-function-mode-fix x1)
                                       mask)))

Function: fgl-function-mode->split-ifs

(defun
 fgl-function-mode->split-ifs (x)
 (declare (xargs :guard (fgl-function-mode-p x)))
 (mbe :logic (let ((x (fgl-function-mode-fix x)))
                  (bit->bool (acl2::part-select x :low 0 :width 1)))
      :exec (bit->bool (the (unsigned-byte 1)
                            (logand (the (unsigned-byte 1) 1)
                                    (the (unsigned-byte 6) x))))))

Theorem: booleanp-of-fgl-function-mode->split-ifs

(defthm booleanp-of-fgl-function-mode->split-ifs
        (b* ((split-ifs (fgl-function-mode->split-ifs x)))
            (booleanp split-ifs))
        :rule-classes :rewrite)

Theorem: fgl-function-mode->split-ifs-of-fgl-function-mode-fix-x

(defthm
     fgl-function-mode->split-ifs-of-fgl-function-mode-fix-x
     (equal (fgl-function-mode->split-ifs (fgl-function-mode-fix x))
            (fgl-function-mode->split-ifs x)))

Theorem: fgl-function-mode->split-ifs-fgl-function-mode-equiv-congruence-on-x

(defthm
 fgl-function-mode->split-ifs-fgl-function-mode-equiv-congruence-on-x
 (implies (fgl-function-mode-equiv x x-equiv)
          (equal (fgl-function-mode->split-ifs x)
                 (fgl-function-mode->split-ifs x-equiv)))
 :rule-classes :congruence)

Theorem: fgl-function-mode->split-ifs-of-fgl-function-mode

(defthm
 fgl-function-mode->split-ifs-of-fgl-function-mode
 (equal
     (fgl-function-mode->split-ifs
          (fgl-function-mode split-ifs
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec))
     (bool-fix split-ifs)))

Theorem: fgl-function-mode->split-ifs-of-write-with-mask

(defthm
    fgl-function-mode->split-ifs-of-write-with-mask
    (implies (and (fty::bitstruct-read-over-write-hyps
                       x fgl-function-mode-equiv-under-mask)
                  (fgl-function-mode-equiv-under-mask x y fty::mask)
                  (equal (logand (lognot fty::mask) 1) 0))
             (equal (fgl-function-mode->split-ifs x)
                    (fgl-function-mode->split-ifs y))))

Function: fgl-function-mode->dont-concrete-exec

(defun
 fgl-function-mode->dont-concrete-exec
 (x)
 (declare (xargs :guard (fgl-function-mode-p x)))
 (mbe
     :logic (let ((x (fgl-function-mode-fix x)))
                 (bit->bool (acl2::part-select x :low 1 :width 1)))
     :exec
     (bit->bool
          (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 5)
                            (ash (the (unsigned-byte 6) x) -1)))))))

Theorem: booleanp-of-fgl-function-mode->dont-concrete-exec

(defthm
 booleanp-of-fgl-function-mode->dont-concrete-exec
 (b*
    ((dont-concrete-exec (fgl-function-mode->dont-concrete-exec x)))
    (booleanp dont-concrete-exec))
 :rule-classes :rewrite)

Theorem: fgl-function-mode->dont-concrete-exec-of-fgl-function-mode-fix-x

(defthm
 fgl-function-mode->dont-concrete-exec-of-fgl-function-mode-fix-x
 (equal
   (fgl-function-mode->dont-concrete-exec (fgl-function-mode-fix x))
   (fgl-function-mode->dont-concrete-exec x)))

Theorem: fgl-function-mode->dont-concrete-exec-fgl-function-mode-equiv-congruence-on-x

(defthm
 fgl-function-mode->dont-concrete-exec-fgl-function-mode-equiv-congruence-on-x
 (implies (fgl-function-mode-equiv x x-equiv)
          (equal (fgl-function-mode->dont-concrete-exec x)
                 (fgl-function-mode->dont-concrete-exec x-equiv)))
 :rule-classes :congruence)

Theorem: fgl-function-mode->dont-concrete-exec-of-fgl-function-mode

(defthm
 fgl-function-mode->dont-concrete-exec-of-fgl-function-mode
 (equal
     (fgl-function-mode->dont-concrete-exec
          (fgl-function-mode split-ifs
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec))
     (bool-fix dont-concrete-exec)))

Theorem: fgl-function-mode->dont-concrete-exec-of-write-with-mask

(defthm
    fgl-function-mode->dont-concrete-exec-of-write-with-mask
    (implies (and (fty::bitstruct-read-over-write-hyps
                       x fgl-function-mode-equiv-under-mask)
                  (fgl-function-mode-equiv-under-mask x y fty::mask)
                  (equal (logand (lognot fty::mask) 2) 0))
             (equal (fgl-function-mode->dont-concrete-exec x)
                    (fgl-function-mode->dont-concrete-exec y))))

Function: fgl-function-mode->dont-expand-def

(defun
 fgl-function-mode->dont-expand-def (x)
 (declare (xargs :guard (fgl-function-mode-p x)))
 (mbe
     :logic (let ((x (fgl-function-mode-fix x)))
                 (bit->bool (acl2::part-select x :low 2 :width 1)))
     :exec
     (bit->bool
          (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 4)
                            (ash (the (unsigned-byte 6) x) -2)))))))

Theorem: booleanp-of-fgl-function-mode->dont-expand-def

(defthm
     booleanp-of-fgl-function-mode->dont-expand-def
     (b* ((dont-expand-def (fgl-function-mode->dont-expand-def x)))
         (booleanp dont-expand-def))
     :rule-classes :rewrite)

Theorem: fgl-function-mode->dont-expand-def-of-fgl-function-mode-fix-x

(defthm
 fgl-function-mode->dont-expand-def-of-fgl-function-mode-fix-x
 (equal
      (fgl-function-mode->dont-expand-def (fgl-function-mode-fix x))
      (fgl-function-mode->dont-expand-def x)))

Theorem: fgl-function-mode->dont-expand-def-fgl-function-mode-equiv-congruence-on-x

(defthm
 fgl-function-mode->dont-expand-def-fgl-function-mode-equiv-congruence-on-x
 (implies (fgl-function-mode-equiv x x-equiv)
          (equal (fgl-function-mode->dont-expand-def x)
                 (fgl-function-mode->dont-expand-def x-equiv)))
 :rule-classes :congruence)

Theorem: fgl-function-mode->dont-expand-def-of-fgl-function-mode

(defthm
 fgl-function-mode->dont-expand-def-of-fgl-function-mode
 (equal
     (fgl-function-mode->dont-expand-def
          (fgl-function-mode split-ifs
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec))
     (bool-fix dont-expand-def)))

Theorem: fgl-function-mode->dont-expand-def-of-write-with-mask

(defthm
    fgl-function-mode->dont-expand-def-of-write-with-mask
    (implies (and (fty::bitstruct-read-over-write-hyps
                       x fgl-function-mode-equiv-under-mask)
                  (fgl-function-mode-equiv-under-mask x y fty::mask)
                  (equal (logand (lognot fty::mask) 4) 0))
             (equal (fgl-function-mode->dont-expand-def x)
                    (fgl-function-mode->dont-expand-def y))))

Function: fgl-function-mode->dont-rewrite

(defun
 fgl-function-mode->dont-rewrite (x)
 (declare (xargs :guard (fgl-function-mode-p x)))
 (mbe
     :logic (let ((x (fgl-function-mode-fix x)))
                 (bit->bool (acl2::part-select x :low 3 :width 1)))
     :exec
     (bit->bool
          (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 3)
                            (ash (the (unsigned-byte 6) x) -3)))))))

Theorem: booleanp-of-fgl-function-mode->dont-rewrite

(defthm booleanp-of-fgl-function-mode->dont-rewrite
        (b* ((dont-rewrite (fgl-function-mode->dont-rewrite x)))
            (booleanp dont-rewrite))
        :rule-classes :rewrite)

Theorem: fgl-function-mode->dont-rewrite-of-fgl-function-mode-fix-x

(defthm
  fgl-function-mode->dont-rewrite-of-fgl-function-mode-fix-x
  (equal (fgl-function-mode->dont-rewrite (fgl-function-mode-fix x))
         (fgl-function-mode->dont-rewrite x)))

Theorem: fgl-function-mode->dont-rewrite-fgl-function-mode-equiv-congruence-on-x

(defthm
 fgl-function-mode->dont-rewrite-fgl-function-mode-equiv-congruence-on-x
 (implies (fgl-function-mode-equiv x x-equiv)
          (equal (fgl-function-mode->dont-rewrite x)
                 (fgl-function-mode->dont-rewrite x-equiv)))
 :rule-classes :congruence)

Theorem: fgl-function-mode->dont-rewrite-of-fgl-function-mode

(defthm
 fgl-function-mode->dont-rewrite-of-fgl-function-mode
 (equal
     (fgl-function-mode->dont-rewrite
          (fgl-function-mode split-ifs
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec))
     (bool-fix dont-rewrite)))

Theorem: fgl-function-mode->dont-rewrite-of-write-with-mask

(defthm
    fgl-function-mode->dont-rewrite-of-write-with-mask
    (implies (and (fty::bitstruct-read-over-write-hyps
                       x fgl-function-mode-equiv-under-mask)
                  (fgl-function-mode-equiv-under-mask x y fty::mask)
                  (equal (logand (lognot fty::mask) 8) 0))
             (equal (fgl-function-mode->dont-rewrite x)
                    (fgl-function-mode->dont-rewrite y))))

Function: fgl-function-mode->dont-rewrite-under-if-test

(defun
 fgl-function-mode->dont-rewrite-under-if-test
 (x)
 (declare (xargs :guard (fgl-function-mode-p x)))
 (mbe
     :logic (let ((x (fgl-function-mode-fix x)))
                 (bit->bool (acl2::part-select x :low 4 :width 1)))
     :exec
     (bit->bool
          (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 2)
                            (ash (the (unsigned-byte 6) x) -4)))))))

Theorem: booleanp-of-fgl-function-mode->dont-rewrite-under-if-test

(defthm
     booleanp-of-fgl-function-mode->dont-rewrite-under-if-test
     (b* ((dont-rewrite-under-if-test
               (fgl-function-mode->dont-rewrite-under-if-test x)))
         (booleanp dont-rewrite-under-if-test))
     :rule-classes :rewrite)

Theorem: fgl-function-mode->dont-rewrite-under-if-test-of-fgl-function-mode-fix-x

(defthm
 fgl-function-mode->dont-rewrite-under-if-test-of-fgl-function-mode-fix-x
 (equal (fgl-function-mode->dont-rewrite-under-if-test
             (fgl-function-mode-fix x))
        (fgl-function-mode->dont-rewrite-under-if-test x)))

Theorem: fgl-function-mode->dont-rewrite-under-if-test-fgl-function-mode-equiv-congruence-on-x

(defthm
 fgl-function-mode->dont-rewrite-under-if-test-fgl-function-mode-equiv-congruence-on-x
 (implies
    (fgl-function-mode-equiv x x-equiv)
    (equal (fgl-function-mode->dont-rewrite-under-if-test x)
           (fgl-function-mode->dont-rewrite-under-if-test x-equiv)))
 :rule-classes :congruence)

Theorem: fgl-function-mode->dont-rewrite-under-if-test-of-fgl-function-mode

(defthm
 fgl-function-mode->dont-rewrite-under-if-test-of-fgl-function-mode
 (equal
     (fgl-function-mode->dont-rewrite-under-if-test
          (fgl-function-mode split-ifs
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec))
     (bool-fix dont-rewrite-under-if-test)))

Theorem: fgl-function-mode->dont-rewrite-under-if-test-of-write-with-mask

(defthm
    fgl-function-mode->dont-rewrite-under-if-test-of-write-with-mask
    (implies
         (and (fty::bitstruct-read-over-write-hyps
                   x fgl-function-mode-equiv-under-mask)
              (fgl-function-mode-equiv-under-mask x y fty::mask)
              (equal (logand (lognot fty::mask) 16)
                     0))
         (equal (fgl-function-mode->dont-rewrite-under-if-test x)
                (fgl-function-mode->dont-rewrite-under-if-test y))))

Function: fgl-function-mode->dont-primitive-exec

(defun
 fgl-function-mode->dont-primitive-exec
 (x)
 (declare (xargs :guard (fgl-function-mode-p x)))
 (mbe
     :logic (let ((x (fgl-function-mode-fix x)))
                 (bit->bool (acl2::part-select x :low 5 :width 1)))
     :exec
     (bit->bool
          (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 1)
                            (ash (the (unsigned-byte 6) x) -5)))))))

Theorem: booleanp-of-fgl-function-mode->dont-primitive-exec

(defthm
 booleanp-of-fgl-function-mode->dont-primitive-exec
 (b*
  ((dont-primitive-exec (fgl-function-mode->dont-primitive-exec x)))
  (booleanp dont-primitive-exec))
 :rule-classes :rewrite)

Theorem: fgl-function-mode->dont-primitive-exec-of-fgl-function-mode-fix-x

(defthm
 fgl-function-mode->dont-primitive-exec-of-fgl-function-mode-fix-x
 (equal
  (fgl-function-mode->dont-primitive-exec (fgl-function-mode-fix x))
  (fgl-function-mode->dont-primitive-exec x)))

Theorem: fgl-function-mode->dont-primitive-exec-fgl-function-mode-equiv-congruence-on-x

(defthm
 fgl-function-mode->dont-primitive-exec-fgl-function-mode-equiv-congruence-on-x
 (implies (fgl-function-mode-equiv x x-equiv)
          (equal (fgl-function-mode->dont-primitive-exec x)
                 (fgl-function-mode->dont-primitive-exec x-equiv)))
 :rule-classes :congruence)

Theorem: fgl-function-mode->dont-primitive-exec-of-fgl-function-mode

(defthm
 fgl-function-mode->dont-primitive-exec-of-fgl-function-mode
 (equal
     (fgl-function-mode->dont-primitive-exec
          (fgl-function-mode split-ifs
                             dont-concrete-exec dont-expand-def
                             dont-rewrite dont-rewrite-under-if-test
                             dont-primitive-exec))
     (bool-fix dont-primitive-exec)))

Theorem: fgl-function-mode->dont-primitive-exec-of-write-with-mask

(defthm
    fgl-function-mode->dont-primitive-exec-of-write-with-mask
    (implies (and (fty::bitstruct-read-over-write-hyps
                       x fgl-function-mode-equiv-under-mask)
                  (fgl-function-mode-equiv-under-mask x y fty::mask)
                  (equal (logand (lognot fty::mask) 32)
                         0))
             (equal (fgl-function-mode->dont-primitive-exec x)
                    (fgl-function-mode->dont-primitive-exec y))))

Theorem: fgl-function-mode-fix-in-terms-of-fgl-function-mode

(defthm fgl-function-mode-fix-in-terms-of-fgl-function-mode
        (equal (fgl-function-mode-fix x)
               (change-fgl-function-mode x)))

Function: !fgl-function-mode->split-ifs

(defun
     !fgl-function-mode->split-ifs
     (split-ifs x)
     (declare (xargs :guard (and (booleanp split-ifs)
                                 (fgl-function-mode-p x))))
     (mbe :logic (b* ((split-ifs (bool->bit split-ifs))
                      (x (fgl-function-mode-fix x)))
                     (acl2::part-install split-ifs x
                                         :width 1
                                         :low 0))
          :exec (the (unsigned-byte 6)
                     (logior (the (unsigned-byte 6)
                                  (logand (the (unsigned-byte 6) x)
                                          (the (signed-byte 2) -2)))
                             (the (unsigned-byte 1)
                                  (bool->bit split-ifs))))))

Theorem: fgl-function-mode-p-of-!fgl-function-mode->split-ifs

(defthm fgl-function-mode-p-of-!fgl-function-mode->split-ifs
        (b* ((new-x (!fgl-function-mode->split-ifs split-ifs x)))
            (fgl-function-mode-p new-x))
        :rule-classes :rewrite)

Theorem: !fgl-function-mode->split-ifs-of-bool-fix-split-ifs

(defthm !fgl-function-mode->split-ifs-of-bool-fix-split-ifs
        (equal (!fgl-function-mode->split-ifs (bool-fix split-ifs)
                                              x)
               (!fgl-function-mode->split-ifs split-ifs x)))

Theorem: !fgl-function-mode->split-ifs-iff-congruence-on-split-ifs

(defthm
 !fgl-function-mode->split-ifs-iff-congruence-on-split-ifs
 (implies (iff split-ifs split-ifs-equiv)
          (equal (!fgl-function-mode->split-ifs split-ifs x)
                 (!fgl-function-mode->split-ifs split-ifs-equiv x)))
 :rule-classes :congruence)

Theorem: !fgl-function-mode->split-ifs-of-fgl-function-mode-fix-x

(defthm !fgl-function-mode->split-ifs-of-fgl-function-mode-fix-x
        (equal (!fgl-function-mode->split-ifs
                    split-ifs (fgl-function-mode-fix x))
               (!fgl-function-mode->split-ifs split-ifs x)))

Theorem: !fgl-function-mode->split-ifs-fgl-function-mode-equiv-congruence-on-x

(defthm
 !fgl-function-mode->split-ifs-fgl-function-mode-equiv-congruence-on-x
 (implies (fgl-function-mode-equiv x x-equiv)
          (equal (!fgl-function-mode->split-ifs split-ifs x)
                 (!fgl-function-mode->split-ifs split-ifs x-equiv)))
 :rule-classes :congruence)

Theorem: !fgl-function-mode->split-ifs-is-fgl-function-mode

(defthm !fgl-function-mode->split-ifs-is-fgl-function-mode
        (equal (!fgl-function-mode->split-ifs split-ifs x)
               (change-fgl-function-mode x
                                         :split-ifs split-ifs)))

Theorem: fgl-function-mode->split-ifs-of-!fgl-function-mode->split-ifs

(defthm
     fgl-function-mode->split-ifs-of-!fgl-function-mode->split-ifs
     (b* ((?new-x (!fgl-function-mode->split-ifs split-ifs x)))
         (equal (fgl-function-mode->split-ifs new-x)
                (bool-fix split-ifs))))

Theorem: !fgl-function-mode->split-ifs-equiv-under-mask

(defthm !fgl-function-mode->split-ifs-equiv-under-mask
        (b* ((?new-x (!fgl-function-mode->split-ifs split-ifs x)))
            (fgl-function-mode-equiv-under-mask new-x x -2)))

Function: !fgl-function-mode->dont-concrete-exec

(defun
 !fgl-function-mode->dont-concrete-exec
 (dont-concrete-exec x)
 (declare (xargs :guard (and (booleanp dont-concrete-exec)
                             (fgl-function-mode-p x))))
 (mbe
   :logic (b* ((dont-concrete-exec (bool->bit dont-concrete-exec))
               (x (fgl-function-mode-fix x)))
              (acl2::part-install dont-concrete-exec x
                                  :width 1
                                  :low 1))
   :exec (the (unsigned-byte 6)
              (logior (the (unsigned-byte 6)
                           (logand (the (unsigned-byte 6) x)
                                   (the (signed-byte 3) -3)))
                      (the (unsigned-byte 2)
                           (ash (the (unsigned-byte 1)
                                     (bool->bit dont-concrete-exec))
                                1))))))

Theorem: fgl-function-mode-p-of-!fgl-function-mode->dont-concrete-exec

(defthm
 fgl-function-mode-p-of-!fgl-function-mode->dont-concrete-exec
 (b*
  ((new-x
     (!fgl-function-mode->dont-concrete-exec dont-concrete-exec x)))
  (fgl-function-mode-p new-x))
 :rule-classes :rewrite)

Theorem: !fgl-function-mode->dont-concrete-exec-of-bool-fix-dont-concrete-exec

(defthm
 !fgl-function-mode->dont-concrete-exec-of-bool-fix-dont-concrete-exec
 (equal
     (!fgl-function-mode->dont-concrete-exec
          (bool-fix dont-concrete-exec)
          x)
     (!fgl-function-mode->dont-concrete-exec dont-concrete-exec x)))

Theorem: !fgl-function-mode->dont-concrete-exec-iff-congruence-on-dont-concrete-exec

(defthm
 !fgl-function-mode->dont-concrete-exec-iff-congruence-on-dont-concrete-exec
 (implies
  (iff dont-concrete-exec
       dont-concrete-exec-equiv)
  (equal
       (!fgl-function-mode->dont-concrete-exec dont-concrete-exec x)
       (!fgl-function-mode->dont-concrete-exec
            dont-concrete-exec-equiv x)))
 :rule-classes :congruence)

Theorem: !fgl-function-mode->dont-concrete-exec-of-fgl-function-mode-fix-x

(defthm
 !fgl-function-mode->dont-concrete-exec-of-fgl-function-mode-fix-x
 (equal
  (!fgl-function-mode->dont-concrete-exec dont-concrete-exec
                                          (fgl-function-mode-fix x))
  (!fgl-function-mode->dont-concrete-exec dont-concrete-exec x)))

Theorem: !fgl-function-mode->dont-concrete-exec-fgl-function-mode-equiv-congruence-on-x

(defthm
 !fgl-function-mode->dont-concrete-exec-fgl-function-mode-equiv-congruence-on-x
 (implies
  (fgl-function-mode-equiv x x-equiv)
  (equal
       (!fgl-function-mode->dont-concrete-exec dont-concrete-exec x)
       (!fgl-function-mode->dont-concrete-exec
            dont-concrete-exec x-equiv)))
 :rule-classes :congruence)

Theorem: !fgl-function-mode->dont-concrete-exec-is-fgl-function-mode

(defthm
  !fgl-function-mode->dont-concrete-exec-is-fgl-function-mode
  (equal
       (!fgl-function-mode->dont-concrete-exec dont-concrete-exec x)
       (change-fgl-function-mode
            x
            :dont-concrete-exec dont-concrete-exec)))

Theorem: fgl-function-mode->dont-concrete-exec-of-!fgl-function-mode->dont-concrete-exec

(defthm
 fgl-function-mode->dont-concrete-exec-of-!fgl-function-mode->dont-concrete-exec
 (b*
  ((?new-x
     (!fgl-function-mode->dont-concrete-exec dont-concrete-exec x)))
  (equal (fgl-function-mode->dont-concrete-exec new-x)
         (bool-fix dont-concrete-exec))))

Theorem: !fgl-function-mode->dont-concrete-exec-equiv-under-mask

(defthm
 !fgl-function-mode->dont-concrete-exec-equiv-under-mask
 (b*
  ((?new-x
     (!fgl-function-mode->dont-concrete-exec dont-concrete-exec x)))
  (fgl-function-mode-equiv-under-mask new-x x -3)))

Function: !fgl-function-mode->dont-expand-def

(defun
 !fgl-function-mode->dont-expand-def
 (dont-expand-def x)
 (declare (xargs :guard (and (booleanp dont-expand-def)
                             (fgl-function-mode-p x))))
 (mbe :logic (b* ((dont-expand-def (bool->bit dont-expand-def))
                  (x (fgl-function-mode-fix x)))
                 (acl2::part-install dont-expand-def x
                                     :width 1
                                     :low 2))
      :exec (the (unsigned-byte 6)
                 (logior (the (unsigned-byte 6)
                              (logand (the (unsigned-byte 6) x)
                                      (the (signed-byte 4) -5)))
                         (the (unsigned-byte 3)
                              (ash (the (unsigned-byte 1)
                                        (bool->bit dont-expand-def))
                                   2))))))

Theorem: fgl-function-mode-p-of-!fgl-function-mode->dont-expand-def

(defthm
 fgl-function-mode-p-of-!fgl-function-mode->dont-expand-def
 (b*
   ((new-x (!fgl-function-mode->dont-expand-def dont-expand-def x)))
   (fgl-function-mode-p new-x))
 :rule-classes :rewrite)

Theorem: !fgl-function-mode->dont-expand-def-of-bool-fix-dont-expand-def

(defthm
 !fgl-function-mode->dont-expand-def-of-bool-fix-dont-expand-def
 (equal
     (!fgl-function-mode->dont-expand-def (bool-fix dont-expand-def)
                                          x)
     (!fgl-function-mode->dont-expand-def dont-expand-def x)))

Theorem: !fgl-function-mode->dont-expand-def-iff-congruence-on-dont-expand-def

(defthm
 !fgl-function-mode->dont-expand-def-iff-congruence-on-dont-expand-def
 (implies
  (iff dont-expand-def dont-expand-def-equiv)
  (equal
     (!fgl-function-mode->dont-expand-def dont-expand-def x)
     (!fgl-function-mode->dont-expand-def dont-expand-def-equiv x)))
 :rule-classes :congruence)

Theorem: !fgl-function-mode->dont-expand-def-of-fgl-function-mode-fix-x

(defthm
 !fgl-function-mode->dont-expand-def-of-fgl-function-mode-fix-x
 (equal
     (!fgl-function-mode->dont-expand-def dont-expand-def
                                          (fgl-function-mode-fix x))
     (!fgl-function-mode->dont-expand-def dont-expand-def x)))

Theorem: !fgl-function-mode->dont-expand-def-fgl-function-mode-equiv-congruence-on-x

(defthm
 !fgl-function-mode->dont-expand-def-fgl-function-mode-equiv-congruence-on-x
 (implies
  (fgl-function-mode-equiv x x-equiv)
  (equal
     (!fgl-function-mode->dont-expand-def dont-expand-def x)
     (!fgl-function-mode->dont-expand-def dont-expand-def x-equiv)))
 :rule-classes :congruence)

Theorem: !fgl-function-mode->dont-expand-def-is-fgl-function-mode

(defthm
  !fgl-function-mode->dont-expand-def-is-fgl-function-mode
  (equal
       (!fgl-function-mode->dont-expand-def dont-expand-def x)
       (change-fgl-function-mode x
                                 :dont-expand-def dont-expand-def)))

Theorem: fgl-function-mode->dont-expand-def-of-!fgl-function-mode->dont-expand-def

(defthm
 fgl-function-mode->dont-expand-def-of-!fgl-function-mode->dont-expand-def
 (b*
  ((?new-x (!fgl-function-mode->dont-expand-def dont-expand-def x)))
  (equal (fgl-function-mode->dont-expand-def new-x)
         (bool-fix dont-expand-def))))

Theorem: !fgl-function-mode->dont-expand-def-equiv-under-mask

(defthm
 !fgl-function-mode->dont-expand-def-equiv-under-mask
 (b*
  ((?new-x (!fgl-function-mode->dont-expand-def dont-expand-def x)))
  (fgl-function-mode-equiv-under-mask new-x x -5)))

Function: !fgl-function-mode->dont-rewrite

(defun
    !fgl-function-mode->dont-rewrite
    (dont-rewrite x)
    (declare (xargs :guard (and (booleanp dont-rewrite)
                                (fgl-function-mode-p x))))
    (mbe :logic (b* ((dont-rewrite (bool->bit dont-rewrite))
                     (x (fgl-function-mode-fix x)))
                    (acl2::part-install dont-rewrite x
                                        :width 1
                                        :low 3))
         :exec (the (unsigned-byte 6)
                    (logior (the (unsigned-byte 6)
                                 (logand (the (unsigned-byte 6) x)
                                         (the (signed-byte 5) -9)))
                            (the (unsigned-byte 4)
                                 (ash (the (unsigned-byte 1)
                                           (bool->bit dont-rewrite))
                                      3))))))

Theorem: fgl-function-mode-p-of-!fgl-function-mode->dont-rewrite

(defthm
     fgl-function-mode-p-of-!fgl-function-mode->dont-rewrite
     (b* ((new-x (!fgl-function-mode->dont-rewrite dont-rewrite x)))
         (fgl-function-mode-p new-x))
     :rule-classes :rewrite)

Theorem: !fgl-function-mode->dont-rewrite-of-bool-fix-dont-rewrite

(defthm
    !fgl-function-mode->dont-rewrite-of-bool-fix-dont-rewrite
    (equal (!fgl-function-mode->dont-rewrite (bool-fix dont-rewrite)
                                             x)
           (!fgl-function-mode->dont-rewrite dont-rewrite x)))

Theorem: !fgl-function-mode->dont-rewrite-iff-congruence-on-dont-rewrite

(defthm
 !fgl-function-mode->dont-rewrite-iff-congruence-on-dont-rewrite
 (implies
    (iff dont-rewrite dont-rewrite-equiv)
    (equal (!fgl-function-mode->dont-rewrite dont-rewrite x)
           (!fgl-function-mode->dont-rewrite dont-rewrite-equiv x)))
 :rule-classes :congruence)

Theorem: !fgl-function-mode->dont-rewrite-of-fgl-function-mode-fix-x

(defthm !fgl-function-mode->dont-rewrite-of-fgl-function-mode-fix-x
        (equal (!fgl-function-mode->dont-rewrite
                    dont-rewrite (fgl-function-mode-fix x))
               (!fgl-function-mode->dont-rewrite dont-rewrite x)))

Theorem: !fgl-function-mode->dont-rewrite-fgl-function-mode-equiv-congruence-on-x

(defthm
 !fgl-function-mode->dont-rewrite-fgl-function-mode-equiv-congruence-on-x
 (implies
    (fgl-function-mode-equiv x x-equiv)
    (equal (!fgl-function-mode->dont-rewrite dont-rewrite x)
           (!fgl-function-mode->dont-rewrite dont-rewrite x-equiv)))
 :rule-classes :congruence)

Theorem: !fgl-function-mode->dont-rewrite-is-fgl-function-mode

(defthm
     !fgl-function-mode->dont-rewrite-is-fgl-function-mode
     (equal (!fgl-function-mode->dont-rewrite dont-rewrite x)
            (change-fgl-function-mode x
                                      :dont-rewrite dont-rewrite)))

Theorem: fgl-function-mode->dont-rewrite-of-!fgl-function-mode->dont-rewrite

(defthm
 fgl-function-mode->dont-rewrite-of-!fgl-function-mode->dont-rewrite
 (b* ((?new-x (!fgl-function-mode->dont-rewrite dont-rewrite x)))
     (equal (fgl-function-mode->dont-rewrite new-x)
            (bool-fix dont-rewrite))))

Theorem: !fgl-function-mode->dont-rewrite-equiv-under-mask

(defthm
    !fgl-function-mode->dont-rewrite-equiv-under-mask
    (b* ((?new-x (!fgl-function-mode->dont-rewrite dont-rewrite x)))
        (fgl-function-mode-equiv-under-mask new-x x -9)))

Function: !fgl-function-mode->dont-rewrite-under-if-test

(defun
 !fgl-function-mode->dont-rewrite-under-if-test
 (dont-rewrite-under-if-test x)
 (declare (xargs :guard (and (booleanp dont-rewrite-under-if-test)
                             (fgl-function-mode-p x))))
 (mbe
  :logic (b* ((dont-rewrite-under-if-test
                   (bool->bit dont-rewrite-under-if-test))
              (x (fgl-function-mode-fix x)))
             (acl2::part-install dont-rewrite-under-if-test x
                                 :width 1
                                 :low 4))
  :exec
  (the
      (unsigned-byte 6)
      (logior (the (unsigned-byte 6)
                   (logand (the (unsigned-byte 6) x)
                           (the (signed-byte 6) -17)))
              (the (unsigned-byte 5)
                   (ash (the (unsigned-byte 1)
                             (bool->bit dont-rewrite-under-if-test))
                        4))))))

Theorem: fgl-function-mode-p-of-!fgl-function-mode->dont-rewrite-under-if-test

(defthm
 fgl-function-mode-p-of-!fgl-function-mode->dont-rewrite-under-if-test
 (b* ((new-x (!fgl-function-mode->dont-rewrite-under-if-test
                  dont-rewrite-under-if-test x)))
     (fgl-function-mode-p new-x))
 :rule-classes :rewrite)

Theorem: !fgl-function-mode->dont-rewrite-under-if-test-of-bool-fix-dont-rewrite-under-if-test

(defthm
 !fgl-function-mode->dont-rewrite-under-if-test-of-bool-fix-dont-rewrite-under-if-test
 (equal (!fgl-function-mode->dont-rewrite-under-if-test
             (bool-fix dont-rewrite-under-if-test)
             x)
        (!fgl-function-mode->dont-rewrite-under-if-test
             dont-rewrite-under-if-test x)))

Theorem: !fgl-function-mode->dont-rewrite-under-if-test-iff-congruence-on-dont-rewrite-under-if-test

(defthm
 !fgl-function-mode->dont-rewrite-under-if-test-iff-congruence-on-dont-rewrite-under-if-test
 (implies (iff dont-rewrite-under-if-test
               dont-rewrite-under-if-test-equiv)
          (equal (!fgl-function-mode->dont-rewrite-under-if-test
                      dont-rewrite-under-if-test x)
                 (!fgl-function-mode->dont-rewrite-under-if-test
                      dont-rewrite-under-if-test-equiv x)))
 :rule-classes :congruence)

Theorem: !fgl-function-mode->dont-rewrite-under-if-test-of-fgl-function-mode-fix-x

(defthm
 !fgl-function-mode->dont-rewrite-under-if-test-of-fgl-function-mode-fix-x
 (equal (!fgl-function-mode->dont-rewrite-under-if-test
             dont-rewrite-under-if-test
             (fgl-function-mode-fix x))
        (!fgl-function-mode->dont-rewrite-under-if-test
             dont-rewrite-under-if-test x)))

Theorem: !fgl-function-mode->dont-rewrite-under-if-test-fgl-function-mode-equiv-congruence-on-x

(defthm
 !fgl-function-mode->dont-rewrite-under-if-test-fgl-function-mode-equiv-congruence-on-x
 (implies (fgl-function-mode-equiv x x-equiv)
          (equal (!fgl-function-mode->dont-rewrite-under-if-test
                      dont-rewrite-under-if-test x)
                 (!fgl-function-mode->dont-rewrite-under-if-test
                      dont-rewrite-under-if-test x-equiv)))
 :rule-classes :congruence)

Theorem: !fgl-function-mode->dont-rewrite-under-if-test-is-fgl-function-mode

(defthm
 !fgl-function-mode->dont-rewrite-under-if-test-is-fgl-function-mode
 (equal
      (!fgl-function-mode->dont-rewrite-under-if-test
           dont-rewrite-under-if-test x)
      (change-fgl-function-mode
           x
           :dont-rewrite-under-if-test dont-rewrite-under-if-test)))

Theorem: fgl-function-mode->dont-rewrite-under-if-test-of-!fgl-function-mode->dont-rewrite-under-if-test

(defthm
 fgl-function-mode->dont-rewrite-under-if-test-of-!fgl-function-mode->dont-rewrite-under-if-test
 (b* ((?new-x (!fgl-function-mode->dont-rewrite-under-if-test
                   dont-rewrite-under-if-test x)))
     (equal (fgl-function-mode->dont-rewrite-under-if-test new-x)
            (bool-fix dont-rewrite-under-if-test))))

Theorem: !fgl-function-mode->dont-rewrite-under-if-test-equiv-under-mask

(defthm
     !fgl-function-mode->dont-rewrite-under-if-test-equiv-under-mask
     (b* ((?new-x (!fgl-function-mode->dont-rewrite-under-if-test
                       dont-rewrite-under-if-test x)))
         (fgl-function-mode-equiv-under-mask new-x x -17)))

Function: !fgl-function-mode->dont-primitive-exec

(defun
 !fgl-function-mode->dont-primitive-exec
 (dont-primitive-exec x)
 (declare (xargs :guard (and (booleanp dont-primitive-exec)
                             (fgl-function-mode-p x))))
 (mbe
  :logic (b* ((dont-primitive-exec (bool->bit dont-primitive-exec))
              (x (fgl-function-mode-fix x)))
             (acl2::part-install dont-primitive-exec x
                                 :width 1
                                 :low 5))
  :exec (the (unsigned-byte 6)
             (logior (the (unsigned-byte 6)
                          (logand (the (unsigned-byte 6) x)
                                  (the (signed-byte 7) -33)))
                     (the (unsigned-byte 6)
                          (ash (the (unsigned-byte 1)
                                    (bool->bit dont-primitive-exec))
                               5))))))

Theorem: fgl-function-mode-p-of-!fgl-function-mode->dont-primitive-exec

(defthm
     fgl-function-mode-p-of-!fgl-function-mode->dont-primitive-exec
     (b* ((new-x (!fgl-function-mode->dont-primitive-exec
                      dont-primitive-exec x)))
         (fgl-function-mode-p new-x))
     :rule-classes :rewrite)

Theorem: !fgl-function-mode->dont-primitive-exec-of-bool-fix-dont-primitive-exec

(defthm
 !fgl-function-mode->dont-primitive-exec-of-bool-fix-dont-primitive-exec
 (equal
   (!fgl-function-mode->dont-primitive-exec
        (bool-fix dont-primitive-exec)
        x)
   (!fgl-function-mode->dont-primitive-exec dont-primitive-exec x)))

Theorem: !fgl-function-mode->dont-primitive-exec-iff-congruence-on-dont-primitive-exec

(defthm
 !fgl-function-mode->dont-primitive-exec-iff-congruence-on-dont-primitive-exec
 (implies
  (iff dont-primitive-exec
       dont-primitive-exec-equiv)
  (equal
     (!fgl-function-mode->dont-primitive-exec dont-primitive-exec x)
     (!fgl-function-mode->dont-primitive-exec
          dont-primitive-exec-equiv x)))
 :rule-classes :congruence)

Theorem: !fgl-function-mode->dont-primitive-exec-of-fgl-function-mode-fix-x

(defthm
 !fgl-function-mode->dont-primitive-exec-of-fgl-function-mode-fix-x
 (equal
   (!fgl-function-mode->dont-primitive-exec
        dont-primitive-exec
        (fgl-function-mode-fix x))
   (!fgl-function-mode->dont-primitive-exec dont-primitive-exec x)))

Theorem: !fgl-function-mode->dont-primitive-exec-fgl-function-mode-equiv-congruence-on-x

(defthm
 !fgl-function-mode->dont-primitive-exec-fgl-function-mode-equiv-congruence-on-x
 (implies
  (fgl-function-mode-equiv x x-equiv)
  (equal
     (!fgl-function-mode->dont-primitive-exec dont-primitive-exec x)
     (!fgl-function-mode->dont-primitive-exec
          dont-primitive-exec x-equiv)))
 :rule-classes :congruence)

Theorem: !fgl-function-mode->dont-primitive-exec-is-fgl-function-mode

(defthm
 !fgl-function-mode->dont-primitive-exec-is-fgl-function-mode
 (equal
     (!fgl-function-mode->dont-primitive-exec dont-primitive-exec x)
     (change-fgl-function-mode
          x
          :dont-primitive-exec dont-primitive-exec)))

Theorem: fgl-function-mode->dont-primitive-exec-of-!fgl-function-mode->dont-primitive-exec

(defthm
 fgl-function-mode->dont-primitive-exec-of-!fgl-function-mode->dont-primitive-exec
 (b* ((?new-x (!fgl-function-mode->dont-primitive-exec
                   dont-primitive-exec x)))
     (equal (fgl-function-mode->dont-primitive-exec new-x)
            (bool-fix dont-primitive-exec))))

Theorem: !fgl-function-mode->dont-primitive-exec-equiv-under-mask

(defthm !fgl-function-mode->dont-primitive-exec-equiv-under-mask
        (b* ((?new-x (!fgl-function-mode->dont-primitive-exec
                          dont-primitive-exec x)))
            (fgl-function-mode-equiv-under-mask new-x x 31)))

Function: fgl-function-mode-debug

(defun
 fgl-function-mode-debug (x)
 (declare (xargs :guard (fgl-function-mode-p x)))
 (let
  ((__function__ 'fgl-function-mode-debug))
  (declare (ignorable __function__))
  (b*
   (((fgl-function-mode x)))
   (cons (cons 'split-ifs x.split-ifs)
         (cons (cons 'dont-concrete-exec
                     x.dont-concrete-exec)
               (cons (cons 'dont-expand-def
                           x.dont-expand-def)
                     (cons (cons 'dont-rewrite x.dont-rewrite)
                           (cons (cons 'dont-rewrite-under-if-test
                                       x.dont-rewrite-under-if-test)
                                 (cons (cons 'dont-primitive-exec
                                             x.dont-primitive-exec)
                                       nil)))))))))

Subtopics

!fgl-function-mode->dont-rewrite-under-if-test

Update the |FGL|::|DONT-REWRITE-UNDER-IF-TEST| field of a fgl-function-mode bit structure.

!fgl-function-mode->dont-primitive-exec

Update the |FGL|::|DONT-PRIMITIVE-EXEC| field of a fgl-function-mode bit structure.

!fgl-function-mode->dont-concrete-exec

Update the |FGL|::|DONT-CONCRETE-EXEC| field of a fgl-function-mode bit structure.

!fgl-function-mode->dont-expand-def

Update the |FGL|::|DONT-EXPAND-DEF| field of a fgl-function-mode bit structure.

!fgl-function-mode->dont-rewrite

Update the |FGL|::|DONT-REWRITE| field of a fgl-function-mode bit structure.

!fgl-function-mode->split-ifs

Update the |FGL|::|SPLIT-IFS| field of a fgl-function-mode bit structure.

Fgl-function-mode->dont-rewrite-under-if-test

Access the |FGL|::|DONT-REWRITE-UNDER-IF-TEST| field of a fgl-function-mode bit structure.

Fgl-function-mode->dont-primitive-exec

Access the |FGL|::|DONT-PRIMITIVE-EXEC| field of a fgl-function-mode bit structure.

Fgl-function-mode->dont-concrete-exec

Access the |FGL|::|DONT-CONCRETE-EXEC| field of a fgl-function-mode bit structure.

Fgl-function-mode-p

Recognizer for fgl-function-mode bit structures.

Fgl-function-mode->dont-expand-def

Access the |FGL|::|DONT-EXPAND-DEF| field of a fgl-function-mode bit structure.

Fgl-function-mode->dont-rewrite

Access the |FGL|::|DONT-REWRITE| field of a fgl-function-mode bit structure.

Fgl-function-mode-fix

Fixing function for fgl-function-mode bit structures.

Fgl-function-mode->split-ifs

Access the |FGL|::|SPLIT-IFS| field of a fgl-function-mode bit structure.