Lift param-declon-to-ident+tyname to lists.
(param-declon-list-to-ident+tyname-lists declons) → (mv ids tynames)
Function:
(defun param-declon-list-to-ident+tyname-lists (declons) (declare (xargs :guard (param-declon-listp declons))) (let ((__function__ 'param-declon-list-to-ident+tyname-lists)) (declare (ignorable __function__)) (b* (((when (endp declons)) (mv nil nil)) ((mv id tyname) (param-declon-to-ident+tyname (car declons))) ((mv ids tynames) (param-declon-list-to-ident+tyname-lists (cdr declons)))) (mv (cons id ids) (cons tyname tynames)))))
Theorem:
(defthm ident-listp-of-param-declon-list-to-ident+tyname-lists.ids (b* (((mv ?ids ?tynames) (param-declon-list-to-ident+tyname-lists declons))) (ident-listp ids)) :rule-classes :rewrite)
Theorem:
(defthm tyname-listp-of-param-declon-list-to-ident+tyname-lists.tynames (b* (((mv ?ids ?tynames) (param-declon-list-to-ident+tyname-lists declons))) (tyname-listp tynames)) :rule-classes :rewrite)
Theorem:
(defthm len-of-param-declon-list-to-ident+tyname-lists.ids (b* (((mv ?ids ?tynames) (param-declon-list-to-ident+tyname-lists declons))) (equal (len ids) (len declons))))
Theorem:
(defthm len-of-param-declon-list-to-ident+tyname-lists.tynames (b* (((mv ?ids ?tynames) (param-declon-list-to-ident+tyname-lists declons))) (equal (len tynames) (len declons))))
Theorem:
(defthm param-declon-list-to-ident+tyname-lists-of-param-declon-list-fix-declons (equal (param-declon-list-to-ident+tyname-lists (param-declon-list-fix declons)) (param-declon-list-to-ident+tyname-lists declons)))
Theorem:
(defthm param-declon-list-to-ident+tyname-lists-param-declon-list-equiv-congruence-on-declons (implies (param-declon-list-equiv declons declons-equiv) (equal (param-declon-list-to-ident+tyname-lists declons) (param-declon-list-to-ident+tyname-lists declons-equiv))) :rule-classes :congruence)