		Search-engine friendly clone of the ACL2 documentation.

Field-div-flagged

Field-div-flagged-circuit

Construction of the circuit.

Signature
(field-div-flagged-circuit) → pdef
Returns: pdef — Type (pfcs::definitionp pdef).

This is a PFCS definition with the three equality constraints described in field-div-flagged.

Definitions and Theorems

Function: field-div-flagged-circuit

(defun field-div-flagged-circuit nil
 (declare (xargs :guard t))
 (let ((__function__ 'field-div-flagged-circuit))
  (declare (ignorable __function__))
  (pfcs::parse-def
   "field_div_flagged(x,y,z,e) := {
    (y) * (w) == (1 - e),
    (y) * (e) == (0),
    (x) * (w) == (z),
    (z) * (e) == (0)
    }")))

Theorem: definitionp-of-field-div-flagged-circuit

(defthm definitionp-of-field-div-flagged-circuit
  (b* ((pdef (field-div-flagged-circuit)))
    (pfcs::definitionp pdef))
  :rule-classes :rewrite)

Theorem: sr1cs-definitionp-of-field-div-flagged-circuit

(defthm sr1cs-definitionp-of-field-div-flagged-circuit
  (b* ((pdef (field-div-flagged-circuit)))
    (pfcs::sr1cs-definitionp pdef))
  :rule-classes :rewrite)