String identifying a non-empty list of ATJ types.
(atj-types-id types) → id
We concatenate the short strings returned by atj-type-id.
Function:
(defun atj-types-id-aux (types) (declare (xargs :guard (atj-type-listp types))) (let ((__function__ 'atj-types-id-aux)) (declare (ignorable __function__)) (cond ((endp types) "") (t (str::cat (atj-type-id (car types)) (atj-types-id-aux (cdr types)))))))
Theorem:
(defthm stringp-of-atj-types-id-aux (b* ((id (atj-types-id-aux types))) (stringp id)) :rule-classes :rewrite)
Theorem:
(defthm atj-types-id-aux-of-atj-type-list-fix-types (equal (atj-types-id-aux (atj-type-list-fix types)) (atj-types-id-aux types)))
Theorem:
(defthm atj-types-id-aux-atj-type-list-equiv-congruence-on-types (implies (atj-type-list-equiv types types-equiv) (equal (atj-types-id-aux types) (atj-types-id-aux types-equiv))) :rule-classes :congruence)
Function:
(defun atj-types-id (types) (declare (xargs :guard (atj-type-listp types))) (declare (xargs :guard (consp types))) (let ((__function__ 'atj-types-id)) (declare (ignorable __function__)) (atj-types-id-aux types)))
Theorem:
(defthm stringp-of-atj-types-id (b* ((id (atj-types-id types))) (stringp id)) :rule-classes :rewrite)
Theorem:
(defthm atj-types-id-of-atj-type-list-fix-types (equal (atj-types-id (atj-type-list-fix types)) (atj-types-id types)))
Theorem:
(defthm atj-types-id-atj-type-list-equiv-congruence-on-types (implies (atj-type-list-equiv types types-equiv) (equal (atj-types-id types) (atj-types-id types-equiv))) :rule-classes :congruence)