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