Lift atj-type-bottom-meet to lists.
(atj-type-bottom-list-meet x y) → glb
This is done element-wise.
When the shorter list is exhausted,
we return
We show that this indeed returns the greatest lower bound of the order relation lifted to lists.
Function:
(defun atj-type-bottom-list-meet (x y) (declare (xargs :guard (and (atj-maybe-type-listp x) (atj-maybe-type-listp y)))) (let ((__function__ 'atj-type-bottom-list-meet)) (declare (ignorable __function__)) (cond ((endp x) nil) ((endp y) nil) (t (cons (atj-type-bottom-meet (car x) (car y)) (atj-type-bottom-list-meet (cdr x) (cdr y)))))))
Theorem:
(defthm atj-maybe-type-listp-of-atj-type-bottom-list-meet (b* ((glb (atj-type-bottom-list-meet x y))) (atj-maybe-type-listp glb)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-bottom-list-meet-lower-bound-left (atj-type-bottom-list-<= (atj-type-bottom-list-meet x y) x))
Theorem:
(defthm atj-type-bottom-list-meet-lower-bound-right (atj-type-bottom-list-<= (atj-type-bottom-list-meet x y) y))
Theorem:
(defthm atj-type-bottom-list-meet-greatest (implies (and (atj-type-bottom-list-<= z x) (atj-type-bottom-list-<= z y)) (atj-type-bottom-list-<= z (atj-type-bottom-list-meet x y))))
Theorem:
(defthm atj-type-bottom-list-meet-of-atj-maybe-type-list-fix-x (equal (atj-type-bottom-list-meet (atj-maybe-type-list-fix x) y) (atj-type-bottom-list-meet x y)))
Theorem:
(defthm atj-type-bottom-list-meet-atj-maybe-type-list-equiv-congruence-on-x (implies (atj-maybe-type-list-equiv x x-equiv) (equal (atj-type-bottom-list-meet x y) (atj-type-bottom-list-meet x-equiv y))) :rule-classes :congruence)
Theorem:
(defthm atj-type-bottom-list-meet-of-atj-maybe-type-list-fix-y (equal (atj-type-bottom-list-meet x (atj-maybe-type-list-fix y)) (atj-type-bottom-list-meet x y)))
Theorem:
(defthm atj-type-bottom-list-meet-atj-maybe-type-list-equiv-congruence-on-y (implies (atj-maybe-type-list-equiv y y-equiv) (equal (atj-type-bottom-list-meet x y) (atj-type-bottom-list-meet x y-equiv))) :rule-classes :congruence)