anchor.diff:        :name updated-fn-lvls-decrease))
       )
   
  -  (define flatten-formals ((formal-lst decl-listp))
  -    :returns (formals symbol-listp)
  -    :measure (len formal-lst)
  -    :hints (("Goal" :in-theory (enable decl-list-fix)))
  -    :enabled t
  -    (b* ((formal-lst (mbe :logic (decl-list-fix formal-lst) :exec formal-lst))
  -         ((if (endp formal-lst)) nil)
  -         ((cons first rest) formal-lst)
  -         ((decl d) first))
  -      (cons d.name (flatten-formals rest))))
  -
     (defprod ex-args
       ((term-lst pseudo-term-listp :default nil)
        (fn-lst func-alistp :default nil)
  
positive.code:                             :hints hyp.hints)
              (generate-hyp-hint-lst rest fn-lst fn-lvls))))
  
    ;; (define generate-fn-hint-pair ((hypo hint-pair-p)
    ;;                                (fn-name symbolp) (returns symbol-listp) (formals symbol-listp)
    ;;                                (actuals pseudo-term-listp))
    ;;   :returns (fn-hint-pair hint-pair-p)
    ;;   (b* (((hint-pair p) hypo)
    ;;        (free-vars (all-vars p.thm))
    ;;        ;; If the returns theorems contain free variables,
    ;;        ;; report an error.
    ;;        ((unless (subsetp free-vars (append returns formals)))
    ;;         (er hard? 'SMT-goal-generator=>generate-fn-hint-pair "Function returns theorem contain free variables: ~q0. The formals are: ~q1 and the returns are: ~q2." p.thm formals returns)))
    ;;     `((lambda ,formals ((lambda ,returns ,p.thm) (,fn-name ,@formals))) ,@actuals)))
  
    ;; (define generate-fn-returns-hint ((returns decl-listp) (fn-name symbolp)
    ;;                                   (formals decl-listp) (actuals pseudo-term-listp)
    ;;                                   (fn-hint-acc hint-pair-listp))
    ;;   :returns (fn-hint-lst hint-pair-listp :hyp :guard)
    ;;   :ignore-ok t
    ;;   nil)
  
    ;; (define generate-fn-more-returns-hint ((more-returns hint-pair-listp) (fn-name symbolp)
    ;;                                        (formals decl-listp) (actuals pseudo-term-listp)
    ;;                                        (fn-hint-acc hint-pair-listp))
    ;;   :returns (fn-hint-lst hint-pair-listp :hyp :guard)
    ;;   :ignore-ok t
    ;;   nil)
  
    ;; (define generate-fn-hint ((fn func-p) (fn-actuals pseudo-term-listp)
    ;;                           (fn-hint-acc hint-pair-listp))
    ;;   :returns (fn-hint-lst hint-pair-listp :hyp :guard)
    ;;   (b* (((func f) fn)
    ;;        ((unless f.uninterpreted)
    ;;         (er hard? 'SMT-goal-generator=>generate-fn-hint "Function call ~q0 still exists in term but it's not declared as an uninterpreted function." f.name))
    ;;        (new-fn-hint-acc
    ;;         (generate-fn-returns-hint f.returns f.name f.formals fn-actuals fn-hint-acc)))
    ;;     (generate-fn-more-returns-hint f.more-returns f.name f.formals fn-actuals new-fn-hint-acc)))
  
  
    ;; ;; function hypotheses generation arguments
    ;; (defprod fhg-args
    ;;   ((term-lst pseudo-term-listp :default nil)
    ;;    (fn-lst func-alistp :default nil)
    ;;    (fn-hint-acc hint-pair-listp :default nil)))
  
    ;; ;; Generate auxiliary hypotheses from function expansion
    ;; (define generate-fn-hint-lst ((args fhg-args-p))
    ;;   :returns (fn-hint-lst hint-pair-listp)
    ;;   (b* (;; If guard is violated, return nil
    ;;        ((unless (fhg-args-p args)) nil)
    ;;        ;; Bind the fields out of the defprod type
    ;;        ((fhg-args a) args)
    ;;        ;; If a.term-lst is nil,
    ;;        ;; return the function hint accumulator a.fn-hint-acc
    ;;        ((unless (consp a.term-lst)) a.fn-hint-acc)
    ;;        ;; If not,
    ;;        ;; cons the first element out of a.term-lst
    ;;        ((cons first rest) a.term-lst)
  
    ;;        ;; If first is symbolp, don't need to generate any hypo
    ;;        ((if (symbolp first))
    ;;         (generate-fn-hint-lst (change-fhg-args :term-lst rest)))
    ;;        ;; Else it must be a consp, if it is a quoted thingy
    ;;        ;; The quoted thingy (cadr term) can be a non-pseudo-termp.
    ;;        ((if (and (equal (car term) 'quote)
    ;;                  (consp (cdr term))
    ;;                  (equal (cddr term) nil)))
    ;;         (generate-fn-hint-lst (change-fhg-args :term-lst rest)))
  
    ;;        ;; Now first must be a true-listp
    ;;        ((cons fn-call fn-actuals) first)
  
    ;;        ;; If term is an atom, return fn-hint-acc
    ;;        ((if (atom G-prim)) fn-hint-acc)
    ;;        ;; If term is nil, return fn-hint-acc
    ;;        ((if (endp G-prim)) fn-hint-acc)
    ;;        ;; Cons the function call and function actuals out of term
    ;;        ((cons fn-call fn-actuals) term)
    ;;        ;; See if fn-call is a lambda expression
    ;;        (pseudo-lambda? (pseudo-lambdap fn-call))
    ;;        ;; Try finding function call from fn-lst
    ;;        (fn (hons-get fn-call fn-lst))
    ;;        ;; If fn-call does not belong to fn-lst and it is not a lambda,
    ;;        ;; then no need to add any hypotheses.
    ;;        ((unless (or fn pseudo-lambda?))
    ;;         (generate-fn-hint-lst-on-lst fn-actuals fn-lst fn-hint-acc))
    ;;        ;; If fn-call belongs to fn-lst
    ;;        ((if fn)
    ;;         (generate-fn-hint-lst-on-lst fn-actuals fn-lst
    ;;                                      (generate-fn-hint (cdr fn) fn-actuals fn-hint-acc)))
    ;;        ;; Else fn-call is a lambda expression
    ;;        (body-fn-hint-lst (generate-fn-hint-lst (lambda-body fn-call) fn-lst fn-hint-acc))
    ;;        )
    ;;     (generate-fn-hint-lst-on-lst fn-actuals fn-lst body-fn-hint-lst)))
  
    ;; Make fn-lst a fast alist
    (define make-alist-fn-lst ((fn-lst func-listp))
      :returns (fast-fn-lst func-alistp)
      :measure (len fn-lst)
      :enabled t
      (b* ((fn-lst (mbe :logic (func-list-fix fn-lst) :exec fn-lst))
           ((unless (consp fn-lst)) nil)
           ((cons first rest) fn-lst)
           ((func f) first))
        (cons (cons f.name f) (make-alist-fn-lst rest))))
  
    ;; The top level function for generating SMT goals: G-prim and A's
    (define SMT-goal-generator ((cl pseudo-term-listp) (hints smtlink-hint-p))
      :returns (new-hints smtlink-hint-p)
      :short "@(call SMT-goal-generator) is the top level function for generating SMT goals: G-prim and A's"
  
      (b* ((cl (mbe :logic (pseudo-term-list-fix cl) :exec cl))
           (hints (mbe :logic (smtlink-hint-fix hints) :exec hints))
           ((smtlink-hint h) hints)
           ;; Make a fast alist version of fn-lst
           (fn-lst (make-alist-fn-lst h.functions))
           (fn-lvls (initialize-fn-lvls fn-lst))
  
           ;; Generate user given hypotheses and their hints from hyp-lst
           (hyp-hint-lst (with-fast-alist fn-lst (generate-hyp-hint-lst h.hypotheses fn-lst fn-lvls)))
  
           ;; Expand main clause using fn-lst
           ;; Generate function hypotheses and their hints from fn-lst
           (G-prim
            (with-fast-alist fn-lst (car (expand (make-ex-args
                                                  :term-lst (list (disjoin cl))
                                                  :fn-lst fn-lst
                                                  :fn-lvls fn-lvls)))))
  
           ;; Generate auxiliary hypotheses from function expansion
           (fn-hint-lst ;; (generate-fn-hint-lst G-prim fn-lst nil)
            nil)
  
           ;; Combine all auxiliary hypotheses
           (total-aux-hint-lst `(,@fn-hint-lst ,@hyp-hint-lst))
  
           ;; Combine expanded main clause and its hint
           (expanded-clause-w/-hint (make-hint-pair :thm G-prim :hints h.main-hint))
  
           ;; Update smtlink-hint
           (new-hints
            (change-smtlink-hint hints
                                 :fast-functions fn-lst
                                 :aux-hint-list total-aux-hint-lst
                                 :expanded-clause-w/-hint expanded-clause-w/-hint
                                 )))
        new-hints))
    )
  
