		Search-engine friendly clone of the ACL2 documentation.

Fgl-config

Fgl-config->sat-config

Get the sat-config field from a fgl-config.

Signature
(fgl-config->sat-config x) → fty::x.name
Arguments: x — Guard (fgl-config-p x).

This is an ordinary field accessor created by defprod.

Definitions and Theorems

Function: fgl-config->sat-config$inline

(defun
 fgl-config->sat-config$inline (x)
 (declare (xargs :guard (fgl-config-p x)))
 (declare (xargs :guard t))
 (let
  ((__function__ 'fgl-config->sat-config))
  (declare (ignorable __function__))
  (mbe
    :logic
    (b* ((x (and t x)))
        (std::prod-cdr
             (std::prod-cdr (std::prod-car (std::prod-cdr x)))))
    :exec (std::prod-cdr
               (std::prod-cdr (std::prod-car (std::prod-cdr x)))))))

Theorem: fgl-config->sat-config$inline-of-fgl-config-fix-x

(defthm fgl-config->sat-config$inline-of-fgl-config-fix-x
        (equal (fgl-config->sat-config$inline (fgl-config-fix x))
               (fgl-config->sat-config$inline x)))

Theorem: fgl-config->sat-config$inline-fgl-config-equiv-congruence-on-x

(defthm
     fgl-config->sat-config$inline-fgl-config-equiv-congruence-on-x
     (implies (fgl-config-equiv x x-equiv)
              (equal (fgl-config->sat-config$inline x)
                     (fgl-config->sat-config$inline x-equiv)))
     :rule-classes :congruence)