		Search-engine friendly clone of the ACL2 documentation.

Truth

Is-xor-with-var

Checks whether the given truth table is the xor of variable n with something. If so, the other input to the xor is the negative cofactor of the truth table with n.

Signature
(is-xor-with-var n truth numvars) → *
Arguments: n — Guard (natp n).; truth — Guard (integerp truth).; numvars — Guard (natp numvars).

Definitions and Theorems

Function: is-xor-with-var

(defun
 is-xor-with-var (n truth numvars)
 (declare (xargs :guard (and (natp n)
                             (integerp truth)
                             (natp numvars))))
 (declare (xargs :guard (< n numvars)))
 (let
     ((__function__ 'is-xor-with-var))
     (declare (ignorable __function__))
     (equal (truth-norm (positive-cofactor n truth numvars)
                        numvars)
            (truth-norm (lognot (negative-cofactor n truth numvars))
                        numvars))))

Theorem: is-xor-with-var-correct

(defthm
 is-xor-with-var-correct
 (implies
      (and (is-xor-with-var n truth numvars)
           (< (nfix n) (nfix numvars)))
      (equal (truth-eval (logxor (negative-cofactor n truth numvars)
                                 (var n numvars))
                         env numvars)
             (truth-eval truth env numvars))))

Theorem: is-xor-with-var-of-truth-norm

(defthm is-xor-with-var-of-truth-norm
        (equal (is-xor-with-var n (truth-norm truth numvars)
                                numvars)
               (is-xor-with-var n truth numvars)))

Theorem: is-xor-with-var-of-nfix-n

(defthm is-xor-with-var-of-nfix-n
        (equal (is-xor-with-var (nfix n) truth numvars)
               (is-xor-with-var n truth numvars)))

Theorem: is-xor-with-var-nat-equiv-congruence-on-n

(defthm is-xor-with-var-nat-equiv-congruence-on-n
        (implies (nat-equiv n n-equiv)
                 (equal (is-xor-with-var n truth numvars)
                        (is-xor-with-var n-equiv truth numvars)))
        :rule-classes :congruence)

Theorem: is-xor-with-var-of-ifix-truth

(defthm is-xor-with-var-of-ifix-truth
        (equal (is-xor-with-var n (ifix truth) numvars)
               (is-xor-with-var n truth numvars)))

Theorem: is-xor-with-var-int-equiv-congruence-on-truth

(defthm is-xor-with-var-int-equiv-congruence-on-truth
        (implies (int-equiv truth truth-equiv)
                 (equal (is-xor-with-var n truth numvars)
                        (is-xor-with-var n truth-equiv numvars)))
        :rule-classes :congruence)

Theorem: is-xor-with-var-of-nfix-numvars

(defthm is-xor-with-var-of-nfix-numvars
        (equal (is-xor-with-var n truth (nfix numvars))
               (is-xor-with-var n truth numvars)))

Theorem: is-xor-with-var-nat-equiv-congruence-on-numvars

(defthm is-xor-with-var-nat-equiv-congruence-on-numvars
        (implies (nat-equiv numvars numvars-equiv)
                 (equal (is-xor-with-var n truth numvars)
                        (is-xor-with-var n truth numvars-equiv)))
        :rule-classes :congruence)