negative.code:                     (consp (ex-args->term-lst expand-args))
                      (not (consp (car (ex-args->term-lst expand-args)))))
                 (symbolp (car (ex-args->term-lst expand-args)))))
  
      (defthm pseudo-termp-of-car-of-ex-args->term-lst
        (implies (and (ex-args-p expand-args)
                      (consp (ex-args->term-lst expand-args)))
                 (pseudo-termp (car (ex-args->term-lst expand-args))))
        :hints (("Goal" :in-theory (enable pseudo-termp))))
  
      (defthm len-equal-of-formals-of-pseudo-lambdap-and-actuals-of-pseudo-termp
        (implies (and (ex-args-p expand-args)
                      (pseudo-termp (car (ex-args->term-lst expand-args)))
                      (pseudo-lambdap (car (car (ex-args->term-lst expand-args)))))
                 (equal (len (cadr (car (car (ex-args->term-lst expand-args)))))
                        (len (cdr (car (ex-args->term-lst expand-args))))))
        :hints (("Goal" :in-theory (enable pseudo-termp pseudo-lambdap))))
  
      (local (defthm lemma-6
               (implies (and (pseudo-termp x) (not (symbolp x)) (not (pseudo-lambdap (car x))))
                        (symbolp (car x)))
               :hints (("Goal" :in-theory (enable pseudo-termp pseudo-lambdap)))))
  
      (defthm symbolp-of-caar-of-ex-args->term-lst
        (implies (and (ex-args-p expand-args)
                      (consp (ex-args->term-lst expand-args))
                      (not (symbolp (car (ex-args->term-lst expand-args))))
                      (not (pseudo-lambdap (car (car (ex-args->term-lst expand-args))))))
                 (symbolp (car (car (ex-args->term-lst expand-args))))))
      )
  
    (encapsulate ()
  