(bfr-<-=-ss a b) → (mv a<b a=b)
Function:
(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)) (b* ((less (bfr-and head1 (bfr-not head2)))) (mv less (if (syntactically-true-p less) nil (bfr-iff head1 head2))))) ((mv rst< rst=) (bfr-<-=-ss tail1 tail2)) (less (bfr-or rst< (bfr-and rst= head2 (bfr-not head1))))) (mv less (if (syntactically-true-p less) nil (bfr-and rst= (bfr-iff head1 head2)))))))
Theorem:
(defthm bfr-<-=-ss-correct (b* (((mv a<b a=b) (bfr-<-=-ss a b))) (and (equal (bfr-eval a<b env) (< (bfr-list->s a env) (bfr-list->s b env))) (equal (bfr-eval a=b env) (= (bfr-list->s a env) (bfr-list->s b env))))))
Theorem:
(defthm bfr-<-=-ss-deps (b* (((mv a<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)) (not (pbfr-depends-on varname param a=b))))))