(atj-type-to-pred-gen-mono-thms-1 sub sups) → *
Function:
(defun atj-type-to-pred-gen-mono-thms-1 (sub sups) (declare (xargs :guard (and (atj-typep sub) (atj-type-listp sups)))) (let ((__function__ 'atj-type-to-pred-gen-mono-thms-1)) (declare (ignorable __function__)) (cond ((endp sups) nil) (t (append (atj-type-to-pred-gen-mono-thm sub (car sups)) (atj-type-to-pred-gen-mono-thms-1 sub (cdr sups)))))))
Theorem:
(defthm atj-type-to-pred-gen-mono-thms-1-of-atj-type-fix-sub (equal (atj-type-to-pred-gen-mono-thms-1 (atj-type-fix sub) sups) (atj-type-to-pred-gen-mono-thms-1 sub sups)))
Theorem:
(defthm atj-type-to-pred-gen-mono-thms-1-atj-type-equiv-congruence-on-sub (implies (atj-type-equiv sub sub-equiv) (equal (atj-type-to-pred-gen-mono-thms-1 sub sups) (atj-type-to-pred-gen-mono-thms-1 sub-equiv sups))) :rule-classes :congruence)
Theorem:
(defthm atj-type-to-pred-gen-mono-thms-1-of-atj-type-list-fix-sups (equal (atj-type-to-pred-gen-mono-thms-1 sub (atj-type-list-fix sups)) (atj-type-to-pred-gen-mono-thms-1 sub sups)))
Theorem:
(defthm atj-type-to-pred-gen-mono-thms-1-atj-type-list-equiv-congruence-on-sups (implies (atj-type-list-equiv sups sups-equiv) (equal (atj-type-to-pred-gen-mono-thms-1 sub sups) (atj-type-to-pred-gen-mono-thms-1 sub sups-equiv))) :rule-classes :congruence)