		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Bfr-logeqv-ss

Signature
(bfr-logeqv-ss a b) → a=b
Arguments: a — Guard (true-listp a).; b — Guard (true-listp b).
Returns: a=b — Type (true-listp a=b).

Definitions and Theorems

Function: bfr-logeqv-ss

(defun bfr-logeqv-ss (a b)
  (declare (xargs :guard (and (true-listp a) (true-listp b))))
  (let ((__function__ 'bfr-logeqv-ss))
    (declare (ignorable __function__))
    (b* (((mv af ar aend) (first/rest/end a))
         ((mv bf br bend) (first/rest/end b))
         (c (bfr-iff af bf))
         ((when (and aend bend)) (bfr-sterm c))
         (r (bfr-logeqv-ss ar br)))
      (bfr-scons c r))))

Theorem: true-listp-of-bfr-logeqv-ss

(defthm true-listp-of-bfr-logeqv-ss
  (b* ((a=b (bfr-logeqv-ss a b)))
    (true-listp a=b))
  :rule-classes :type-prescription)

Theorem: bfr-logeqv-ss-correct

(defthm bfr-logeqv-ss-correct
  (b* ((a=b (bfr-logeqv-ss a b)))
    (and (equal (bfr-list->s a=b env)
                (logeqv (bfr-list->s a env)
                        (bfr-list->s b env))))))

Theorem: bfr-logeqv-ss-deps

(defthm bfr-logeqv-ss-deps
  (b* ((a=b (bfr-logeqv-ss a b)))
    (implies (and (not (pbfr-list-depends-on varname param a))
                  (not (pbfr-list-depends-on varname param b)))
             (and (not (pbfr-list-depends-on varname param a=b))))))