(sv::aig-<-=-ss a b) → (mv a<b a=b)
Function:
(defun sv::aig-<-=-ss (a b) (declare (xargs :guard (and (true-listp a) (true-listp b)))) (let ((__function__ 'sv::aig-<-=-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 (acl2::aig-and head1 (acl2::aig-not head2)))) (mv less (if (syntactically-true-p less) nil (acl2::aig-iff head1 head2))))) ((mv rst< rst=) (sv::aig-<-=-ss tail1 tail2)) (less (acl2::aig-or rst< (acl2::aig-and rst= head2 (acl2::aig-not head1))))) (mv less (if (syntactically-true-p less) nil (acl2::aig-and rst= (acl2::aig-iff head1 head2)))))))
Theorem:
(defthm sv::aig-<-=-ss-correct (b* (((mv a<b a=b) (sv::aig-<-=-ss a b))) (and (equal (acl2::aig-eval a<b env) (< (sv::aig-list->s a env) (sv::aig-list->s b env))) (equal (acl2::aig-eval a=b env) (= (sv::aig-list->s a env) (sv::aig-list->s b env))))))