		Search-engine friendly clone of the ACL2 documentation.

Group-literal-product

Group-literal-product->factor

Get the factor field from a group-literal-product.

Signature
(group-literal-product->factor lit) → factor
Arguments: lit — Guard (group-literalp lit).
Returns: factor — Type (natp factor).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: group-literal-product->factor$inline

(defun group-literal-product->factor$inline (lit)
  (declare (xargs :guard (group-literalp lit)))
  (declare (xargs :guard (equal (group-literal-kind lit)
                                :product)))
  (let ((__function__ 'group-literal-product->factor))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((lit (and (equal (group-literal-kind lit)
                               :product)
                        lit)))
           (nfix (std::da-nth 0 (cdr lit))))
         :exec (std::da-nth 0 (cdr lit)))))

Theorem: natp-of-group-literal-product->factor

(defthm natp-of-group-literal-product->factor
  (b* ((factor (group-literal-product->factor$inline lit)))
    (natp factor))
  :rule-classes :rewrite)

Theorem: group-literal-product->factor$inline-of-group-literal-fix-lit

(defthm
      group-literal-product->factor$inline-of-group-literal-fix-lit
 (equal
      (group-literal-product->factor$inline (group-literal-fix lit))
      (group-literal-product->factor$inline lit)))

Theorem: group-literal-product->factor$inline-group-literal-equiv-congruence-on-lit

(defthm
 group-literal-product->factor$inline-group-literal-equiv-congruence-on-lit
 (implies (group-literal-equiv lit lit-equiv)
          (equal (group-literal-product->factor$inline lit)
                 (group-literal-product->factor$inline lit-equiv)))
 :rule-classes :congruence)

Theorem: group-literal-product->factor-when-wrong-kind

(defthm group-literal-product->factor-when-wrong-kind
  (implies (not (equal (group-literal-kind lit)
                       :product))
           (equal (group-literal-product->factor lit)
                  (nfix nil))))