Least upper bound of two ATJ types.
(atj-type-join x y) → lub
We have defined atj-type-top-join
in order to exhibit and prove the semilattice structure,
but we always want to use ATJ types as arguments, never
Function:
(defun atj-type-join (x y) (declare (xargs :guard (and (atj-typep x) (atj-typep y)))) (let ((__function__ 'atj-type-join)) (declare (ignorable __function__)) (atj-type-top-join x y)))
Theorem:
(defthm atj-maybe-typep-of-atj-type-join (b* ((lub (atj-type-join x y))) (atj-maybe-typep lub)) :rule-classes :rewrite)