		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-<-ss

Signature
(aabf-<-ss a b man) → (mv a<b new-man)
Arguments: a — Guard (true-listp a).; b — Guard (true-listp b).

Definitions and Theorems

Function: aabf-<-ss

(defun aabf-<-ss (a b man)
  (declare (xargs :guard (and (true-listp a) (true-listp b))))
  (declare (xargs :guard (and (aabflist-p a man)
                              (aabflist-p b man))))
  (let ((__function__ 'aabf-<-ss))
    (declare (ignorable __function__))
    (b* (((when (aabf-syntactically-zero-p b))
          (mv (aabf-sign-s a) man))
         ((mv head1 tail1 end1)
          (aabf-first/rest/end a))
         ((mv head2 tail2 end2)
          (aabf-first/rest/end b))
         ((when (and* end1 end2))
          (aabf-nest (aabf-and head1 (aabf-not head2))
                     man))
         ((mv rst< rst= man)
          (aabf-<-=-ss tail1 tail2 man)))
      (aabf-nest (or rst< (and rst= head2 (aabf-not head1)))
                 man))))

Theorem: trivial-theorem-about-aabf-<-ss

(defthm trivial-theorem-about-aabf-<-ss
  (b* nil
    (b* ((?ignore (aabf-<-ss a b man))) t))
  :rule-classes nil)

Theorem: aabf-extension-p-of-aabf-<-ss

(defthm aabf-extension-p-of-aabf-<-ss
  (b* (((mv ?a<b ?new-man)
        (aabf-<-ss a b man)))
    (aabf-extension-p new-man man)))

Theorem: aabf-p-of-aabf-<-ss

(defthm aabf-p-of-aabf-<-ss
  (b* (((mv a<b new-man) (aabf-<-ss a b man)))
    (implies (and (aabflist-p a man)
                  (aabflist-p b man))
             (and (aabf-p a<b new-man)))))

Theorem: aabf-eval-of-aabf-<-ss

(defthm aabf-eval-of-aabf-<-ss
  (b* (((mv a<b new-man) (aabf-<-ss a b man)))
    (implies
         (and (aabflist-p a man)
              (aabflist-p b man))
         (and (equal (aabf-eval a<b env new-man)
                     (< (bools->int (aabflist-eval a env man))
                        (bools->int (aabflist-eval b env man))))))))

Theorem: aabf-pred-of-aabf-<-ss

(defthm aabf-pred-of-aabf-<-ss
  (b* (((mv a<b new-man) (aabf-<-ss a b man)))
    (implies (and (aabflist-p a man)
                  (aabflist-p b man)
                  (aabflist-pred a man)
                  (aabflist-pred b man))
             (and (aabf-pred a<b new-man)))))