• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
    • Gl
    • Witness-cp
    • Ccg
    • Install-not-normalized
    • Rewrite$
    • Removable-runes
    • 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-expand-def
        • Fgl-function-mode->dont-concrete-exec
        • Fgl-function-mode-p
        • Fgl-function-mode->dont-rewrite
        • Fgl-function-mode->split-ifs
        • Fgl-function-mode-fix
      • 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
      • Fgl-array-support
      • Advanced-equivalence-checking-with-fgl
      • Fgl-internals
    • Efficiency
    • Rewrite-bounds
    • Bash
    • Def-dag-measure
    • 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
  • Math
  • Testing-utilities

• 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-expand-def

Access the |FGL|::|DONT-EXPAND-DEF| 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-rewrite

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

Fgl-function-mode->split-ifs

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

Fgl-function-mode-fix

Fixing function for fgl-function-mode bit structures.