Lift atj-type-meet to lists.
(atj-type-list-meet x y) → glb
This is done element-wise.
When the shorter list is exhausted,
we return
We show that this agrees with atj-type-bottom-list-meet
over lists of ATJ types.
Note that atj-type-bottom-list-meet has been defined
just to show the semilattice properties,
but we always want to use, as arguments,
lists of ATJ types without
Function:
(defun atj-type-list-meet (x y) (declare (xargs :guard (and (atj-type-listp x) (atj-type-listp y)))) (declare (xargs :guard (= (len x) (len y)))) (let ((__function__ 'atj-type-list-meet)) (declare (ignorable __function__)) (cond ((endp x) nil) ((endp y) nil) (t (cons (atj-type-meet (car x) (car y)) (atj-type-list-meet (cdr x) (cdr y)))))))
Theorem:
(defthm atj-maybe-type-listp-of-atj-type-list-meet (b* ((glb (atj-type-list-meet x y))) (atj-maybe-type-listp glb)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-list-meet-alt-def (implies (and (atj-type-listp x) (atj-type-listp y)) (equal (atj-type-list-meet x y) (atj-type-bottom-list-meet x y))))