`(rulename-sfix x)` is a usual ACL2::fty set fixing function.

- Signature
(rulename-sfix x) → *

- Arguments
`x`—Guard (rulename-setp x) .

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

**Function: **

(defun rulename-sfix (x) (declare (xargs :guard (rulename-setp x))) (mbe :logic (if (rulename-setp x) x nil) :exec x))

**Theorem: **

(defthm rulename-setp-of-rulename-sfix (rulename-setp (rulename-sfix x)))

**Theorem: **

(defthm rulename-sfix-when-rulename-setp (implies (rulename-setp x) (equal (rulename-sfix x) x)))

**Theorem: **

(defthm emptyp-rulename-sfix (implies (or (emptyp x) (not (rulename-setp x))) (emptyp (rulename-sfix x))))

**Function: **

(defun rulename-sequiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (rulename-setp acl2::x) (rulename-setp acl2::y)))) (equal (rulename-sfix acl2::x) (rulename-sfix acl2::y)))

**Theorem: **

(defthm rulename-sequiv-is-an-equivalence (and (booleanp (rulename-sequiv x y)) (rulename-sequiv x x) (implies (rulename-sequiv x y) (rulename-sequiv y x)) (implies (and (rulename-sequiv x y) (rulename-sequiv y z)) (rulename-sequiv x z))) :rule-classes (:equivalence))

**Theorem: **

(defthm rulename-sequiv-implies-equal-rulename-sfix-1 (implies (rulename-sequiv acl2::x x-equiv) (equal (rulename-sfix acl2::x) (rulename-sfix x-equiv))) :rule-classes (:congruence))

**Theorem: **

(defthm rulename-sfix-under-rulename-sequiv (rulename-sequiv (rulename-sfix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))

**Theorem: **

(defthm equal-of-rulename-sfix-1-forward-to-rulename-sequiv (implies (equal (rulename-sfix acl2::x) acl2::y) (rulename-sequiv acl2::x acl2::y)) :rule-classes :forward-chaining)

**Theorem: **

(defthm equal-of-rulename-sfix-2-forward-to-rulename-sequiv (implies (equal acl2::x (rulename-sfix acl2::y)) (rulename-sequiv acl2::x acl2::y)) :rule-classes :forward-chaining)

**Theorem: **

(defthm rulename-sequiv-of-rulename-sfix-1-forward (implies (rulename-sequiv (rulename-sfix acl2::x) acl2::y) (rulename-sequiv acl2::x acl2::y)) :rule-classes :forward-chaining)

**Theorem: **

(defthm rulename-sequiv-of-rulename-sfix-2-forward (implies (rulename-sequiv acl2::x (rulename-sfix acl2::y)) (rulename-sequiv acl2::x acl2::y)) :rule-classes :forward-chaining)