Helper for function-option-lst-syntax-p.
(function-option-lst-syntax-p-helper term used) → ok
Function:
(defun function-option-lst-syntax-p-helper (term used) (declare (xargs :guard (function-option-name-lst-p used))) (let ((acl2::__function__ 'function-option-lst-syntax-p-helper)) (declare (ignorable acl2::__function__)) (b* (((unless (true-listp term)) nil) ((unless term) t) ((unless (cdr term)) nil) ((list* first second rest) term) ((mv res new-used) (function-option-syntax-p (list first second) used))) (and res (function-option-lst-syntax-p-helper rest new-used)))))
Theorem:
(defthm booleanp-of-function-option-lst-syntax-p-helper (b* ((ok (function-option-lst-syntax-p-helper term used))) (booleanp ok)) :rule-classes :rewrite)
Theorem:
(defthm function-option-lst-syntax-p-helper--monotonicity (implies (and (subsetp used-1 used :test 'equal) (function-option-lst-syntax-p-helper term used)) (function-option-lst-syntax-p-helper term used-1)))
Theorem:
(defthm function-option-lst-syntax-p-helper--congruence (b* ((ok (function-option-lst-syntax-p-helper term used))) (implies (acl2::set-equiv used-1 used) (equal (function-option-lst-syntax-p-helper term used-1) ok))) :rule-classes (:congruence))
Theorem:
(defthm function-option-lst-syntax-p-helper--head (implies (and (function-option-lst-syntax-p-helper term used) term) (and (<= 2 (len term)) (function-option-syntax-p (list (car term) (cadr term)) used))))
Theorem:
(defthm function-option-lst-syntax-p-helper-preserve (implies (and (function-option-lst-syntax-p-helper term nil) (consp term)) (function-option-lst-syntax-p-helper (cddr term) nil)))