anchor.diff:      (mbe :logic (if (function-option-name-p option-name) option-name ':formals)
            :exec option-name))
   
  -(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))
  -
  -  ;; (define function-option-name-lst-p ((option-lst t))
  -  ;;   :returns (syntax-good? booleanp)
  -  ;;   :short "Recoginizer for option-lst."
  -  ;;   (b* (((if (atom option-lst)) (equal option-lst nil))
  -  ;;        ((cons first rest) option-lst))
  -  ;;     (and (function-option-name-p first)
  -  ;;          (function-option-name-lst-p rest))))
  -
  -  ;; (define function-option-name-lst-fix ((option-lst function-option-name-lst-p))
  -  ;;   :returns (fixed-option-lst function-option-name-lst-p
  -  ;;                              :hints (("Goal" :in-theory (enable function-option-name-lst-p))))
  -  ;;   :short "Fixing function for option-name-lst."
  -  ;;   :verify-guards nil
  -  ;;   (mbe :logic (if (atom option-lst)
  -  ;;                   nil
  -  ;;                 (cons (function-option-name-fix (car option-lst))
  -  ;;                       (function-option-name-lst-fix (cdr option-lst))))
  -  ;;        :exec option-lst))
  -  ;; (verify-guards function-option-name-lst-fix
  -  ;;   :hints (("Goal" :in-theory (enable function-option-name-fix
  -  ;;                                      function-option-name-lst-fix
  -  ;;                                      function-option-name-p function-option-name-lst-p))))
  -
  -  ;; 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))
  -    :returns (mv (syntax-good? booleanp)
  -                 (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."
  -    :verify-guards nil
  -    (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))))
  -  (verify-guards function-option-syntax-p
  -    :guard-debug t
  -    :hints (("Goal" :in-theory (enable function-option-syntax-p function-option-name-p
  -                                       eval-function-option-type function-option-name-lst-p))))
  -
  -  ;; (define exist-odd-lst ((key symbolp) (lst t))
  -  ;;   :returns (exist? booleanp)
  -  ;;   :short "Test if key exist in lst on the odd positions (with position staring
  -  ;; from 1)"
  -  ;;   :measure (len lst)
  -  ;;   :hints (("Goal" :in-theory (enable true-list-fix)))
  -  ;;   :verify-guards nil
  -  ;;   (b* ((key (symbol-fix key))
  -  ;;        ((if (equal lst nil)) nil)
  -  ;;        ((unless (and (true-listp lst) (>= (len lst) 2))) nil)
  -  ;;        ((list* first & rest) lst)
  -  ;;        ((if (equal first key)) t))
  -  ;;     (exist-odd-lst key rest)))
  -  ;; (verify-guards exist-odd-lst
  -  ;;   :hints (("Goal" :in-theory (enable true-list-fix))))
  -
  -(define function-option-lst-syntax-p-helper ((term t) (used function-option-name-lst-p))
  -    :returns (syntax-good? booleanp)
  -    :short "Helper for function-option-lst-syntax-p."
  -    (b* (((if (atom term)) (equal term nil))
  -         ((unless (and (true-listp term) (>= (len term) 2))) nil)
  -         ((list* first second rest) term)
  -         (- (cw "first: ~q0" first))
  -         (- (cw "second: ~q0" second))
  -         ((mv res new-used) (function-option-syntax-p (list first second)
  -                                                      used))
  -         (- (cw "res: ~q0" res))
  -         (- (cw "booleanp? ~q0" (booleanp second))))
  -      (and res (function-option-lst-syntax-p-helper rest new-used)))
  -    ///
  -    (defthm function-option-lst-syntax-p-constraint
  -      (implies (and (function-option-lst-syntax-p-helper fun-opt-lst any)
  -                    (consp fun-opt-lst))
  -               (or (equal (car fun-opt-lst) ':formals)
  -                   (equal (car fun-opt-lst) ':returns)
  -                   (equal (car fun-opt-lst) ':level)
  -                   (equal (car fun-opt-lst) ':guard)
  -                   (equal (car fun-opt-lst) ':more-returns)))
  -      :hints (("Goal"
  -               :in-theory (enable eval-function-option-type
  -                                  function-option-syntax-p
  -                                  function-option-name-p))))
  -
  -    (defthm function-option-lst-syntax-p-of-option
  -      (implies
  -       (and (consp (cdr fun-opt-lst))
  -            (function-option-lst-syntax-p-helper fun-opt-lst nil)
  -            (consp fun-opt-lst))
  -       (and (implies (equal (car fun-opt-lst) ':formals)
  -                     (argument-lst-syntax-p (cadr fun-opt-lst)))
  -            (implies (equal (car fun-opt-lst) ':returns)
  -                     (argument-lst-syntax-p (cadr fun-opt-lst)))
  -            (implies (equal (car fun-opt-lst) ':level)
  -                     (natp (cadr fun-opt-lst)))
  -            (implies (equal (car fun-opt-lst) ':guard)
  -                     (hypothesis-syntax-p (cadr fun-opt-lst)))
  -            (implies (equal (car fun-opt-lst) ':more-returns)
  -                     (hypothesis-lst-syntax-p (cadr fun-opt-lst)))))
  -      :hints (("Goal"
  -               :in-theory (enable function-option-syntax-p
  -                                  eval-function-option-type))))
  -
  -    (defthm car-term-function-option-syntax-p
  -      (implies (and (consp term)
  -                    (function-option-lst-syntax-p-helper term used))
  -               (function-option-name-p (car term)))
  -      :hints (("Goal" :in-theory (enable function-option-syntax-p))))
  -
  -    (defthm caddr-term-function-option-syntax-p
  -      (implies (and (consp (cddr term))
  -                    (not (function-option-name-p (caddr term)))
  -                    (function-option-lst-syntax-p-helper (cddr term) used))
  -               (not (caddr term)))
  -      :hints (("Goal" :in-theory (enable function-option-syntax-p))))
  -    )
  -
   (define true-set-equiv ((list1 true-listp) (list2 true-listp))
     :returns (p booleanp)
     (if (equal (true-listp list1) (true-listp list2))
  
positive.code:                                        hypothesis-lst-syntax-fix
                                         hypothesis-syntax-p
                                         hypothesis-syntax-fix))))
  
    ;; 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)
  
negative.code:   :hints (("Goal"
             :in-theory (e/d (function-option-lst-syntax-fix
                              function-option-lst-syntax-p
                              function-option-syntax-p
                              hypothesis-lst-syntax-p)
                             (function-option-lst-syntax-p-helper--head
                              natp))
             :expand ((function-option-syntax-p (list (car fun-opt-lst) (cadr
                                                                         fun-opt-lst)) nil))
             )))
  
    (define make-merge-function ((func function-syntax-p) (smt-func func-p))
  