(aabf-<-=-ss a b man) → (mv a<b a=b new-man)
Function:
(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* (((mv head1 tail1 end1) (aabf-first/rest/end a)) ((mv head2 tail2 end2) (aabf-first/rest/end b)) ((when (and* end1 end2)) (b* (((mv less man) (aabf-nest (and head1 (not head2)) man)) ((mv equal man) (if (aabf-syntactically-true-p less man) (mv (aabf-false) man) (aabf-iff head1 head2 man)))) (mv less equal man))) ((mv rst< rst= man) (aabf-<-=-ss tail1 tail2 man)) ((mv less man) (aabf-nest (or rst< (and rst= head2 (aabf-not head1))) man)) ((mv equal man) (if (aabf-syntactically-true-p less man) (mv (aabf-false) man) (aabf-nest (aabf-and rst= (aabf-iff head1 head2)) man)))) (mv less equal man))))
Theorem:
(defthm trivial-theorem-about-aabf-<-=-ss (b* nil (b* ((?ignore (aabf-<-=-ss a b man))) t)) :rule-classes nil)
Theorem:
(defthm aabf-extension-p-of-aabf-<-=-ss (b* (((mv ?a<b ?a=b ?new-man) (aabf-<-=-ss a b man))) (aabf-extension-p new-man man)))
Theorem:
(defthm aabf-p-of-aabf-<-=-ss (b* (((mv a<b 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) (aabf-p a=b new-man)))))
Theorem:
(defthm aabf-eval-of-aabf-<-=-ss (b* (((mv a<b 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)))) (equal (aabf-eval a=b env new-man) (= (bools->int (aabflist-eval a env man)) (bools->int (aabflist-eval b env man))))))))
Theorem:
(defthm aabf-pred-of-aabf-<-=-ss (b* (((mv a<b 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) (aabf-pred a=b new-man)))))