		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Bfr-=-ss

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

Definitions and Theorems

Function: bfr-=-ss

(defun bfr-=-ss (a b)
  (declare (xargs :guard (and (true-listp a) (true-listp b))))
  (let ((__function__ 'bfr-=-ss))
    (declare (ignorable __function__))
    (b* (((mv head1 tail1 end1)
          (first/rest/end a))
         ((mv head2 tail2 end2)
          (first/rest/end b))
         ((when (and end1 end2))
          (bfr-iff head1 head2))
         (first-eq (bfr-iff head1 head2)))
      (bfr-and first-eq (bfr-=-ss tail1 tail2)))))

Theorem: bfr-=-ss-correct

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

Theorem: bfr-=-ss-deps

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