		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* (((when (syntactically-zero-p b))
          (bfr-sign-s a))
         ((mv head1 tail1 end1)
          (first/rest/end a))
         ((mv head2 tail2 end2)
          (first/rest/end b))
         ((when (and end1 end2))
          (bfr-and head1 (bfr-not head2)))
         ((mv rst< rst=)
          (bfr-<-=-ss tail1 tail2)))
      (bfr-or rst<
              (bfr-and rst= head2 (bfr-not head1))))))

Theorem: bfr-<-ss-correct

(defthm bfr-<-ss-correct
  (b* ((a<b (bfr-<-ss a b)))
    (and (equal (bfr-eval a<b env)
                (< (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))))))