Lift atj-type-top-<= to lists.
(atj-type-top-list-<= sub sup) → yes/no
Lists are ordered element-wise. Given two lists of different lengths such that the shorter one is a prefix of the longer one (i.e. the two lists cannot be ordered based on their initial elements), the shorter one is smaller than the longer one.
We show that the resulting relation is a partial order, i.e. reflexive, anti-symmetric, and transitive.
Function:
(defun atj-type-top-list-<= (sub sup) (declare (xargs :guard (and (atj-maybe-type-listp sub) (atj-maybe-type-listp sup)))) (let ((__function__ 'atj-type-top-list-<=)) (declare (ignorable __function__)) (cond ((endp sub) t) ((endp sup) nil) (t (and (atj-type-top-<= (car sub) (car sup)) (atj-type-top-list-<= (cdr sub) (cdr sup)))))))
Theorem:
(defthm booleanp-of-atj-type-top-list-<= (b* ((yes/no (atj-type-top-list-<= sub sup))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-top-list-<=-reflexive (implies (atj-maybe-type-list-equiv x y) (atj-type-top-list-<= x y)))
Theorem:
(defthm atj-type-top-list-<=-antisymmetric (implies (and (atj-type-top-list-<= x y) (atj-type-top-list-<= y x)) (atj-maybe-type-list-equiv x y)))
Theorem:
(defthm atj-type-top-list-<=-transitive (implies (and (atj-type-top-list-<= x y) (atj-type-top-list-<= y z)) (atj-type-top-list-<= x z)))
Theorem:
(defthm atj-type-top-list-<=-of-atj-maybe-type-list-fix-sub (equal (atj-type-top-list-<= (atj-maybe-type-list-fix sub) sup) (atj-type-top-list-<= sub sup)))
Theorem:
(defthm atj-type-top-list-<=-atj-maybe-type-list-equiv-congruence-on-sub (implies (atj-maybe-type-list-equiv sub sub-equiv) (equal (atj-type-top-list-<= sub sup) (atj-type-top-list-<= sub-equiv sup))) :rule-classes :congruence)
Theorem:
(defthm atj-type-top-list-<=-of-atj-maybe-type-list-fix-sup (equal (atj-type-top-list-<= sub (atj-maybe-type-list-fix sup)) (atj-type-top-list-<= sub sup)))
Theorem:
(defthm atj-type-top-list-<=-atj-maybe-type-list-equiv-congruence-on-sup (implies (atj-maybe-type-list-equiv sup sup-equiv) (equal (atj-type-top-list-<= sub sup) (atj-type-top-list-<= sub sup-equiv))) :rule-classes :congruence)