		Search-engine friendly clone of the ACL2 documentation.

Atj-types

Atj-type-join

Least upper bound of two ATJ types.

Signature
(atj-type-join x y) → lub
Arguments: x — Guard (atj-typep x).; y — Guard (atj-typep y).
Returns: lub — Type (atj-maybe-typep 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 nil. So we introduce this function, which operates on types but may return nil, which can be also interpreted as saying that the two ATJ types have no (least) upper bound w.r.t atj-type-<=.

Definitions and Theorems

Function: atj-type-join

(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: atj-maybe-typep-of-atj-type-join

(defthm atj-maybe-typep-of-atj-type-join
  (b* ((lub (atj-type-join x y)))
    (atj-maybe-typep lub))
  :rule-classes :rewrite)