(atj-mark-lambda-formals formals actuals vars-in-scope vars-used-after vars-to-mark-new) → (mv marked-formals new-vars-to-mark-new)
Function:
(defun atj-mark-lambda-formals (formals actuals vars-in-scope vars-used-after vars-to-mark-new) (declare (xargs :guard (and (symbol-listp formals) (pseudo-term-listp actuals) (symbol-listp vars-in-scope) (symbol-listp vars-used-after) (symbol-listp vars-to-mark-new)))) (declare (xargs :guard (= (len formals) (len actuals)))) (let ((__function__ 'atj-mark-lambda-formals)) (declare (ignorable __function__)) (b* (((when (endp formals)) (mv nil vars-to-mark-new)) (formal (car formals)) (new? (or (not (member-eq formal vars-in-scope)) (member-eq formal vars-used-after) (dumb-occur-var-open-lst formal (cdr actuals)))) (marked-formal (if new? (atj-mark-var-new formal) (atj-mark-var-old formal))) (vars-to-mark-new (if new? (cons formal vars-to-mark-new) (remove-eq formal vars-to-mark-new))) ((mv marked-formals vars-to-mark-new) (atj-mark-lambda-formals (cdr formals) (cdr actuals) vars-in-scope vars-used-after vars-to-mark-new))) (mv (cons marked-formal marked-formals) vars-to-mark-new))))
Theorem:
(defthm return-type-of-atj-mark-lambda-formals.marked-formals (b* (((mv ?marked-formals ?new-vars-to-mark-new) (atj-mark-lambda-formals formals actuals vars-in-scope vars-used-after vars-to-mark-new))) (and (symbol-listp marked-formals) (equal (len marked-formals) (len formals)))) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atj-mark-lambda-formals.new-vars-to-mark-new (implies (and (symbol-listp formals) (symbol-listp vars-to-mark-new)) (b* (((mv ?marked-formals ?new-vars-to-mark-new) (atj-mark-lambda-formals formals actuals vars-in-scope vars-used-after vars-to-mark-new))) (symbol-listp new-vars-to-mark-new))) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-atj-mark-lambda-formals.marked-formals (b* (((mv ?marked-formals ?new-vars-to-mark-new) (atj-mark-lambda-formals formals actuals vars-in-scope vars-used-after vars-to-mark-new))) (true-listp marked-formals)) :rule-classes :type-prescription)
Theorem:
(defthm true-listp-of-atj-mark-lambda-formals.new-vars-to-mark-new (implies (true-listp vars-to-mark-new) (b* (((mv ?marked-formals ?new-vars-to-mark-new) (atj-mark-lambda-formals formals actuals vars-in-scope vars-used-after vars-to-mark-new))) (true-listp new-vars-to-mark-new))) :rule-classes :type-prescription)
Theorem:
(defthm len-of-atj-mark-lambda-formals.marked-formals (b* (((mv ?marked-formals ?new-vars-to-mark-new) (atj-mark-lambda-formals formals actuals vars-in-scope vars-used-after vars-to-mark-new))) (equal (len marked-formals) (len formals))))