anchor.diff:              (b* (((unless (function-symbolp fn-call (w state)))
                     (prog2$
                      (er hard? 'SMT-goal-generator=>expand "Should be a function call: ~q0" fn-call)
  -                   a.term-lst))
  +                   (make-ex-outs :expanded-term-lst a.term-lst :expanded-fn-lst a.expand-lst)))
                    (basic-function (member-equal fn-call *SMT-basics*))
                    (lvl-item (assoc-equal fn-call a.fn-lvls))
                    ((if (or basic-function (<= a.wrld-fn-len 0) (and lvl-item (zp (cdr lvl-item)))))
  -                  (cons (cons fn-call (expand (change-ex-args a :term-lst fn-actuals) state))
  -                        (expand (change-ex-args a :term-lst rest) state)))
  +                  (b* ((actuals-res
  +                        (expand (change-ex-args a :term-lst fn-actuals) state))
  +                       ((ex-outs ac) actuals-res)
  +                       (rest-res
  +                        (expand (change-ex-args a :term-lst rest :expand-lst ac.expanded-fn-lst) state))
  +                       ((ex-outs r) rest-res))
  +                    (make-ex-outs :expanded-term-lst (cons (cons fn-call ac.expanded-term-lst) r.expanded-term-lst)
  +
  +                                  :expanded-fn-lst r.expanded-fn-lst)))
                    (formals (formals fn-call (w state)))
                    ((unless (symbol-listp formals))
                     (prog2$
  -                   (er hard? 'SMT-goal-generator=>expand "Formals should be symbol-listp: ~q0" formals)
  -                   a.term-lst))
  +                   (er hard? 'SMT-goal-generator=>expand "formals get a list that's not a symbol-listp for ~q0, the formals are ~q1" fn-call formals)
  +                   (make-ex-outs :expanded-term-lst a.term-lst :expanded-fn-lst a.expand-lst)))
                    (extract-res (meta-extract-formula fn-call state))
                    ((unless (true-listp extract-res))
                     (prog2$
  -                   (er hard? 'SMT-goal-generator=>expand "Function formula should be true-listp: ~q0" extract-res)
  -                   a.term-lst))
  +                   (er hard? 'SMT-goal-generator=>expand "meta-extract-formula returning a non-true-listp for ~q0The extracted result is ~q1" fn-call extract-res)
  +                   (make-ex-outs :expanded-term-lst a.term-lst :expanded-fn-lst a.expand-lst)))
                    (body (nth 2 extract-res))
                    ((unless (pseudo-termp body))
                     (prog2$
  -                   (er hard? 'SMT-goal-generator=>expand "Should be a pseudo-termp: ~q0" body)
  -                   a.term-lst))
  -                 (- (cw "Expanding ... ~q0" fn-call))
  -                 (expanded-lambda-body
  -                  (car (expand (change-ex-args a
  -                                               :term-lst (list body)
  -                                               :fn-lvls (cons `(,fn-call . 0) a.fn-lvls)
  -                                               :wrld-fn-len (1- a.wrld-fn-len))
  -                               state)))
  +                   (er hard? 'SMT-goal-generator=>expand "meta-extract-formula returning a non-pseudo-term for ~q0The body is ~q1" fn-call body)
  +                   (make-ex-outs :expanded-term-lst a.term-lst :expanded-fn-lst a.expand-lst)))
  +                 (- (cw "SMT-goal-generator=>Expanding ... ~q0" fn-call))
  +                 ;; Adding function symbol into expand-lst
  +                 (updated-expand-lst
  +                  (if (assoc-equal term a.expand-lst)
  +                      a.expand-lst (cons `(,term . ,term) a.expand-lst)))
  +                 (body-res
  +                  (expand (change-ex-args a
  +                                          :term-lst (list body)
  +                                          :fn-lvls (cons `(,fn-call . 0) a.fn-lvls)
  +                                          :wrld-fn-len (1- a.wrld-fn-len)
  +                                          :expand-lst updated-expand-lst)
  +                          state))
  +                 ((ex-outs b) body-res)
  +                 ;; Expand function
  +                 (expanded-lambda-body (car b.expanded-term-lst))
                    (expanded-lambda `(lambda ,formals ,expanded-lambda-body))
  -                 (expanded-term-list (expand (change-ex-args a :term-lst fn-actuals) state))
  +                 (actuals-res
  +                  (expand (change-ex-args a :term-lst fn-actuals :expand-lst b.expanded-fn-lst) state))
  +                 ((ex-outs ac) actuals-res)
  +                 (expanded-term-list ac.expanded-term-lst)
                    ((unless (equal (len formals) (len expanded-term-list)))
                     (prog2$
  -                   (er hard? 'SMT-goal-generator=>expand "You called your function with the wrong number of actuals: ~q0" term) a.term-lst)))
  -              (cons `(,expanded-lambda ,@expanded-term-list)
  -                    (expand (change-ex-args a :term-lst rest) state))))
  +                   (er hard? 'SMT-goal-generator=>expand "You called your function with the wrong number of actuals: ~q0" term)
  +                   (make-ex-outs :expanded-term-lst a.term-lst :expanded-fn-lst ac.expanded-fn-lst)) )
  +                 (rest-res
  +                  (expand (change-ex-args a :term-lst rest :expand-lst ac.expanded-fn-lst) state))
  +                 ((ex-outs r) rest-res))
  +              (make-ex-outs :expanded-term-lst (cons `(,expanded-lambda ,@expanded-term-list) r.expanded-term-lst)
  +                            :expanded-fn-lst r.expanded-fn-lst)))
   
              ;; Now fn is a function in fn-lst
              ;; If fn-call is already expanded to level 0, don't expand.
  
positive.code:     ;; 4. clean up the above encapsulated theorems, maybe in another file
      (define expand ((expand-args ex-args-p) state)
        :parents (SMT-goal-generator)
        :returns (expanded-terms pseudo-term-listp
                                 :hints (("Goal" :use ((:instance not-cddr-of-car-of-pseudo-term-list-fix-of-expand-args->term-lst)
                                                       (:instance consp-cdr-of-car-of-pseudo-term-list-fix-of-expand-args->term-lst)))))
        :measure (expand-measure expand-args)
        :verify-guards nil
        :hints
  
negative.code:      (fn-lst func-alistp "List of function definitions to use for
        function expansion." :default nil)
       (fn-lvls sym-nat-alistp "Levels to expand each functions to." :default nil)
       (wrld-fn-len natp "Number of function definitions in curent world." :default 0)
       (expand-lst pseudo-term-alistp "An alist of expanded function symbols associated with their function call" :default nil)))
  
    (defprod ex-outs
      :parents (expand)
      :short "Outputs for function expand"
      ((expanded-term-lst pseudo-term-listp "List of expanded terms." :default nil)
       (expanded-fn-lst pseudo-term-alistp "List of expanded function calls" :default nil)))
  
    (defthm natp-of-sum-lvls-lemma
      (implies (and (consp (sym-nat-alist-fix fn-lvls)) (natp x))
  