anchor.diff:                                         hypothesis-lst-syntax-fix
                                          hypothesis-syntax-p
                                          hypothesis-syntax-fix))))
  -
  -  ;; BOZO:
  +  )
  +
  +
  +(working-here)
  +(defthm function-option-lst-syntax-p-implies-everything-you-want
  +  (implies (and (function-option-lst-syntax-p term) term)
  +           (and (function-option-syntax-p (list (car term) (cadr term)) nil)))
  +  :hints(("Goal"
  +          :expand((function-option-lst-syntax-p term)
  +                  (function-option-lst-syntax-p-helper term nil))
  +          :use ((:instance function-option-lst-syntax-p-helper--monotonicity
  +                           (term (cddr term)))))))
  +
  +  ;; Bozo:
     ;; This implementation is potentially slow because of the threading of smt-func
     ;; all the way while at the same time updating it.
     (define make-merge-function-option-lst ((fun-opt-lst function-option-lst-syntax-p)
  
positive.code:   :hints (("Goal"
             :in-theory (e/d (function-option-lst-syntax-fix
                              function-option-lst-syntax-p
                              function-option-lst-syntax-p-helper
                              hypothesis-lst-syntax-p) (natp))
             :use ((:instance function-option-lst-syntax-p-of-option)
                   (:instance function-option-lst-syntax-p-constraint (any nil)))
             )))
  
    (define make-merge-function ((func function-syntax-p) (smt-func func-p))
  
negative.code: (defequiv true-set-equiv
    :hints (("Goal" :in-theory (enable true-set-equiv))))
  
  
  (defsection function-option-name-lst
    (encapsulate ()
      (local (in-theory (enable function-option-name-fix)))
      (deffixtype function-option-name
        :pred  function-option-name-p
        :fix   function-option-name-fix
        :equiv function-option-name-equiv
        :define t
        :forward t
        :topic function-option-name-p)
  
      (deflist function-option-name-lst
        :elt-type function-option-name
        :true-listp t))
  
    (defthm function-option-name-fix-preserves-member
      (implies (member x used :test 'equal)
               (member (function-option-name-fix x)
                       (function-option-name-lst-fix used) :test 'equal)))
  
    (defthm function-option-name-lst-fix-preserves-subsetp
      (implies (subsetp used-1 used-2 :test 'equal)
               (subsetp (function-option-name-lst-fix used-1)
                        (function-option-name-lst-fix used-2)
                        :test 'equal))
      :hints(("Goal" :in-theory (e/d (subsetp-equal)))))
  
    (defthm function-option-name-lst-fix-preserves-set-equiv
      (implies (acl2::set-equiv used-1 used-2)
               (acl2::set-equiv
                (function-option-name-lst-fix used-1)
                (function-option-name-lst-fix used-2)))
      :hints (("Goal" :in-theory (enable acl2::set-equiv)))
      :rule-classes(:congruence))
  
    (defthm function-option-name-lst-p-and-member
      (implies (and (member x used)
                    (not (function-option-name-p x)))
               (not (function-option-name-lst-p used)))
      :hints(("Goal" :in-theory (enable function-option-name-lst-p))))
  
    (defthm function-option-name-lst-p--monotonicity
      (implies (and (equal (true-listp used-1) (true-listp used-2))
                    (subsetp used-1 used-2 :test 'equal)
                    (function-option-name-lst-p used-2))
               (function-option-name-lst-p used-1))
      :hints(("Goal" :in-theory (enable function-option-name-lst-p))))
  
    (defthm function-option-name-lst-p--congruence
      (implies (true-set-equiv used-1 used-2)
               (equal (function-option-name-lst-p used-1)
                      (function-option-name-lst-p used-2)))
      :hints(("Goal" :cases ((function-option-name-lst-p used-1)
                             (function-option-name-lst-p used-2))))
      :rule-classes(:congruence)))
  
  
    ;; The conditions in eval-type should go along with *function-options*
    (define eval-function-option-type ((option-type function-option-type-p) (term t))
      :returns (type-correct? booleanp)
      :short "Evaluating types for function option body."
      (b* ((option-type (function-option-type-fix option-type)))
        (case option-type
          (argument-lst-syntax-p (argument-lst-syntax-p term))
          (natp (natp term))
          (hypothesis-syntax-p (hypothesis-syntax-p term))
          (t (hypothesis-lst-syntax-p term)))))
  
  (define function-option-syntax-p ((term t) (used function-option-name-lst-p))
    :guard-hints (("Goal"
                   :in-theory (enable function-option-syntax-p function-option-name-p
                                       eval-function-option-type function-option-name-lst-p)))
      :returns (mv (ok booleanp)
                   (new-used function-option-name-lst-p
                             :hints (("Goal" :in-theory (enable function-option-name-lst-p function-option-name-p)))))
      :short "Recoginizer for function-option-syntax."
      (b* ((used (function-option-name-lst-fix used))
           ((if (equal term nil)) (mv t used))
           ((unless (and (true-listp term) (car term) (not (cddr term)))) (mv nil used))
           ((cons option body-lst) term)
           ((unless (function-option-name-p option)) (mv nil used))
           (option-type (cdr (assoc-equal option *function-options*))))
        (mv (and (not (member-equal option used))
                 (eval-function-option-type option-type (car body-lst)))
            (cons option used)))
      ///
      (more-returns
       (ok (implies (and (subsetp used-1 used :test 'equal) ok)
                    (mv-nth 0 (function-option-syntax-p term used-1)))
           :name function-option-syntax-p--monotonicity.ok
           )     
       (ok (implies (acl2::set-equiv used-1 used)
                    (equal (mv-nth 0 (function-option-syntax-p term used-1))
                           ok))
           :name function-option-syntax-p--ok-congruence.ok
           :hints(("Goal"
                   :in-theory (disable function-option-syntax-p
                                       function-option-syntax-p--monotonicity.ok
                                       booleanp-of-function-option-syntax-p.ok)
                   :use((:instance function-option-syntax-p--monotonicity.ok
                                   (used-1 used-1) (used used) (term term))
                        (:instance function-option-syntax-p--monotonicity.ok
                                   (used-1 used) (used used-1) (term term))
                        (:instance booleanp-of-function-option-syntax-p.ok
                                   (used used-1) (term term))
                        (:instance booleanp-of-function-option-syntax-p.ok
                                   (used used) (term term)))))
           :rule-classes (:congruence))
       (new-used (implies (and (subsetp used-1 used :test 'equal) ok)
                          (subsetp
                           (mv-nth 1 (function-option-syntax-p term used-1))
                           new-used
                           :test 'equal))
                 :name function-option-syntax-p--monotonicity.new-used)
       (new-used (implies (and term ok)
                          (equal new-used
                                 (cons (car term) (function-option-name-lst-fix used))))
                 :name function-option-syntax-p--new-used-when-ok)))
  
  
  (define function-option-lst-syntax-p-helper ((term t) (used function-option-name-lst-p))
      :returns (ok booleanp)
      :short "Helper for function-option-lst-syntax-p."
      (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)))
      ///
      ;; These seem like they should be more-returns theorems, but
      ;; when I try that, ACL2 fails miserably.
      (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)))
  
      (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))
  
      ;; (more-returns
      ;;  (ok
      ;;   (implies (and (subsetp used-1 used :test 'equal) ok)
      ;;            (function-option-lst-syntax-p-helper term used-1))
      ;;   :name function-option-lst-syntax-p-helper--monotonicity))
  
      ;; (more-returns
      ;;  (ok
      ;;    (implies (acl2::set-equiv used-1 used)
      ;;             (equal (function-option-lst-syntax-p-helper term used-1) ok))
      ;;    :rule-classes(:congruence)
      ;;    :name function-option-lst-syntax-p-helper--congruence)
  
      (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))))
      )
  
  (encapsulate ()
    (defthm lemma-16
      (implies (and (function-option-name-lst-p used)
                    (function-option-name-p new-opt)
                    (function-option-lst-syntax-p-helper term (cons new-opt used)))
               (function-option-lst-syntax-p-helper term used))
      :hints(("Goal"
              :in-theory (disable
                          function-option-lst-syntax-p-helper--monotonicity)
              :use((:instance function-option-lst-syntax-p-helper--monotonicity
                              (used-1 used) (used (cons new-opt used))
                              (term term))))))
  
    (defthm function-option-lst-syntax-preserve
      (implies (and (function-option-lst-syntax-p-helper term nil)
                    (consp term))
               (function-option-lst-syntax-p-helper (cddr term)
                                                    nil))
      :hints (("Goal"
               :in-theory (disable lemma-16)
               :expand ((function-option-lst-syntax-p-helper term nil)
                        (function-option-syntax-p (list (car term) (cadr term))
                                                  nil))
               :use ((:instance lemma-16
                                (term (cddr term))
                                (new-opt (car term))
                                (used nil)))))))
  
  
  (defsection silly-section
    (define function-option-lst-syntax-p ((term t))
      :returns (syntax-good? booleanp)
      :short "Recogizer for function-option-lst-syntax"
  