Lift atj-type-join to lists.
(atj-type-list-join x y) → lub
This is done element-wise. When the shorter list is exhausted, we return (what remains of) the longer list.
We show that this agrees with atj-type-top-list-join
over lists of ATJ types.
Note that atj-type-top-list-join 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-join (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-join)) (declare (ignorable __function__)) (cond ((endp x) (atj-type-list-fix y)) ((endp y) (atj-type-list-fix x)) (t (cons (atj-type-join (car x) (car y)) (atj-type-list-join (cdr x) (cdr y)))))))
Theorem:
(defthm atj-maybe-type-listp-of-atj-type-list-join (b* ((lub (atj-type-list-join x y))) (atj-maybe-type-listp lub)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-list-join-alt-def (implies (and (atj-type-listp x) (atj-type-listp y)) (equal (atj-type-list-join x y) (atj-type-top-list-join x y))))
Theorem:
(defthm consp-of-atj-type-list-join (b* ((?lub (atj-type-list-join x y))) (equal (consp lub) (or (consp x) (consp y)))))