		Search-engine friendly clone of the ACL2 documentation.

Verified

Uninterpreted-fn-cp

Verified clause-processor for proving return types of uninterpreted functions.

Definitions and Theorems

Theorem: ev-uninterpreted-constraint-0

(defthm ev-uninterpreted-constraint-0
 (implies
    (and (consp acl2::x)
         (syntaxp (not (equal acl2::a ''nil)))
         (not (equal (car acl2::x) 'quote)))
    (equal (ev-uninterpreted acl2::x acl2::a)
           (ev-uninterpreted
                (cons (car acl2::x)
                      (kwote-lst (ev-lst-uninterpreted (cdr acl2::x)
                                                       acl2::a)))
                nil))))

Theorem: ev-uninterpreted-constraint-1

(defthm ev-uninterpreted-constraint-1
  (implies (symbolp acl2::x)
           (equal (ev-uninterpreted acl2::x acl2::a)
                  (and acl2::x
                       (cdr (assoc-equal acl2::x acl2::a))))))

Theorem: ev-uninterpreted-constraint-2

(defthm ev-uninterpreted-constraint-2
  (implies (and (consp acl2::x)
                (equal (car acl2::x) 'quote))
           (equal (ev-uninterpreted acl2::x acl2::a)
                  (cadr acl2::x))))

Theorem: ev-uninterpreted-constraint-3

(defthm ev-uninterpreted-constraint-3
 (implies
  (and (consp acl2::x)
       (consp (car acl2::x)))
  (equal
     (ev-uninterpreted acl2::x acl2::a)
     (ev-uninterpreted (caddr (car acl2::x))
                       (pairlis$ (cadr (car acl2::x))
                                 (ev-lst-uninterpreted (cdr acl2::x)
                                                       acl2::a))))))

Theorem: ev-uninterpreted-constraint-4

(defthm ev-uninterpreted-constraint-4
  (implies (not (consp acl2::x-lst))
           (equal (ev-lst-uninterpreted acl2::x-lst acl2::a)
                  nil)))

Theorem: ev-uninterpreted-constraint-5

(defthm ev-uninterpreted-constraint-5
  (implies (consp acl2::x-lst)
           (equal (ev-lst-uninterpreted acl2::x-lst acl2::a)
                  (cons (ev-uninterpreted (car acl2::x-lst)
                                          acl2::a)
                        (ev-lst-uninterpreted (cdr acl2::x-lst)
                                              acl2::a)))))

Theorem: ev-uninterpreted-constraint-6

(defthm ev-uninterpreted-constraint-6
  (implies (and (not (consp acl2::x))
                (not (symbolp acl2::x)))
           (equal (ev-uninterpreted acl2::x acl2::a)
                  nil)))

Theorem: ev-uninterpreted-constraint-7

(defthm ev-uninterpreted-constraint-7
  (implies (and (consp acl2::x)
                (not (consp (car acl2::x)))
                (not (symbolp (car acl2::x))))
           (equal (ev-uninterpreted acl2::x acl2::a)
                  nil)))

Theorem: ev-uninterpreted-constraint-8

(defthm ev-uninterpreted-constraint-8
  (implies (and (consp acl2::x)
                (equal (car acl2::x) 'not))
           (equal (ev-uninterpreted acl2::x acl2::a)
                  (not (ev-uninterpreted (cadr acl2::x)
                                         acl2::a)))))

Theorem: ev-uninterpreted-constraint-9

(defthm ev-uninterpreted-constraint-9
  (implies (and (consp acl2::x)
                (equal (car acl2::x) 'if))
           (equal (ev-uninterpreted acl2::x acl2::a)
                  (if (ev-uninterpreted (cadr acl2::x)
                                        acl2::a)
                      (ev-uninterpreted (caddr acl2::x)
                                        acl2::a)
                    (ev-uninterpreted (cadddr acl2::x)
                                      acl2::a)))))

Theorem: ev-uninterpreted-constraint-10

(defthm ev-uninterpreted-constraint-10
  (implies (and (consp acl2::x)
                (equal (car acl2::x) 'hint-please))
           (equal (ev-uninterpreted acl2::x acl2::a)
                  (hint-please (ev-uninterpreted (cadr acl2::x)
                                                 acl2::a)))))

Theorem: ev-uninterpreted-disjoin-cons

(defthm ev-uninterpreted-disjoin-cons
  (iff (ev-uninterpreted (disjoin (cons acl2::x acl2::y))
                         acl2::a)
       (or (ev-uninterpreted acl2::x acl2::a)
           (ev-uninterpreted (disjoin acl2::y)
                             acl2::a))))

Theorem: ev-uninterpreted-disjoin-when-consp

(defthm ev-uninterpreted-disjoin-when-consp
  (implies (consp acl2::x)
           (iff (ev-uninterpreted (disjoin acl2::x)
                                  acl2::a)
                (or (ev-uninterpreted (car acl2::x) acl2::a)
                    (ev-uninterpreted (disjoin (cdr acl2::x))
                                      acl2::a)))))

Theorem: ev-uninterpreted-disjoin-atom

(defthm ev-uninterpreted-disjoin-atom
  (implies (not (consp acl2::x))
           (equal (ev-uninterpreted (disjoin acl2::x)
                                    acl2::a)
                  nil))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: ev-uninterpreted-disjoin-append

(defthm ev-uninterpreted-disjoin-append
  (iff (ev-uninterpreted (disjoin (append acl2::x acl2::y))
                         acl2::a)
       (or (ev-uninterpreted (disjoin acl2::x)
                             acl2::a)
           (ev-uninterpreted (disjoin acl2::y)
                             acl2::a))))

Theorem: ev-uninterpreted-conjoin-cons

(defthm ev-uninterpreted-conjoin-cons
  (iff (ev-uninterpreted (conjoin (cons acl2::x acl2::y))
                         acl2::a)
       (and (ev-uninterpreted acl2::x acl2::a)
            (ev-uninterpreted (conjoin acl2::y)
                              acl2::a))))

Theorem: ev-uninterpreted-conjoin-when-consp

(defthm ev-uninterpreted-conjoin-when-consp
  (implies (consp acl2::x)
           (iff (ev-uninterpreted (conjoin acl2::x)
                                  acl2::a)
                (and (ev-uninterpreted (car acl2::x) acl2::a)
                     (ev-uninterpreted (conjoin (cdr acl2::x))
                                       acl2::a)))))

Theorem: ev-uninterpreted-conjoin-atom

(defthm ev-uninterpreted-conjoin-atom
  (implies (not (consp acl2::x))
           (equal (ev-uninterpreted (conjoin acl2::x)
                                    acl2::a)
                  t))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: ev-uninterpreted-conjoin-append

(defthm ev-uninterpreted-conjoin-append
  (iff (ev-uninterpreted (conjoin (append acl2::x acl2::y))
                         acl2::a)
       (and (ev-uninterpreted (conjoin acl2::x)
                              acl2::a)
            (ev-uninterpreted (conjoin acl2::y)
                              acl2::a))))

Theorem: ev-uninterpreted-conjoin-clauses-cons

(defthm ev-uninterpreted-conjoin-clauses-cons
  (iff (ev-uninterpreted (conjoin-clauses (cons acl2::x acl2::y))
                         acl2::a)
       (and (ev-uninterpreted (disjoin acl2::x)
                              acl2::a)
            (ev-uninterpreted (conjoin-clauses acl2::y)
                              acl2::a))))

Theorem: ev-uninterpreted-conjoin-clauses-when-consp

(defthm ev-uninterpreted-conjoin-clauses-when-consp
  (implies
       (consp acl2::x)
       (iff (ev-uninterpreted (conjoin-clauses acl2::x)
                              acl2::a)
            (and (ev-uninterpreted (disjoin (car acl2::x))
                                   acl2::a)
                 (ev-uninterpreted (conjoin-clauses (cdr acl2::x))
                                   acl2::a)))))

Theorem: ev-uninterpreted-conjoin-clauses-atom

(defthm ev-uninterpreted-conjoin-clauses-atom
  (implies (not (consp acl2::x))
           (equal (ev-uninterpreted (conjoin-clauses acl2::x)
                                    acl2::a)
                  t))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: ev-uninterpreted-conjoin-clauses-append

(defthm ev-uninterpreted-conjoin-clauses-append
  (iff (ev-uninterpreted (conjoin-clauses (append acl2::x acl2::y))
                         acl2::a)
       (and (ev-uninterpreted (conjoin-clauses acl2::x)
                              acl2::a)
            (ev-uninterpreted (conjoin-clauses acl2::y)
                              acl2::a))))

Function: lambda->actuals-fix

(defun lambda->actuals-fix (formals actuals)
  (declare (xargs :guard (and (symbol-listp formals)
                              (pseudo-term-listp actuals))))
  (let ((acl2::__function__ 'lambda->actuals-fix))
    (declare (ignorable acl2::__function__))
    (b* ((formals (symbol-list-fix formals))
         (actuals (pseudo-term-list-fix actuals))
         (len-formals (len formals))
         (len-actuals (len actuals))
         ((if (equal len-formals len-actuals))
          actuals))
      nil)))

Theorem: pseudo-term-listp-of-lambda->actuals-fix

(defthm pseudo-term-listp-of-lambda->actuals-fix
  (b* ((new-actuals (lambda->actuals-fix formals actuals)))
    (pseudo-term-listp new-actuals))
  :rule-classes :rewrite)

Function: lambda->formals-fix

(defun lambda->formals-fix (formals actuals)
  (declare (xargs :guard (and (symbol-listp formals)
                              (pseudo-term-listp actuals))))
  (let ((acl2::__function__ 'lambda->formals-fix))
    (declare (ignorable acl2::__function__))
    (b* ((formals (symbol-list-fix formals))
         (actuals (pseudo-term-list-fix actuals))
         (len-formals (len formals))
         (len-actuals (len actuals))
         ((if (equal len-formals len-actuals))
          formals))
      nil)))

Theorem: symbol-listp-of-lambda->formals-fix

(defthm symbol-listp-of-lambda->formals-fix
  (b* ((new-formals (lambda->formals-fix formals actuals)))
    (symbol-listp new-formals))
  :rule-classes :rewrite)

Function: lambda-binding-p

(defun lambda-binding-p (x)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'lambda-binding-p))
    (declare (ignorable acl2::__function__))
    (and (mbe :logic (and (alistp x)
                          (equal (strip-cars x)
                                 '(formals actuals)))
              :exec (fty::alist-with-carsp x '(formals actuals)))
         (b* ((formals (cdr (std::da-nth 0 x)))
              (actuals (cdr (std::da-nth 1 x))))
           (and (symbol-listp formals)
                (pseudo-term-listp actuals)
                (equal (len formals) (len actuals)))))))

Theorem: consp-when-lambda-binding-p

(defthm consp-when-lambda-binding-p
  (implies (lambda-binding-p x) (consp x))
  :rule-classes :compound-recognizer)

Function: lambda-binding-fix$inline

(defun lambda-binding-fix$inline (x)
 (declare (xargs :guard (lambda-binding-p x)))
 (let ((acl2::__function__ 'lambda-binding-fix))
  (declare (ignorable acl2::__function__))
  (mbe
      :logic
      (b* ((formals (symbol-list-fix (cdr (std::da-nth 0 x))))
           (actuals (pseudo-term-list-fix (cdr (std::da-nth 1 x)))))
        (let ((formals (lambda->formals-fix formals actuals))
              (actuals (lambda->actuals-fix formals actuals)))
          (list (cons 'formals formals)
                (cons 'actuals actuals))))
      :exec x)))

Theorem: lambda-binding-p-of-lambda-binding-fix

(defthm lambda-binding-p-of-lambda-binding-fix
  (b* ((new-x (lambda-binding-fix$inline x)))
    (lambda-binding-p new-x))
  :rule-classes :rewrite)

Theorem: lambda-binding-fix-when-lambda-binding-p

(defthm lambda-binding-fix-when-lambda-binding-p
  (implies (lambda-binding-p x)
           (equal (lambda-binding-fix x) x)))

Function: lambda-binding-equiv$inline

(defun lambda-binding-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (lambda-binding-p acl2::x)
                              (lambda-binding-p acl2::y))))
  (equal (lambda-binding-fix acl2::x)
         (lambda-binding-fix acl2::y)))

Theorem: lambda-binding-equiv-is-an-equivalence

(defthm lambda-binding-equiv-is-an-equivalence
  (and (booleanp (lambda-binding-equiv x y))
       (lambda-binding-equiv x x)
       (implies (lambda-binding-equiv x y)
                (lambda-binding-equiv y x))
       (implies (and (lambda-binding-equiv x y)
                     (lambda-binding-equiv y z))
                (lambda-binding-equiv x z)))
  :rule-classes (:equivalence))

Theorem: lambda-binding-equiv-implies-equal-lambda-binding-fix-1

(defthm lambda-binding-equiv-implies-equal-lambda-binding-fix-1
  (implies (lambda-binding-equiv acl2::x x-equiv)
           (equal (lambda-binding-fix acl2::x)
                  (lambda-binding-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: lambda-binding-fix-under-lambda-binding-equiv

(defthm lambda-binding-fix-under-lambda-binding-equiv
  (lambda-binding-equiv (lambda-binding-fix acl2::x)
                        acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-lambda-binding-fix-1-forward-to-lambda-binding-equiv

(defthm
      equal-of-lambda-binding-fix-1-forward-to-lambda-binding-equiv
  (implies (equal (lambda-binding-fix acl2::x)
                  acl2::y)
           (lambda-binding-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: equal-of-lambda-binding-fix-2-forward-to-lambda-binding-equiv

(defthm
      equal-of-lambda-binding-fix-2-forward-to-lambda-binding-equiv
  (implies (equal acl2::x (lambda-binding-fix acl2::y))
           (lambda-binding-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: lambda-binding-equiv-of-lambda-binding-fix-1-forward

(defthm lambda-binding-equiv-of-lambda-binding-fix-1-forward
  (implies (lambda-binding-equiv (lambda-binding-fix acl2::x)
                                 acl2::y)
           (lambda-binding-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: lambda-binding-equiv-of-lambda-binding-fix-2-forward

(defthm lambda-binding-equiv-of-lambda-binding-fix-2-forward
  (implies
       (lambda-binding-equiv acl2::x (lambda-binding-fix acl2::y))
       (lambda-binding-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Function: lambda-binding->formals$inline

(defun lambda-binding->formals$inline (x)
 (declare (xargs :guard (lambda-binding-p x)))
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'lambda-binding->formals))
  (declare (ignorable acl2::__function__))
  (mbe
      :logic
      (b* ((x (and t x))
           (formals (symbol-list-fix (cdr (std::da-nth 0 x))))
           (actuals (pseudo-term-list-fix (cdr (std::da-nth 1 x)))))
        (lambda->formals-fix formals actuals))
      :exec (cdr (std::da-nth 0 x)))))

Theorem: symbol-listp-of-lambda-binding->formals

(defthm symbol-listp-of-lambda-binding->formals
  (b* ((formals (lambda-binding->formals$inline x)))
    (symbol-listp formals))
  :rule-classes :rewrite)

Theorem: lambda-binding->formals$inline-of-lambda-binding-fix-x

(defthm lambda-binding->formals$inline-of-lambda-binding-fix-x
  (equal (lambda-binding->formals$inline (lambda-binding-fix x))
         (lambda-binding->formals$inline x)))

Theorem: lambda-binding->formals$inline-lambda-binding-equiv-congruence-on-x

(defthm
 lambda-binding->formals$inline-lambda-binding-equiv-congruence-on-x
 (implies (lambda-binding-equiv x x-equiv)
          (equal (lambda-binding->formals$inline x)
                 (lambda-binding->formals$inline x-equiv)))
 :rule-classes :congruence)

Function: lambda-binding->actuals$inline

(defun lambda-binding->actuals$inline (x)
 (declare (xargs :guard (lambda-binding-p x)))
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'lambda-binding->actuals))
  (declare (ignorable acl2::__function__))
  (mbe
      :logic
      (b* ((x (and t x))
           (formals (symbol-list-fix (cdr (std::da-nth 0 x))))
           (actuals (pseudo-term-list-fix (cdr (std::da-nth 1 x)))))
        (lambda->actuals-fix formals actuals))
      :exec (cdr (std::da-nth 1 x)))))

Theorem: pseudo-term-listp-of-lambda-binding->actuals

(defthm pseudo-term-listp-of-lambda-binding->actuals
  (b* ((actuals (lambda-binding->actuals$inline x)))
    (pseudo-term-listp actuals))
  :rule-classes :rewrite)

Theorem: lambda-binding->actuals$inline-of-lambda-binding-fix-x

(defthm lambda-binding->actuals$inline-of-lambda-binding-fix-x
  (equal (lambda-binding->actuals$inline (lambda-binding-fix x))
         (lambda-binding->actuals$inline x)))

Theorem: lambda-binding->actuals$inline-lambda-binding-equiv-congruence-on-x

(defthm
 lambda-binding->actuals$inline-lambda-binding-equiv-congruence-on-x
 (implies (lambda-binding-equiv x x-equiv)
          (equal (lambda-binding->actuals$inline x)
                 (lambda-binding->actuals$inline x-equiv)))
 :rule-classes :congruence)

Function: lambda-binding

(defun lambda-binding (formals actuals)
 (declare (xargs :guard (and (symbol-listp formals)
                             (pseudo-term-listp actuals))))
 (declare (xargs :guard (equal (len formals) (len actuals))))
 (let ((acl2::__function__ 'lambda-binding))
  (declare (ignorable acl2::__function__))
  (b* ((formals (mbe :logic (symbol-list-fix formals)
                     :exec formals))
       (actuals (mbe :logic (pseudo-term-list-fix actuals)
                     :exec actuals)))
    (let ((formals (mbe :logic (lambda->formals-fix formals actuals)
                        :exec formals))
          (actuals (mbe :logic (lambda->actuals-fix formals actuals)
                        :exec actuals)))
      (list (cons 'formals formals)
            (cons 'actuals actuals))))))

Theorem: lambda-binding-p-of-lambda-binding

(defthm lambda-binding-p-of-lambda-binding
  (b* ((x (lambda-binding formals actuals)))
    (lambda-binding-p x))
  :rule-classes :rewrite)

Theorem: lambda-binding->formals-of-lambda-binding

(defthm lambda-binding->formals-of-lambda-binding
  (equal (lambda-binding->formals (lambda-binding formals actuals))
         (b* ((acl2::?formals (symbol-list-fix formals))
              (?actuals (pseudo-term-list-fix actuals)))
           (lambda->formals-fix formals actuals))))

Theorem: lambda-binding->actuals-of-lambda-binding

(defthm lambda-binding->actuals-of-lambda-binding
  (equal (lambda-binding->actuals (lambda-binding formals actuals))
         (b* ((acl2::?formals (symbol-list-fix formals))
              (?actuals (pseudo-term-list-fix actuals)))
           (lambda->actuals-fix formals actuals))))

Theorem: lambda-binding-requirements

(defthm lambda-binding-requirements
  (b* ((acl2::?formals (lambda-binding->formals x))
       (?actuals (lambda-binding->actuals x)))
    (equal (len formals) (len actuals))))

Theorem: lambda-binding-of-fields

(defthm lambda-binding-of-fields
  (equal (lambda-binding (lambda-binding->formals x)
                         (lambda-binding->actuals x))
         (lambda-binding-fix x)))

Theorem: lambda-binding-fix-when-lambda-binding

(defthm lambda-binding-fix-when-lambda-binding
  (equal (lambda-binding-fix x)
         (lambda-binding (lambda-binding->formals x)
                         (lambda-binding->actuals x))))

Theorem: equal-of-lambda-binding

(defthm equal-of-lambda-binding
  (equal (equal (lambda-binding formals actuals)
                x)
         (and (lambda-binding-p x)
              (equal (lambda-binding->formals x)
                     (b* ((acl2::?formals (symbol-list-fix formals))
                          (?actuals (pseudo-term-list-fix actuals)))
                       (lambda->formals-fix formals actuals)))
              (equal (lambda-binding->actuals x)
                     (b* ((acl2::?formals (symbol-list-fix formals))
                          (?actuals (pseudo-term-list-fix actuals)))
                       (lambda->actuals-fix formals actuals))))))

Theorem: lambda-binding-of-symbol-list-fix-formals

(defthm lambda-binding-of-symbol-list-fix-formals
  (equal (lambda-binding (symbol-list-fix formals)
                         actuals)
         (lambda-binding formals actuals)))

Theorem: lambda-binding-symbol-list-equiv-congruence-on-formals

(defthm lambda-binding-symbol-list-equiv-congruence-on-formals
  (implies (acl2::symbol-list-equiv formals formals-equiv)
           (equal (lambda-binding formals actuals)
                  (lambda-binding formals-equiv actuals)))
  :rule-classes :congruence)

Theorem: lambda-binding-of-pseudo-term-list-fix-actuals

(defthm lambda-binding-of-pseudo-term-list-fix-actuals
  (equal (lambda-binding formals (pseudo-term-list-fix actuals))
         (lambda-binding formals actuals)))

Theorem: lambda-binding-pseudo-term-list-equiv-congruence-on-actuals

(defthm lambda-binding-pseudo-term-list-equiv-congruence-on-actuals
  (implies (pseudo-term-list-equiv actuals actuals-equiv)
           (equal (lambda-binding formals actuals)
                  (lambda-binding formals actuals-equiv)))
  :rule-classes :congruence)

Theorem: lambda-binding-fix-redef

(defthm lambda-binding-fix-redef
  (equal (lambda-binding-fix x)
         (lambda-binding (lambda-binding->formals x)
                         (lambda-binding->actuals x)))
  :rule-classes :definition)

Function: lambda-binding-listp

(defun lambda-binding-listp (x)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'lambda-binding-listp))
    (declare (ignorable acl2::__function__))
    (if (atom x)
        (eq x nil)
      (and (lambda-binding-p (car x))
           (lambda-binding-listp (cdr x))))))

Theorem: lambda-binding-listp-of-cons

(defthm lambda-binding-listp-of-cons
  (equal (lambda-binding-listp (cons acl2::a acl2::x))
         (and (lambda-binding-p acl2::a)
              (lambda-binding-listp acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-cdr-when-lambda-binding-listp

(defthm lambda-binding-listp-of-cdr-when-lambda-binding-listp
  (implies (lambda-binding-listp (double-rewrite acl2::x))
           (lambda-binding-listp (cdr acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-when-not-consp

(defthm lambda-binding-listp-when-not-consp
  (implies (not (consp acl2::x))
           (equal (lambda-binding-listp acl2::x)
                  (not acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-p-of-car-when-lambda-binding-listp

(defthm lambda-binding-p-of-car-when-lambda-binding-listp
  (implies (lambda-binding-listp acl2::x)
           (iff (lambda-binding-p (car acl2::x))
                (or (consp acl2::x)
                    (lambda-binding-p nil))))
  :rule-classes ((:rewrite)))

Theorem: true-listp-when-lambda-binding-listp-compound-recognizer

(defthm true-listp-when-lambda-binding-listp-compound-recognizer
  (implies (lambda-binding-listp acl2::x)
           (true-listp acl2::x))
  :rule-classes :compound-recognizer)

Theorem: lambda-binding-listp-of-list-fix

(defthm lambda-binding-listp-of-list-fix
  (implies (lambda-binding-listp acl2::x)
           (lambda-binding-listp (acl2::list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-sfix

(defthm lambda-binding-listp-of-sfix
  (iff (lambda-binding-listp (set::sfix acl2::x))
       (or (lambda-binding-listp acl2::x)
           (not (set::setp acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-insert

(defthm lambda-binding-listp-of-insert
  (iff (lambda-binding-listp (set::insert acl2::a acl2::x))
       (and (lambda-binding-listp (set::sfix acl2::x))
            (lambda-binding-p acl2::a)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-delete

(defthm lambda-binding-listp-of-delete
  (implies (lambda-binding-listp acl2::x)
           (lambda-binding-listp (set::delete acl2::k acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-mergesort

(defthm lambda-binding-listp-of-mergesort
  (iff (lambda-binding-listp (set::mergesort acl2::x))
       (lambda-binding-listp (acl2::list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-union

(defthm lambda-binding-listp-of-union
  (iff (lambda-binding-listp (set::union acl2::x acl2::y))
       (and (lambda-binding-listp (set::sfix acl2::x))
            (lambda-binding-listp (set::sfix acl2::y))))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-intersect-1

(defthm lambda-binding-listp-of-intersect-1
  (implies (lambda-binding-listp acl2::x)
           (lambda-binding-listp (set::intersect acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-intersect-2

(defthm lambda-binding-listp-of-intersect-2
  (implies (lambda-binding-listp acl2::y)
           (lambda-binding-listp (set::intersect acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-difference

(defthm lambda-binding-listp-of-difference
  (implies (lambda-binding-listp acl2::x)
           (lambda-binding-listp (set::difference acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-duplicated-members

(defthm lambda-binding-listp-of-duplicated-members
 (implies (lambda-binding-listp acl2::x)
          (lambda-binding-listp (acl2::duplicated-members acl2::x)))
 :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-rev

(defthm lambda-binding-listp-of-rev
  (equal (lambda-binding-listp (acl2::rev acl2::x))
         (lambda-binding-listp (acl2::list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-append

(defthm lambda-binding-listp-of-append
  (equal (lambda-binding-listp (append acl2::a acl2::b))
         (and (lambda-binding-listp (acl2::list-fix acl2::a))
              (lambda-binding-listp acl2::b)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-rcons

(defthm lambda-binding-listp-of-rcons
  (iff (lambda-binding-listp (acl2::rcons acl2::a acl2::x))
       (and (lambda-binding-p acl2::a)
            (lambda-binding-listp (acl2::list-fix acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-p-when-member-equal-of-lambda-binding-listp

(defthm lambda-binding-p-when-member-equal-of-lambda-binding-listp
  (and (implies (and (member-equal acl2::a acl2::x)
                     (lambda-binding-listp acl2::x))
                (lambda-binding-p acl2::a))
       (implies (and (lambda-binding-listp acl2::x)
                     (member-equal acl2::a acl2::x))
                (lambda-binding-p acl2::a)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-when-subsetp-equal

(defthm lambda-binding-listp-when-subsetp-equal
  (and (implies (and (subsetp-equal acl2::x acl2::y)
                     (lambda-binding-listp acl2::y))
                (equal (lambda-binding-listp acl2::x)
                       (true-listp acl2::x)))
       (implies (and (lambda-binding-listp acl2::y)
                     (subsetp-equal acl2::x acl2::y))
                (equal (lambda-binding-listp acl2::x)
                       (true-listp acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-set-difference-equal

(defthm lambda-binding-listp-of-set-difference-equal
 (implies
      (lambda-binding-listp acl2::x)
      (lambda-binding-listp (set-difference-equal acl2::x acl2::y)))
 :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-intersection-equal-1

(defthm lambda-binding-listp-of-intersection-equal-1
  (implies
       (lambda-binding-listp (double-rewrite acl2::x))
       (lambda-binding-listp (intersection-equal acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-intersection-equal-2

(defthm lambda-binding-listp-of-intersection-equal-2
  (implies
       (lambda-binding-listp (double-rewrite acl2::y))
       (lambda-binding-listp (intersection-equal acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-union-equal

(defthm lambda-binding-listp-of-union-equal
  (equal (lambda-binding-listp (union-equal acl2::x acl2::y))
         (and (lambda-binding-listp (acl2::list-fix acl2::x))
              (lambda-binding-listp (double-rewrite acl2::y))))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-take

(defthm lambda-binding-listp-of-take
  (implies (lambda-binding-listp (double-rewrite acl2::x))
           (iff (lambda-binding-listp (take acl2::n acl2::x))
                (or (lambda-binding-p nil)
                    (<= (nfix acl2::n) (len acl2::x)))))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-repeat

(defthm lambda-binding-listp-of-repeat
  (iff (lambda-binding-listp (acl2::repeat acl2::n acl2::x))
       (or (lambda-binding-p acl2::x)
           (zp acl2::n)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-p-of-nth-when-lambda-binding-listp

(defthm lambda-binding-p-of-nth-when-lambda-binding-listp
  (implies (and (lambda-binding-listp acl2::x)
                (< (nfix acl2::n) (len acl2::x)))
           (lambda-binding-p (nth acl2::n acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-update-nth

(defthm lambda-binding-listp-of-update-nth
 (implies
    (lambda-binding-listp (double-rewrite acl2::x))
    (iff (lambda-binding-listp (update-nth acl2::n acl2::y acl2::x))
         (and (lambda-binding-p acl2::y)
              (or (<= (nfix acl2::n) (len acl2::x))
                  (lambda-binding-p nil)))))
 :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-butlast

(defthm lambda-binding-listp-of-butlast
  (implies (lambda-binding-listp (double-rewrite acl2::x))
           (lambda-binding-listp (butlast acl2::x acl2::n)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-nthcdr

(defthm lambda-binding-listp-of-nthcdr
  (implies (lambda-binding-listp (double-rewrite acl2::x))
           (lambda-binding-listp (nthcdr acl2::n acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-last

(defthm lambda-binding-listp-of-last
  (implies (lambda-binding-listp (double-rewrite acl2::x))
           (lambda-binding-listp (last acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-remove

(defthm lambda-binding-listp-of-remove
  (implies (lambda-binding-listp acl2::x)
           (lambda-binding-listp (remove acl2::a acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: lambda-binding-listp-of-revappend

(defthm lambda-binding-listp-of-revappend
  (equal (lambda-binding-listp (revappend acl2::x acl2::y))
         (and (lambda-binding-listp (acl2::list-fix acl2::x))
              (lambda-binding-listp acl2::y)))
  :rule-classes ((:rewrite)))

Function: lambda-binding-list-fix$inline

(defun lambda-binding-list-fix$inline (x)
  (declare (xargs :guard (lambda-binding-listp x)))
  (let ((acl2::__function__ 'lambda-binding-list-fix))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (if (atom x)
             nil
           (cons (lambda-binding-fix (car x))
                 (lambda-binding-list-fix (cdr x))))
         :exec x)))

Theorem: lambda-binding-listp-of-lambda-binding-list-fix

(defthm lambda-binding-listp-of-lambda-binding-list-fix
  (b* ((fty::newx (lambda-binding-list-fix$inline x)))
    (lambda-binding-listp fty::newx))
  :rule-classes :rewrite)

Theorem: lambda-binding-list-fix-when-lambda-binding-listp

(defthm lambda-binding-list-fix-when-lambda-binding-listp
  (implies (lambda-binding-listp x)
           (equal (lambda-binding-list-fix x) x)))

Function: lambda-binding-list-equiv$inline

(defun lambda-binding-list-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (lambda-binding-listp acl2::x)
                              (lambda-binding-listp acl2::y))))
  (equal (lambda-binding-list-fix acl2::x)
         (lambda-binding-list-fix acl2::y)))

Theorem: lambda-binding-list-equiv-is-an-equivalence

(defthm lambda-binding-list-equiv-is-an-equivalence
  (and (booleanp (lambda-binding-list-equiv x y))
       (lambda-binding-list-equiv x x)
       (implies (lambda-binding-list-equiv x y)
                (lambda-binding-list-equiv y x))
       (implies (and (lambda-binding-list-equiv x y)
                     (lambda-binding-list-equiv y z))
                (lambda-binding-list-equiv x z)))
  :rule-classes (:equivalence))

Theorem: lambda-binding-list-equiv-implies-equal-lambda-binding-list-fix-1

(defthm
  lambda-binding-list-equiv-implies-equal-lambda-binding-list-fix-1
  (implies (lambda-binding-list-equiv acl2::x x-equiv)
           (equal (lambda-binding-list-fix acl2::x)
                  (lambda-binding-list-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: lambda-binding-list-fix-under-lambda-binding-list-equiv

(defthm lambda-binding-list-fix-under-lambda-binding-list-equiv
  (lambda-binding-list-equiv (lambda-binding-list-fix acl2::x)
                             acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-lambda-binding-list-fix-1-forward-to-lambda-binding-list-equiv

(defthm
 equal-of-lambda-binding-list-fix-1-forward-to-lambda-binding-list-equiv
 (implies (equal (lambda-binding-list-fix acl2::x)
                 acl2::y)
          (lambda-binding-list-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Theorem: equal-of-lambda-binding-list-fix-2-forward-to-lambda-binding-list-equiv

(defthm
 equal-of-lambda-binding-list-fix-2-forward-to-lambda-binding-list-equiv
 (implies (equal acl2::x
                 (lambda-binding-list-fix acl2::y))
          (lambda-binding-list-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Theorem: lambda-binding-list-equiv-of-lambda-binding-list-fix-1-forward

(defthm
     lambda-binding-list-equiv-of-lambda-binding-list-fix-1-forward
  (implies
       (lambda-binding-list-equiv (lambda-binding-list-fix acl2::x)
                                  acl2::y)
       (lambda-binding-list-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: lambda-binding-list-equiv-of-lambda-binding-list-fix-2-forward

(defthm
     lambda-binding-list-equiv-of-lambda-binding-list-fix-2-forward
  (implies
       (lambda-binding-list-equiv acl2::x
                                  (lambda-binding-list-fix acl2::y))
       (lambda-binding-list-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: car-of-lambda-binding-list-fix-x-under-lambda-binding-equiv

(defthm car-of-lambda-binding-list-fix-x-under-lambda-binding-equiv
  (lambda-binding-equiv (car (lambda-binding-list-fix acl2::x))
                        (car acl2::x)))

Theorem: car-lambda-binding-list-equiv-congruence-on-x-under-lambda-binding-equiv

(defthm
 car-lambda-binding-list-equiv-congruence-on-x-under-lambda-binding-equiv
 (implies (lambda-binding-list-equiv acl2::x x-equiv)
          (lambda-binding-equiv (car acl2::x)
                                (car x-equiv)))
 :rule-classes :congruence)

Theorem: cdr-of-lambda-binding-list-fix-x-under-lambda-binding-list-equiv

(defthm
   cdr-of-lambda-binding-list-fix-x-under-lambda-binding-list-equiv
  (lambda-binding-list-equiv (cdr (lambda-binding-list-fix acl2::x))
                             (cdr acl2::x)))

Theorem: cdr-lambda-binding-list-equiv-congruence-on-x-under-lambda-binding-list-equiv

(defthm
 cdr-lambda-binding-list-equiv-congruence-on-x-under-lambda-binding-list-equiv
 (implies (lambda-binding-list-equiv acl2::x x-equiv)
          (lambda-binding-list-equiv (cdr acl2::x)
                                     (cdr x-equiv)))
 :rule-classes :congruence)

Theorem: cons-of-lambda-binding-fix-x-under-lambda-binding-list-equiv

(defthm cons-of-lambda-binding-fix-x-under-lambda-binding-list-equiv
  (lambda-binding-list-equiv (cons (lambda-binding-fix acl2::x)
                                   acl2::y)
                             (cons acl2::x acl2::y)))

Theorem: cons-lambda-binding-equiv-congruence-on-x-under-lambda-binding-list-equiv

(defthm
 cons-lambda-binding-equiv-congruence-on-x-under-lambda-binding-list-equiv
 (implies (lambda-binding-equiv acl2::x x-equiv)
          (lambda-binding-list-equiv (cons acl2::x acl2::y)
                                     (cons x-equiv acl2::y)))
 :rule-classes :congruence)

Theorem: cons-of-lambda-binding-list-fix-y-under-lambda-binding-list-equiv

(defthm
  cons-of-lambda-binding-list-fix-y-under-lambda-binding-list-equiv
 (lambda-binding-list-equiv (cons acl2::x
                                  (lambda-binding-list-fix acl2::y))
                            (cons acl2::x acl2::y)))

Theorem: cons-lambda-binding-list-equiv-congruence-on-y-under-lambda-binding-list-equiv

(defthm
 cons-lambda-binding-list-equiv-congruence-on-y-under-lambda-binding-list-equiv
 (implies (lambda-binding-list-equiv acl2::y y-equiv)
          (lambda-binding-list-equiv (cons acl2::x acl2::y)
                                     (cons acl2::x y-equiv)))
 :rule-classes :congruence)

Theorem: consp-of-lambda-binding-list-fix

(defthm consp-of-lambda-binding-list-fix
  (equal (consp (lambda-binding-list-fix acl2::x))
         (consp acl2::x)))

Theorem: lambda-binding-list-fix-under-iff

(defthm lambda-binding-list-fix-under-iff
  (iff (lambda-binding-list-fix acl2::x)
       (consp acl2::x)))

Theorem: lambda-binding-list-fix-of-cons

(defthm lambda-binding-list-fix-of-cons
  (equal (lambda-binding-list-fix (cons a x))
         (cons (lambda-binding-fix a)
               (lambda-binding-list-fix x))))

Theorem: len-of-lambda-binding-list-fix

(defthm len-of-lambda-binding-list-fix
  (equal (len (lambda-binding-list-fix acl2::x))
         (len acl2::x)))

Theorem: lambda-binding-list-fix-of-append

(defthm lambda-binding-list-fix-of-append
  (equal (lambda-binding-list-fix (append std::a std::b))
         (append (lambda-binding-list-fix std::a)
                 (lambda-binding-list-fix std::b))))

Theorem: lambda-binding-list-fix-of-repeat

(defthm lambda-binding-list-fix-of-repeat
  (equal (lambda-binding-list-fix (acl2::repeat acl2::n acl2::x))
         (acl2::repeat acl2::n (lambda-binding-fix acl2::x))))

Theorem: list-equiv-refines-lambda-binding-list-equiv

(defthm list-equiv-refines-lambda-binding-list-equiv
  (implies (acl2::list-equiv acl2::x acl2::y)
           (lambda-binding-list-equiv acl2::x acl2::y))
  :rule-classes :refinement)

Theorem: nth-of-lambda-binding-list-fix

(defthm nth-of-lambda-binding-list-fix
  (equal (nth acl2::n
              (lambda-binding-list-fix acl2::x))
         (if (< (nfix acl2::n) (len acl2::x))
             (lambda-binding-fix (nth acl2::n acl2::x))
           nil)))

Theorem: lambda-binding-list-equiv-implies-lambda-binding-list-equiv-append-1

(defthm
 lambda-binding-list-equiv-implies-lambda-binding-list-equiv-append-1
 (implies (lambda-binding-list-equiv acl2::x fty::x-equiv)
          (lambda-binding-list-equiv (append acl2::x acl2::y)
                                     (append fty::x-equiv acl2::y)))
 :rule-classes (:congruence))

Theorem: lambda-binding-list-equiv-implies-lambda-binding-list-equiv-append-2

(defthm
 lambda-binding-list-equiv-implies-lambda-binding-list-equiv-append-2
 (implies (lambda-binding-list-equiv acl2::y fty::y-equiv)
          (lambda-binding-list-equiv (append acl2::x acl2::y)
                                     (append acl2::x fty::y-equiv)))
 :rule-classes (:congruence))

Theorem: lambda-binding-list-equiv-implies-lambda-binding-list-equiv-nthcdr-2

(defthm
 lambda-binding-list-equiv-implies-lambda-binding-list-equiv-nthcdr-2
 (implies (lambda-binding-list-equiv acl2::l l-equiv)
          (lambda-binding-list-equiv (nthcdr acl2::n acl2::l)
                                     (nthcdr acl2::n l-equiv)))
 :rule-classes (:congruence))

Theorem: lambda-binding-list-equiv-implies-lambda-binding-list-equiv-take-2

(defthm
 lambda-binding-list-equiv-implies-lambda-binding-list-equiv-take-2
 (implies (lambda-binding-list-equiv acl2::l l-equiv)
          (lambda-binding-list-equiv (take acl2::n acl2::l)
                                     (take acl2::n l-equiv)))
 :rule-classes (:congruence))

Function: fhg-single-args-p

(defun fhg-single-args-p (x)
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'fhg-single-args-p))
  (declare (ignorable acl2::__function__))
  (and
   (mbe
      :logic (and (alistp x)
                  (equal (strip-cars x)
                         '(fn actuals fn-returns-hint-acc
                              fn-more-returns-hint-acc lambda-acc)))
      :exec (fty::alist-with-carsp
                 x
                 '(fn actuals fn-returns-hint-acc
                      fn-more-returns-hint-acc lambda-acc)))
   (b* ((fn (cdr (std::da-nth 0 x)))
        (actuals (cdr (std::da-nth 1 x)))
        (fn-returns-hint-acc (cdr (std::da-nth 2 x)))
        (fn-more-returns-hint-acc (cdr (std::da-nth 3 x)))
        (lambda-acc (cdr (std::da-nth 4 x))))
     (and (func-p fn)
          (pseudo-term-listp actuals)
          (hint-pair-listp fn-returns-hint-acc)
          (hint-pair-listp fn-more-returns-hint-acc)
          (lambda-binding-listp lambda-acc))))))

Theorem: consp-when-fhg-single-args-p

(defthm consp-when-fhg-single-args-p
  (implies (fhg-single-args-p x)
           (consp x))
  :rule-classes :compound-recognizer)

Function: fhg-single-args-fix$inline

(defun fhg-single-args-fix$inline (x)
 (declare (xargs :guard (fhg-single-args-p x)))
 (let ((acl2::__function__ 'fhg-single-args-fix))
  (declare (ignorable acl2::__function__))
  (mbe
   :logic
   (b*
    ((fn (func-fix (cdr (std::da-nth 0 x))))
     (actuals (pseudo-term-list-fix (cdr (std::da-nth 1 x))))
     (fn-returns-hint-acc
          (hint-pair-list-fix (cdr (std::da-nth 2 x))))
     (fn-more-returns-hint-acc
          (hint-pair-list-fix (cdr (std::da-nth 3 x))))
     (lambda-acc (lambda-binding-list-fix (cdr (std::da-nth 4 x)))))
    (list (cons 'fn fn)
          (cons 'actuals actuals)
          (cons 'fn-returns-hint-acc
                fn-returns-hint-acc)
          (cons 'fn-more-returns-hint-acc
                fn-more-returns-hint-acc)
          (cons 'lambda-acc lambda-acc)))
   :exec x)))

Theorem: fhg-single-args-p-of-fhg-single-args-fix

(defthm fhg-single-args-p-of-fhg-single-args-fix
  (b* ((new-x (fhg-single-args-fix$inline x)))
    (fhg-single-args-p new-x))
  :rule-classes :rewrite)

Theorem: fhg-single-args-fix-when-fhg-single-args-p

(defthm fhg-single-args-fix-when-fhg-single-args-p
  (implies (fhg-single-args-p x)
           (equal (fhg-single-args-fix x) x)))

Function: fhg-single-args-equiv$inline

(defun fhg-single-args-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (fhg-single-args-p acl2::x)
                              (fhg-single-args-p acl2::y))))
  (equal (fhg-single-args-fix acl2::x)
         (fhg-single-args-fix acl2::y)))

Theorem: fhg-single-args-equiv-is-an-equivalence

(defthm fhg-single-args-equiv-is-an-equivalence
  (and (booleanp (fhg-single-args-equiv x y))
       (fhg-single-args-equiv x x)
       (implies (fhg-single-args-equiv x y)
                (fhg-single-args-equiv y x))
       (implies (and (fhg-single-args-equiv x y)
                     (fhg-single-args-equiv y z))
                (fhg-single-args-equiv x z)))
  :rule-classes (:equivalence))

Theorem: fhg-single-args-equiv-implies-equal-fhg-single-args-fix-1

(defthm fhg-single-args-equiv-implies-equal-fhg-single-args-fix-1
  (implies (fhg-single-args-equiv acl2::x x-equiv)
           (equal (fhg-single-args-fix acl2::x)
                  (fhg-single-args-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: fhg-single-args-fix-under-fhg-single-args-equiv

(defthm fhg-single-args-fix-under-fhg-single-args-equiv
  (fhg-single-args-equiv (fhg-single-args-fix acl2::x)
                         acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-fhg-single-args-fix-1-forward-to-fhg-single-args-equiv

(defthm
    equal-of-fhg-single-args-fix-1-forward-to-fhg-single-args-equiv
  (implies (equal (fhg-single-args-fix acl2::x)
                  acl2::y)
           (fhg-single-args-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: equal-of-fhg-single-args-fix-2-forward-to-fhg-single-args-equiv

(defthm
    equal-of-fhg-single-args-fix-2-forward-to-fhg-single-args-equiv
  (implies (equal acl2::x (fhg-single-args-fix acl2::y))
           (fhg-single-args-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: fhg-single-args-equiv-of-fhg-single-args-fix-1-forward

(defthm fhg-single-args-equiv-of-fhg-single-args-fix-1-forward
  (implies (fhg-single-args-equiv (fhg-single-args-fix acl2::x)
                                  acl2::y)
           (fhg-single-args-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: fhg-single-args-equiv-of-fhg-single-args-fix-2-forward

(defthm fhg-single-args-equiv-of-fhg-single-args-fix-2-forward
  (implies
       (fhg-single-args-equiv acl2::x (fhg-single-args-fix acl2::y))
       (fhg-single-args-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Function: fhg-single-args->fn$inline

(defun fhg-single-args->fn$inline (x)
  (declare (xargs :guard (fhg-single-args-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'fhg-single-args->fn))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (func-fix (cdr (std::da-nth 0 x))))
         :exec (cdr (std::da-nth 0 x)))))

Theorem: func-p-of-fhg-single-args->fn

(defthm func-p-of-fhg-single-args->fn
  (b* ((fn (fhg-single-args->fn$inline x)))
    (func-p fn))
  :rule-classes :rewrite)

Theorem: fhg-single-args->fn$inline-of-fhg-single-args-fix-x

(defthm fhg-single-args->fn$inline-of-fhg-single-args-fix-x
  (equal (fhg-single-args->fn$inline (fhg-single-args-fix x))
         (fhg-single-args->fn$inline x)))

Theorem: fhg-single-args->fn$inline-fhg-single-args-equiv-congruence-on-x

(defthm
   fhg-single-args->fn$inline-fhg-single-args-equiv-congruence-on-x
  (implies (fhg-single-args-equiv x x-equiv)
           (equal (fhg-single-args->fn$inline x)
                  (fhg-single-args->fn$inline x-equiv)))
  :rule-classes :congruence)

Function: fhg-single-args->actuals$inline

(defun fhg-single-args->actuals$inline (x)
  (declare (xargs :guard (fhg-single-args-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'fhg-single-args->actuals))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (pseudo-term-list-fix (cdr (std::da-nth 1 x))))
         :exec (cdr (std::da-nth 1 x)))))

Theorem: pseudo-term-listp-of-fhg-single-args->actuals

(defthm pseudo-term-listp-of-fhg-single-args->actuals
  (b* ((actuals (fhg-single-args->actuals$inline x)))
    (pseudo-term-listp actuals))
  :rule-classes :rewrite)

Theorem: fhg-single-args->actuals$inline-of-fhg-single-args-fix-x

(defthm fhg-single-args->actuals$inline-of-fhg-single-args-fix-x
  (equal (fhg-single-args->actuals$inline (fhg-single-args-fix x))
         (fhg-single-args->actuals$inline x)))

Theorem: fhg-single-args->actuals$inline-fhg-single-args-equiv-congruence-on-x

(defthm
 fhg-single-args->actuals$inline-fhg-single-args-equiv-congruence-on-x
 (implies (fhg-single-args-equiv x x-equiv)
          (equal (fhg-single-args->actuals$inline x)
                 (fhg-single-args->actuals$inline x-equiv)))
 :rule-classes :congruence)

Function: fhg-single-args->fn-returns-hint-acc$inline

(defun fhg-single-args->fn-returns-hint-acc$inline (x)
  (declare (xargs :guard (fhg-single-args-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'fhg-single-args->fn-returns-hint-acc))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (hint-pair-list-fix (cdr (std::da-nth 2 x))))
         :exec (cdr (std::da-nth 2 x)))))

Theorem: hint-pair-listp-of-fhg-single-args->fn-returns-hint-acc

(defthm hint-pair-listp-of-fhg-single-args->fn-returns-hint-acc
  (b* ((fn-returns-hint-acc
            (fhg-single-args->fn-returns-hint-acc$inline x)))
    (hint-pair-listp fn-returns-hint-acc))
  :rule-classes :rewrite)

Theorem: fhg-single-args->fn-returns-hint-acc$inline-of-fhg-single-args-fix-x

(defthm
 fhg-single-args->fn-returns-hint-acc$inline-of-fhg-single-args-fix-x
 (equal (fhg-single-args->fn-returns-hint-acc$inline
             (fhg-single-args-fix x))
        (fhg-single-args->fn-returns-hint-acc$inline x)))

Theorem: fhg-single-args->fn-returns-hint-acc$inline-fhg-single-args-equiv-congruence-on-x

(defthm
 fhg-single-args->fn-returns-hint-acc$inline-fhg-single-args-equiv-congruence-on-x
 (implies
      (fhg-single-args-equiv x x-equiv)
      (equal (fhg-single-args->fn-returns-hint-acc$inline x)
             (fhg-single-args->fn-returns-hint-acc$inline x-equiv)))
 :rule-classes :congruence)

Function: fhg-single-args->fn-more-returns-hint-acc$inline

(defun fhg-single-args->fn-more-returns-hint-acc$inline (x)
  (declare (xargs :guard (fhg-single-args-p x)))
  (declare (xargs :guard t))
  (let
   ((acl2::__function__ 'fhg-single-args->fn-more-returns-hint-acc))
   (declare (ignorable acl2::__function__))
   (mbe :logic
        (b* ((x (and t x)))
          (hint-pair-list-fix (cdr (std::da-nth 3 x))))
        :exec (cdr (std::da-nth 3 x)))))

Theorem: hint-pair-listp-of-fhg-single-args->fn-more-returns-hint-acc

(defthm hint-pair-listp-of-fhg-single-args->fn-more-returns-hint-acc
  (b* ((fn-more-returns-hint-acc
            (fhg-single-args->fn-more-returns-hint-acc$inline x)))
    (hint-pair-listp fn-more-returns-hint-acc))
  :rule-classes :rewrite)

Theorem: fhg-single-args->fn-more-returns-hint-acc$inline-of-fhg-single-args-fix-x

(defthm
 fhg-single-args->fn-more-returns-hint-acc$inline-of-fhg-single-args-fix-x
 (equal (fhg-single-args->fn-more-returns-hint-acc$inline
             (fhg-single-args-fix x))
        (fhg-single-args->fn-more-returns-hint-acc$inline x)))

Theorem: fhg-single-args->fn-more-returns-hint-acc$inline-fhg-single-args-equiv-congruence-on-x

(defthm
 fhg-single-args->fn-more-returns-hint-acc$inline-fhg-single-args-equiv-congruence-on-x
 (implies
   (fhg-single-args-equiv x x-equiv)
   (equal
        (fhg-single-args->fn-more-returns-hint-acc$inline x)
        (fhg-single-args->fn-more-returns-hint-acc$inline x-equiv)))
 :rule-classes :congruence)

Function: fhg-single-args->lambda-acc$inline

(defun fhg-single-args->lambda-acc$inline (x)
  (declare (xargs :guard (fhg-single-args-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'fhg-single-args->lambda-acc))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (lambda-binding-list-fix (cdr (std::da-nth 4 x))))
         :exec (cdr (std::da-nth 4 x)))))

Theorem: lambda-binding-listp-of-fhg-single-args->lambda-acc

(defthm lambda-binding-listp-of-fhg-single-args->lambda-acc
  (b* ((lambda-acc (fhg-single-args->lambda-acc$inline x)))
    (lambda-binding-listp lambda-acc))
  :rule-classes :rewrite)

Theorem: fhg-single-args->lambda-acc$inline-of-fhg-single-args-fix-x

(defthm fhg-single-args->lambda-acc$inline-of-fhg-single-args-fix-x
 (equal (fhg-single-args->lambda-acc$inline (fhg-single-args-fix x))
        (fhg-single-args->lambda-acc$inline x)))

Theorem: fhg-single-args->lambda-acc$inline-fhg-single-args-equiv-congruence-on-x

(defthm
 fhg-single-args->lambda-acc$inline-fhg-single-args-equiv-congruence-on-x
 (implies (fhg-single-args-equiv x x-equiv)
          (equal (fhg-single-args->lambda-acc$inline x)
                 (fhg-single-args->lambda-acc$inline x-equiv)))
 :rule-classes :congruence)

Function: fhg-single-args

(defun fhg-single-args (fn actuals fn-returns-hint-acc
                           fn-more-returns-hint-acc lambda-acc)
 (declare
      (xargs :guard (and (func-p fn)
                         (pseudo-term-listp actuals)
                         (hint-pair-listp fn-returns-hint-acc)
                         (hint-pair-listp fn-more-returns-hint-acc)
                         (lambda-binding-listp lambda-acc))))
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'fhg-single-args))
   (declare (ignorable acl2::__function__))
   (b*
     ((fn (mbe :logic (func-fix fn) :exec fn))
      (actuals (mbe :logic (pseudo-term-list-fix actuals)
                    :exec actuals))
      (fn-returns-hint-acc
           (mbe :logic (hint-pair-list-fix fn-returns-hint-acc)
                :exec fn-returns-hint-acc))
      (fn-more-returns-hint-acc
           (mbe :logic (hint-pair-list-fix fn-more-returns-hint-acc)
                :exec fn-more-returns-hint-acc))
      (lambda-acc (mbe :logic (lambda-binding-list-fix lambda-acc)
                       :exec lambda-acc)))
     (list (cons 'fn fn)
           (cons 'actuals actuals)
           (cons 'fn-returns-hint-acc
                 fn-returns-hint-acc)
           (cons 'fn-more-returns-hint-acc
                 fn-more-returns-hint-acc)
           (cons 'lambda-acc lambda-acc)))))

Theorem: fhg-single-args-p-of-fhg-single-args

(defthm fhg-single-args-p-of-fhg-single-args
  (b* ((x (fhg-single-args fn actuals fn-returns-hint-acc
                           fn-more-returns-hint-acc lambda-acc)))
    (fhg-single-args-p x))
  :rule-classes :rewrite)

Theorem: fhg-single-args->fn-of-fhg-single-args

(defthm fhg-single-args->fn-of-fhg-single-args
  (equal (fhg-single-args->fn
              (fhg-single-args fn actuals fn-returns-hint-acc
                               fn-more-returns-hint-acc lambda-acc))
         (func-fix fn)))

Theorem: fhg-single-args->actuals-of-fhg-single-args

(defthm fhg-single-args->actuals-of-fhg-single-args
  (equal (fhg-single-args->actuals
              (fhg-single-args fn actuals fn-returns-hint-acc
                               fn-more-returns-hint-acc lambda-acc))
         (pseudo-term-list-fix actuals)))

Theorem: fhg-single-args->fn-returns-hint-acc-of-fhg-single-args

(defthm fhg-single-args->fn-returns-hint-acc-of-fhg-single-args
  (equal (fhg-single-args->fn-returns-hint-acc
              (fhg-single-args fn actuals fn-returns-hint-acc
                               fn-more-returns-hint-acc lambda-acc))
         (hint-pair-list-fix fn-returns-hint-acc)))

Theorem: fhg-single-args->fn-more-returns-hint-acc-of-fhg-single-args

(defthm fhg-single-args->fn-more-returns-hint-acc-of-fhg-single-args
  (equal (fhg-single-args->fn-more-returns-hint-acc
              (fhg-single-args fn actuals fn-returns-hint-acc
                               fn-more-returns-hint-acc lambda-acc))
         (hint-pair-list-fix fn-more-returns-hint-acc)))

Theorem: fhg-single-args->lambda-acc-of-fhg-single-args

(defthm fhg-single-args->lambda-acc-of-fhg-single-args
  (equal (fhg-single-args->lambda-acc
              (fhg-single-args fn actuals fn-returns-hint-acc
                               fn-more-returns-hint-acc lambda-acc))
         (lambda-binding-list-fix lambda-acc)))

Theorem: fhg-single-args-of-fields

(defthm fhg-single-args-of-fields
 (equal
      (fhg-single-args (fhg-single-args->fn x)
                       (fhg-single-args->actuals x)
                       (fhg-single-args->fn-returns-hint-acc x)
                       (fhg-single-args->fn-more-returns-hint-acc x)
                       (fhg-single-args->lambda-acc x))
      (fhg-single-args-fix x)))

Theorem: fhg-single-args-fix-when-fhg-single-args

(defthm fhg-single-args-fix-when-fhg-single-args
 (equal
      (fhg-single-args-fix x)
      (fhg-single-args (fhg-single-args->fn x)
                       (fhg-single-args->actuals x)
                       (fhg-single-args->fn-returns-hint-acc x)
                       (fhg-single-args->fn-more-returns-hint-acc x)
                       (fhg-single-args->lambda-acc x))))

Theorem: equal-of-fhg-single-args

(defthm equal-of-fhg-single-args
 (equal (equal (fhg-single-args fn actuals fn-returns-hint-acc
                                fn-more-returns-hint-acc lambda-acc)
               x)
        (and (fhg-single-args-p x)
             (equal (fhg-single-args->fn x)
                    (func-fix fn))
             (equal (fhg-single-args->actuals x)
                    (pseudo-term-list-fix actuals))
             (equal (fhg-single-args->fn-returns-hint-acc x)
                    (hint-pair-list-fix fn-returns-hint-acc))
             (equal (fhg-single-args->fn-more-returns-hint-acc x)
                    (hint-pair-list-fix fn-more-returns-hint-acc))
             (equal (fhg-single-args->lambda-acc x)
                    (lambda-binding-list-fix lambda-acc)))))

Theorem: fhg-single-args-of-func-fix-fn

(defthm fhg-single-args-of-func-fix-fn
  (equal (fhg-single-args (func-fix fn)
                          actuals fn-returns-hint-acc
                          fn-more-returns-hint-acc lambda-acc)
         (fhg-single-args fn actuals fn-returns-hint-acc
                          fn-more-returns-hint-acc lambda-acc)))

Theorem: fhg-single-args-func-equiv-congruence-on-fn

(defthm fhg-single-args-func-equiv-congruence-on-fn
 (implies
      (func-equiv fn fn-equiv)
      (equal (fhg-single-args fn actuals fn-returns-hint-acc
                              fn-more-returns-hint-acc lambda-acc)
             (fhg-single-args fn-equiv actuals fn-returns-hint-acc
                              fn-more-returns-hint-acc lambda-acc)))
 :rule-classes :congruence)

Theorem: fhg-single-args-of-pseudo-term-list-fix-actuals

(defthm fhg-single-args-of-pseudo-term-list-fix-actuals
  (equal (fhg-single-args fn (pseudo-term-list-fix actuals)
                          fn-returns-hint-acc
                          fn-more-returns-hint-acc lambda-acc)
         (fhg-single-args fn actuals fn-returns-hint-acc
                          fn-more-returns-hint-acc lambda-acc)))

Theorem: fhg-single-args-pseudo-term-list-equiv-congruence-on-actuals

(defthm fhg-single-args-pseudo-term-list-equiv-congruence-on-actuals
 (implies
      (pseudo-term-list-equiv actuals actuals-equiv)
      (equal (fhg-single-args fn actuals fn-returns-hint-acc
                              fn-more-returns-hint-acc lambda-acc)
             (fhg-single-args fn actuals-equiv fn-returns-hint-acc
                              fn-more-returns-hint-acc lambda-acc)))
 :rule-classes :congruence)

Theorem: fhg-single-args-of-hint-pair-list-fix-fn-returns-hint-acc

(defthm fhg-single-args-of-hint-pair-list-fix-fn-returns-hint-acc
  (equal (fhg-single-args fn actuals
                          (hint-pair-list-fix fn-returns-hint-acc)
                          fn-more-returns-hint-acc lambda-acc)
         (fhg-single-args fn actuals fn-returns-hint-acc
                          fn-more-returns-hint-acc lambda-acc)))

Theorem: fhg-single-args-hint-pair-list-equiv-congruence-on-fn-returns-hint-acc

(defthm
 fhg-single-args-hint-pair-list-equiv-congruence-on-fn-returns-hint-acc
 (implies
      (hint-pair-list-equiv fn-returns-hint-acc
                            fn-returns-hint-acc-equiv)
      (equal (fhg-single-args fn actuals fn-returns-hint-acc
                              fn-more-returns-hint-acc lambda-acc)
             (fhg-single-args fn actuals fn-returns-hint-acc-equiv
                              fn-more-returns-hint-acc lambda-acc)))
 :rule-classes :congruence)

Theorem: fhg-single-args-of-hint-pair-list-fix-fn-more-returns-hint-acc

(defthm
     fhg-single-args-of-hint-pair-list-fix-fn-more-returns-hint-acc
 (equal
      (fhg-single-args fn actuals fn-returns-hint-acc
                       (hint-pair-list-fix fn-more-returns-hint-acc)
                       lambda-acc)
      (fhg-single-args fn actuals fn-returns-hint-acc
                       fn-more-returns-hint-acc lambda-acc)))

Theorem: fhg-single-args-hint-pair-list-equiv-congruence-on-fn-more-returns-hint-acc

(defthm
 fhg-single-args-hint-pair-list-equiv-congruence-on-fn-more-returns-hint-acc
 (implies
      (hint-pair-list-equiv fn-more-returns-hint-acc
                            fn-more-returns-hint-acc-equiv)
      (equal (fhg-single-args fn actuals fn-returns-hint-acc
                              fn-more-returns-hint-acc lambda-acc)
             (fhg-single-args fn actuals fn-returns-hint-acc
                              fn-more-returns-hint-acc-equiv
                              lambda-acc)))
 :rule-classes :congruence)

Theorem: fhg-single-args-of-lambda-binding-list-fix-lambda-acc

(defthm fhg-single-args-of-lambda-binding-list-fix-lambda-acc
  (equal (fhg-single-args fn actuals fn-returns-hint-acc
                          fn-more-returns-hint-acc
                          (lambda-binding-list-fix lambda-acc))
         (fhg-single-args fn actuals fn-returns-hint-acc
                          fn-more-returns-hint-acc lambda-acc)))

Theorem: fhg-single-args-lambda-binding-list-equiv-congruence-on-lambda-acc

(defthm
 fhg-single-args-lambda-binding-list-equiv-congruence-on-lambda-acc
 (implies
      (lambda-binding-list-equiv lambda-acc lambda-acc-equiv)
      (equal (fhg-single-args fn actuals fn-returns-hint-acc
                              fn-more-returns-hint-acc lambda-acc)
             (fhg-single-args fn actuals fn-returns-hint-acc
                              fn-more-returns-hint-acc
                              lambda-acc-equiv)))
 :rule-classes :congruence)

Theorem: fhg-single-args-fix-redef

(defthm fhg-single-args-fix-redef
 (equal
      (fhg-single-args-fix x)
      (fhg-single-args (fhg-single-args->fn x)
                       (fhg-single-args->actuals x)
                       (fhg-single-args->fn-returns-hint-acc x)
                       (fhg-single-args->fn-more-returns-hint-acc x)
                       (fhg-single-args->lambda-acc x)))
 :rule-classes :definition)

Function: generate-fn-hint-pair

(defun generate-fn-hint-pair (hypo args flag)
 (declare (xargs :guard (and (hint-pair-p hypo)
                             (fhg-single-args-p args)
                             (symbolp flag))))
 (let ((acl2::__function__ 'generate-fn-hint-pair))
  (declare (ignorable acl2::__function__))
  (b*
   ((hypo (hint-pair-fix hypo))
    (args (fhg-single-args-fix args))
    (flag (symbol-fix flag))
    ((hint-pair h) hypo)
    ((fhg-single-args a) args)
    ((func f) a.fn)
    (formals f.flattened-formals)
    (returns f.flattened-returns)
    ((unless (equal (len returns) 1))
     (prog2$
      (er
       hard?
       'smt-goal-generator=>generate-fn-hint-pair
       "User ~
                defined function with more than one returns is not supported ~
                currently. ~%The function ~q0 has returns ~q1."
       f.name returns)
      (make-hint-pair)))
    ((unless (equal (len formals) (len a.actuals)))
     (prog2$
      (er
       hard?
       'smt-goal-generator=>generate-fn-hint-pair
       "Number ~
                of formals and actuals don't match. ~%Formals: ~q0, actuals: ~q1."
       formals a.actuals)
      (make-hint-pair)))
    ((if (equal f.name 'quote))
     (prog2$ (er hard?
                 'smt-goal-generator=>generate-fn-hint-pair
                 "Function name can't be 'quote.")
             (make-hint-pair)))
    ((unless (or (equal flag 'more-returns)
                 (and (consp h.thm)
                      (symbolp (car h.thm)))))
     (prog2$ (er hard?
                 'smt-goal-generator=>generate-fn-hint-pair
                 "Returns should have consp h.thm.~%")
             (make-hint-pair)))
    (thm (if (equal flag 'more-returns)
             (cons (cons 'lambda
                         (cons (append formals returns)
                               (cons h.thm 'nil)))
                   (append a.actuals
                           (cons (cons f.name a.actuals) 'nil)))
           (cons (car h.thm)
                 (cons (cons f.name a.actuals) 'nil)))))
   (change-hint-pair h :thm thm))))

Theorem: hint-pair-p-of-generate-fn-hint-pair

(defthm hint-pair-p-of-generate-fn-hint-pair
  (b* ((fn-hint-pair (generate-fn-hint-pair hypo args flag)))
    (hint-pair-p fn-hint-pair))
  :rule-classes :rewrite)

Function: generate-fn-returns-hint

(defun generate-fn-returns-hint (returns args)
 (declare (xargs :guard (and (decl-listp returns)
                             (fhg-single-args-p args))))
 (let ((acl2::__function__ 'generate-fn-returns-hint))
  (declare (ignorable acl2::__function__))
  (b*
    ((returns (decl-list-fix returns))
     (args (fhg-single-args-fix args))
     ((fhg-single-args a) args)
     ((unless (consp returns))
      a.fn-returns-hint-acc)
     ((cons first rest) returns)
     ((decl d) first)
     ((hint-pair h) d.type)
     (hypo (change-hint-pair h
                             :thm (cons h.thm (cons d.name 'nil))))
     (first-hint-pair (generate-fn-hint-pair hypo args 'returns)))
    (generate-fn-returns-hint
         rest
         (change-fhg-single-args
              a
              :fn-returns-hint-acc (cons first-hint-pair
                                         a.fn-returns-hint-acc))))))

Theorem: hint-pair-listp-of-generate-fn-returns-hint

(defthm hint-pair-listp-of-generate-fn-returns-hint
  (b* ((fn-hint-lst (generate-fn-returns-hint returns args)))
    (hint-pair-listp fn-hint-lst))
  :rule-classes :rewrite)

Function: generate-fn-more-returns-hint

(defun generate-fn-more-returns-hint (more-returns args)
 (declare (xargs :guard (and (hint-pair-listp more-returns)
                             (fhg-single-args-p args))))
 (let ((acl2::__function__ 'generate-fn-more-returns-hint))
  (declare (ignorable acl2::__function__))
  (b* ((more-returns (hint-pair-list-fix more-returns))
       (args (fhg-single-args-fix args))
       ((fhg-single-args a) args)
       ((unless (consp more-returns))
        a.fn-more-returns-hint-acc)
       ((cons first rest) more-returns)
       (first-hint-pair
            (generate-fn-hint-pair first args 'more-returns)))
   (generate-fn-more-returns-hint
      rest
      (change-fhg-single-args a
                              :fn-more-returns-hint-acc
                              (cons first-hint-pair
                                    a.fn-more-returns-hint-acc))))))

Theorem: hint-pair-listp-of-generate-fn-more-returns-hint

(defthm hint-pair-listp-of-generate-fn-more-returns-hint
  (b*
   ((fn-hint-lst (generate-fn-more-returns-hint more-returns args)))
   (hint-pair-listp fn-hint-lst))
  :rule-classes :rewrite)

Function: generate-fn-hint

(defun generate-fn-hint (args)
 (declare (xargs :guard (fhg-single-args-p args)))
 (let ((acl2::__function__ 'generate-fn-hint))
  (declare (ignorable acl2::__function__))
  (b* ((args (fhg-single-args-fix args))
       ((fhg-single-args a) args)
       ((func f) a.fn))
    (change-fhg-single-args
         a
         :fn-returns-hint-acc (generate-fn-returns-hint f.returns a)
         :fn-more-returns-hint-acc
         (generate-fn-more-returns-hint f.more-returns a)))))

Theorem: fhg-single-args-p-of-generate-fn-hint

(defthm fhg-single-args-p-of-generate-fn-hint
  (b* ((fn-hint-lst (generate-fn-hint args)))
    (fhg-single-args-p fn-hint-lst))
  :rule-classes :rewrite)

Function: fhg-args-p

(defun fhg-args-p (x)
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'fhg-args-p))
  (declare (ignorable acl2::__function__))
  (and
   (mbe
       :logic
       (and (alistp x)
            (equal (strip-cars x)
                   '(term-lst fn-lst fn-returns-hint-acc
                              fn-more-returns-hint-acc lambda-acc)))
       :exec (fty::alist-with-carsp
                  x
                  '(term-lst fn-lst fn-returns-hint-acc
                             fn-more-returns-hint-acc lambda-acc)))
   (b* ((term-lst (cdr (std::da-nth 0 x)))
        (fn-lst (cdr (std::da-nth 1 x)))
        (fn-returns-hint-acc (cdr (std::da-nth 2 x)))
        (fn-more-returns-hint-acc (cdr (std::da-nth 3 x)))
        (lambda-acc (cdr (std::da-nth 4 x))))
     (and (pseudo-term-listp term-lst)
          (func-alistp fn-lst)
          (hint-pair-listp fn-returns-hint-acc)
          (hint-pair-listp fn-more-returns-hint-acc)
          (lambda-binding-listp lambda-acc))))))

Theorem: consp-when-fhg-args-p

(defthm consp-when-fhg-args-p
  (implies (fhg-args-p x) (consp x))
  :rule-classes :compound-recognizer)

Function: fhg-args-fix$inline

(defun fhg-args-fix$inline (x)
 (declare (xargs :guard (fhg-args-p x)))
 (let ((acl2::__function__ 'fhg-args-fix))
  (declare (ignorable acl2::__function__))
  (mbe
   :logic
   (b*
    ((term-lst (pseudo-term-list-fix (cdr (std::da-nth 0 x))))
     (fn-lst (func-alist-fix (cdr (std::da-nth 1 x))))
     (fn-returns-hint-acc
          (hint-pair-list-fix (cdr (std::da-nth 2 x))))
     (fn-more-returns-hint-acc
          (hint-pair-list-fix (cdr (std::da-nth 3 x))))
     (lambda-acc (lambda-binding-list-fix (cdr (std::da-nth 4 x)))))
    (list (cons 'term-lst term-lst)
          (cons 'fn-lst fn-lst)
          (cons 'fn-returns-hint-acc
                fn-returns-hint-acc)
          (cons 'fn-more-returns-hint-acc
                fn-more-returns-hint-acc)
          (cons 'lambda-acc lambda-acc)))
   :exec x)))

Theorem: fhg-args-p-of-fhg-args-fix

(defthm fhg-args-p-of-fhg-args-fix
  (b* ((new-x (fhg-args-fix$inline x)))
    (fhg-args-p new-x))
  :rule-classes :rewrite)

Theorem: fhg-args-fix-when-fhg-args-p

(defthm fhg-args-fix-when-fhg-args-p
  (implies (fhg-args-p x)
           (equal (fhg-args-fix x) x)))

Function: fhg-args-equiv$inline

(defun fhg-args-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (fhg-args-p acl2::x)
                              (fhg-args-p acl2::y))))
  (equal (fhg-args-fix acl2::x)
         (fhg-args-fix acl2::y)))

Theorem: fhg-args-equiv-is-an-equivalence

(defthm fhg-args-equiv-is-an-equivalence
  (and (booleanp (fhg-args-equiv x y))
       (fhg-args-equiv x x)
       (implies (fhg-args-equiv x y)
                (fhg-args-equiv y x))
       (implies (and (fhg-args-equiv x y)
                     (fhg-args-equiv y z))
                (fhg-args-equiv x z)))
  :rule-classes (:equivalence))

Theorem: fhg-args-equiv-implies-equal-fhg-args-fix-1

(defthm fhg-args-equiv-implies-equal-fhg-args-fix-1
  (implies (fhg-args-equiv acl2::x x-equiv)
           (equal (fhg-args-fix acl2::x)
                  (fhg-args-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: fhg-args-fix-under-fhg-args-equiv

(defthm fhg-args-fix-under-fhg-args-equiv
  (fhg-args-equiv (fhg-args-fix acl2::x)
                  acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-fhg-args-fix-1-forward-to-fhg-args-equiv

(defthm equal-of-fhg-args-fix-1-forward-to-fhg-args-equiv
  (implies (equal (fhg-args-fix acl2::x) acl2::y)
           (fhg-args-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: equal-of-fhg-args-fix-2-forward-to-fhg-args-equiv

(defthm equal-of-fhg-args-fix-2-forward-to-fhg-args-equiv
  (implies (equal acl2::x (fhg-args-fix acl2::y))
           (fhg-args-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: fhg-args-equiv-of-fhg-args-fix-1-forward

(defthm fhg-args-equiv-of-fhg-args-fix-1-forward
  (implies (fhg-args-equiv (fhg-args-fix acl2::x)
                           acl2::y)
           (fhg-args-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: fhg-args-equiv-of-fhg-args-fix-2-forward

(defthm fhg-args-equiv-of-fhg-args-fix-2-forward
  (implies (fhg-args-equiv acl2::x (fhg-args-fix acl2::y))
           (fhg-args-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Function: fhg-args->term-lst$inline

(defun fhg-args->term-lst$inline (x)
  (declare (xargs :guard (fhg-args-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'fhg-args->term-lst))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (pseudo-term-list-fix (cdr (std::da-nth 0 x))))
         :exec (cdr (std::da-nth 0 x)))))

Theorem: pseudo-term-listp-of-fhg-args->term-lst

(defthm pseudo-term-listp-of-fhg-args->term-lst
  (b* ((term-lst (fhg-args->term-lst$inline x)))
    (pseudo-term-listp term-lst))
  :rule-classes :rewrite)

Theorem: fhg-args->term-lst$inline-of-fhg-args-fix-x

(defthm fhg-args->term-lst$inline-of-fhg-args-fix-x
  (equal (fhg-args->term-lst$inline (fhg-args-fix x))
         (fhg-args->term-lst$inline x)))

Theorem: fhg-args->term-lst$inline-fhg-args-equiv-congruence-on-x

(defthm fhg-args->term-lst$inline-fhg-args-equiv-congruence-on-x
  (implies (fhg-args-equiv x x-equiv)
           (equal (fhg-args->term-lst$inline x)
                  (fhg-args->term-lst$inline x-equiv)))
  :rule-classes :congruence)

Function: fhg-args->fn-lst$inline

(defun fhg-args->fn-lst$inline (x)
  (declare (xargs :guard (fhg-args-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'fhg-args->fn-lst))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (func-alist-fix (cdr (std::da-nth 1 x))))
         :exec (cdr (std::da-nth 1 x)))))

Theorem: func-alistp-of-fhg-args->fn-lst

(defthm func-alistp-of-fhg-args->fn-lst
  (b* ((fn-lst (fhg-args->fn-lst$inline x)))
    (func-alistp fn-lst))
  :rule-classes :rewrite)

Theorem: fhg-args->fn-lst$inline-of-fhg-args-fix-x

(defthm fhg-args->fn-lst$inline-of-fhg-args-fix-x
  (equal (fhg-args->fn-lst$inline (fhg-args-fix x))
         (fhg-args->fn-lst$inline x)))

Theorem: fhg-args->fn-lst$inline-fhg-args-equiv-congruence-on-x

(defthm fhg-args->fn-lst$inline-fhg-args-equiv-congruence-on-x
  (implies (fhg-args-equiv x x-equiv)
           (equal (fhg-args->fn-lst$inline x)
                  (fhg-args->fn-lst$inline x-equiv)))
  :rule-classes :congruence)

Function: fhg-args->fn-returns-hint-acc$inline

(defun fhg-args->fn-returns-hint-acc$inline (x)
  (declare (xargs :guard (fhg-args-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'fhg-args->fn-returns-hint-acc))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (hint-pair-list-fix (cdr (std::da-nth 2 x))))
         :exec (cdr (std::da-nth 2 x)))))

Theorem: hint-pair-listp-of-fhg-args->fn-returns-hint-acc

(defthm hint-pair-listp-of-fhg-args->fn-returns-hint-acc
  (b*
    ((fn-returns-hint-acc (fhg-args->fn-returns-hint-acc$inline x)))
    (hint-pair-listp fn-returns-hint-acc))
  :rule-classes :rewrite)

Theorem: fhg-args->fn-returns-hint-acc$inline-of-fhg-args-fix-x

(defthm fhg-args->fn-returns-hint-acc$inline-of-fhg-args-fix-x
  (equal (fhg-args->fn-returns-hint-acc$inline (fhg-args-fix x))
         (fhg-args->fn-returns-hint-acc$inline x)))

Theorem: fhg-args->fn-returns-hint-acc$inline-fhg-args-equiv-congruence-on-x

(defthm
 fhg-args->fn-returns-hint-acc$inline-fhg-args-equiv-congruence-on-x
 (implies (fhg-args-equiv x x-equiv)
          (equal (fhg-args->fn-returns-hint-acc$inline x)
                 (fhg-args->fn-returns-hint-acc$inline x-equiv)))
 :rule-classes :congruence)

Function: fhg-args->fn-more-returns-hint-acc$inline

(defun fhg-args->fn-more-returns-hint-acc$inline (x)
  (declare (xargs :guard (fhg-args-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'fhg-args->fn-more-returns-hint-acc))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (hint-pair-list-fix (cdr (std::da-nth 3 x))))
         :exec (cdr (std::da-nth 3 x)))))

Theorem: hint-pair-listp-of-fhg-args->fn-more-returns-hint-acc

(defthm hint-pair-listp-of-fhg-args->fn-more-returns-hint-acc
  (b* ((fn-more-returns-hint-acc
            (fhg-args->fn-more-returns-hint-acc$inline x)))
    (hint-pair-listp fn-more-returns-hint-acc))
  :rule-classes :rewrite)

Theorem: fhg-args->fn-more-returns-hint-acc$inline-of-fhg-args-fix-x

(defthm fhg-args->fn-more-returns-hint-acc$inline-of-fhg-args-fix-x
 (equal (fhg-args->fn-more-returns-hint-acc$inline (fhg-args-fix x))
        (fhg-args->fn-more-returns-hint-acc$inline x)))

Theorem: fhg-args->fn-more-returns-hint-acc$inline-fhg-args-equiv-congruence-on-x

(defthm
 fhg-args->fn-more-returns-hint-acc$inline-fhg-args-equiv-congruence-on-x
 (implies
      (fhg-args-equiv x x-equiv)
      (equal (fhg-args->fn-more-returns-hint-acc$inline x)
             (fhg-args->fn-more-returns-hint-acc$inline x-equiv)))
 :rule-classes :congruence)

Function: fhg-args->lambda-acc$inline

(defun fhg-args->lambda-acc$inline (x)
  (declare (xargs :guard (fhg-args-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'fhg-args->lambda-acc))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (lambda-binding-list-fix (cdr (std::da-nth 4 x))))
         :exec (cdr (std::da-nth 4 x)))))

Theorem: lambda-binding-listp-of-fhg-args->lambda-acc

(defthm lambda-binding-listp-of-fhg-args->lambda-acc
  (b* ((lambda-acc (fhg-args->lambda-acc$inline x)))
    (lambda-binding-listp lambda-acc))
  :rule-classes :rewrite)

Theorem: fhg-args->lambda-acc$inline-of-fhg-args-fix-x

(defthm fhg-args->lambda-acc$inline-of-fhg-args-fix-x
  (equal (fhg-args->lambda-acc$inline (fhg-args-fix x))
         (fhg-args->lambda-acc$inline x)))

Theorem: fhg-args->lambda-acc$inline-fhg-args-equiv-congruence-on-x

(defthm fhg-args->lambda-acc$inline-fhg-args-equiv-congruence-on-x
  (implies (fhg-args-equiv x x-equiv)
           (equal (fhg-args->lambda-acc$inline x)
                  (fhg-args->lambda-acc$inline x-equiv)))
  :rule-classes :congruence)

Function: fhg-args

(defun fhg-args (term-lst fn-lst fn-returns-hint-acc
                          fn-more-returns-hint-acc lambda-acc)
 (declare
      (xargs :guard (and (pseudo-term-listp term-lst)
                         (func-alistp fn-lst)
                         (hint-pair-listp fn-returns-hint-acc)
                         (hint-pair-listp fn-more-returns-hint-acc)
                         (lambda-binding-listp lambda-acc))))
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'fhg-args))
   (declare (ignorable acl2::__function__))
   (b*
     ((term-lst (mbe :logic (pseudo-term-list-fix term-lst)
                     :exec term-lst))
      (fn-lst (mbe :logic (func-alist-fix fn-lst)
                   :exec fn-lst))
      (fn-returns-hint-acc
           (mbe :logic (hint-pair-list-fix fn-returns-hint-acc)
                :exec fn-returns-hint-acc))
      (fn-more-returns-hint-acc
           (mbe :logic (hint-pair-list-fix fn-more-returns-hint-acc)
                :exec fn-more-returns-hint-acc))
      (lambda-acc (mbe :logic (lambda-binding-list-fix lambda-acc)
                       :exec lambda-acc)))
     (list (cons 'term-lst term-lst)
           (cons 'fn-lst fn-lst)
           (cons 'fn-returns-hint-acc
                 fn-returns-hint-acc)
           (cons 'fn-more-returns-hint-acc
                 fn-more-returns-hint-acc)
           (cons 'lambda-acc lambda-acc)))))

Theorem: fhg-args-p-of-fhg-args

(defthm fhg-args-p-of-fhg-args
  (b* ((x (fhg-args term-lst fn-lst fn-returns-hint-acc
                    fn-more-returns-hint-acc lambda-acc)))
    (fhg-args-p x))
  :rule-classes :rewrite)

Theorem: fhg-args->term-lst-of-fhg-args

(defthm fhg-args->term-lst-of-fhg-args
  (equal (fhg-args->term-lst
              (fhg-args term-lst fn-lst fn-returns-hint-acc
                        fn-more-returns-hint-acc lambda-acc))
         (pseudo-term-list-fix term-lst)))

Theorem: fhg-args->fn-lst-of-fhg-args

(defthm fhg-args->fn-lst-of-fhg-args
 (equal
   (fhg-args->fn-lst (fhg-args term-lst fn-lst fn-returns-hint-acc
                               fn-more-returns-hint-acc lambda-acc))
   (func-alist-fix fn-lst)))

Theorem: fhg-args->fn-returns-hint-acc-of-fhg-args

(defthm fhg-args->fn-returns-hint-acc-of-fhg-args
  (equal (fhg-args->fn-returns-hint-acc
              (fhg-args term-lst fn-lst fn-returns-hint-acc
                        fn-more-returns-hint-acc lambda-acc))
         (hint-pair-list-fix fn-returns-hint-acc)))

Theorem: fhg-args->fn-more-returns-hint-acc-of-fhg-args

(defthm fhg-args->fn-more-returns-hint-acc-of-fhg-args
  (equal (fhg-args->fn-more-returns-hint-acc
              (fhg-args term-lst fn-lst fn-returns-hint-acc
                        fn-more-returns-hint-acc lambda-acc))
         (hint-pair-list-fix fn-more-returns-hint-acc)))

Theorem: fhg-args->lambda-acc-of-fhg-args

(defthm fhg-args->lambda-acc-of-fhg-args
  (equal (fhg-args->lambda-acc
              (fhg-args term-lst fn-lst fn-returns-hint-acc
                        fn-more-returns-hint-acc lambda-acc))
         (lambda-binding-list-fix lambda-acc)))

Theorem: fhg-args-of-fields

(defthm fhg-args-of-fields
  (equal (fhg-args (fhg-args->term-lst x)
                   (fhg-args->fn-lst x)
                   (fhg-args->fn-returns-hint-acc x)
                   (fhg-args->fn-more-returns-hint-acc x)
                   (fhg-args->lambda-acc x))
         (fhg-args-fix x)))

Theorem: fhg-args-fix-when-fhg-args

(defthm fhg-args-fix-when-fhg-args
  (equal (fhg-args-fix x)
         (fhg-args (fhg-args->term-lst x)
                   (fhg-args->fn-lst x)
                   (fhg-args->fn-returns-hint-acc x)
                   (fhg-args->fn-more-returns-hint-acc x)
                   (fhg-args->lambda-acc x))))

Theorem: equal-of-fhg-args

(defthm equal-of-fhg-args
  (equal (equal (fhg-args term-lst fn-lst fn-returns-hint-acc
                          fn-more-returns-hint-acc lambda-acc)
                x)
         (and (fhg-args-p x)
              (equal (fhg-args->term-lst x)
                     (pseudo-term-list-fix term-lst))
              (equal (fhg-args->fn-lst x)
                     (func-alist-fix fn-lst))
              (equal (fhg-args->fn-returns-hint-acc x)
                     (hint-pair-list-fix fn-returns-hint-acc))
              (equal (fhg-args->fn-more-returns-hint-acc x)
                     (hint-pair-list-fix fn-more-returns-hint-acc))
              (equal (fhg-args->lambda-acc x)
                     (lambda-binding-list-fix lambda-acc)))))

Theorem: fhg-args-of-pseudo-term-list-fix-term-lst

(defthm fhg-args-of-pseudo-term-list-fix-term-lst
  (equal (fhg-args (pseudo-term-list-fix term-lst)
                   fn-lst fn-returns-hint-acc
                   fn-more-returns-hint-acc lambda-acc)
         (fhg-args term-lst fn-lst fn-returns-hint-acc
                   fn-more-returns-hint-acc lambda-acc)))

Theorem: fhg-args-pseudo-term-list-equiv-congruence-on-term-lst

(defthm fhg-args-pseudo-term-list-equiv-congruence-on-term-lst
  (implies (pseudo-term-list-equiv term-lst term-lst-equiv)
           (equal (fhg-args term-lst fn-lst fn-returns-hint-acc
                            fn-more-returns-hint-acc lambda-acc)
                  (fhg-args term-lst-equiv
                            fn-lst fn-returns-hint-acc
                            fn-more-returns-hint-acc lambda-acc)))
  :rule-classes :congruence)

Theorem: fhg-args-of-func-alist-fix-fn-lst

(defthm fhg-args-of-func-alist-fix-fn-lst
  (equal (fhg-args term-lst (func-alist-fix fn-lst)
                   fn-returns-hint-acc
                   fn-more-returns-hint-acc lambda-acc)
         (fhg-args term-lst fn-lst fn-returns-hint-acc
                   fn-more-returns-hint-acc lambda-acc)))

Theorem: fhg-args-func-alist-equiv-congruence-on-fn-lst

(defthm fhg-args-func-alist-equiv-congruence-on-fn-lst
  (implies (func-alist-equiv fn-lst fn-lst-equiv)
           (equal (fhg-args term-lst fn-lst fn-returns-hint-acc
                            fn-more-returns-hint-acc lambda-acc)
                  (fhg-args term-lst
                            fn-lst-equiv fn-returns-hint-acc
                            fn-more-returns-hint-acc lambda-acc)))
  :rule-classes :congruence)

Theorem: fhg-args-of-hint-pair-list-fix-fn-returns-hint-acc

(defthm fhg-args-of-hint-pair-list-fix-fn-returns-hint-acc
  (equal (fhg-args term-lst fn-lst
                   (hint-pair-list-fix fn-returns-hint-acc)
                   fn-more-returns-hint-acc lambda-acc)
         (fhg-args term-lst fn-lst fn-returns-hint-acc
                   fn-more-returns-hint-acc lambda-acc)))

Theorem: fhg-args-hint-pair-list-equiv-congruence-on-fn-returns-hint-acc

(defthm
    fhg-args-hint-pair-list-equiv-congruence-on-fn-returns-hint-acc
  (implies (hint-pair-list-equiv fn-returns-hint-acc
                                 fn-returns-hint-acc-equiv)
           (equal (fhg-args term-lst fn-lst fn-returns-hint-acc
                            fn-more-returns-hint-acc lambda-acc)
                  (fhg-args term-lst
                            fn-lst fn-returns-hint-acc-equiv
                            fn-more-returns-hint-acc lambda-acc)))
  :rule-classes :congruence)

Theorem: fhg-args-of-hint-pair-list-fix-fn-more-returns-hint-acc

(defthm fhg-args-of-hint-pair-list-fix-fn-more-returns-hint-acc
  (equal (fhg-args term-lst fn-lst fn-returns-hint-acc
                   (hint-pair-list-fix fn-more-returns-hint-acc)
                   lambda-acc)
         (fhg-args term-lst fn-lst fn-returns-hint-acc
                   fn-more-returns-hint-acc lambda-acc)))

Theorem: fhg-args-hint-pair-list-equiv-congruence-on-fn-more-returns-hint-acc

(defthm
 fhg-args-hint-pair-list-equiv-congruence-on-fn-more-returns-hint-acc
 (implies (hint-pair-list-equiv fn-more-returns-hint-acc
                                fn-more-returns-hint-acc-equiv)
          (equal (fhg-args term-lst fn-lst fn-returns-hint-acc
                           fn-more-returns-hint-acc lambda-acc)
                 (fhg-args term-lst fn-lst fn-returns-hint-acc
                           fn-more-returns-hint-acc-equiv
                           lambda-acc)))
 :rule-classes :congruence)

Theorem: fhg-args-of-lambda-binding-list-fix-lambda-acc

(defthm fhg-args-of-lambda-binding-list-fix-lambda-acc
  (equal (fhg-args term-lst fn-lst fn-returns-hint-acc
                   fn-more-returns-hint-acc
                   (lambda-binding-list-fix lambda-acc))
         (fhg-args term-lst fn-lst fn-returns-hint-acc
                   fn-more-returns-hint-acc lambda-acc)))

Theorem: fhg-args-lambda-binding-list-equiv-congruence-on-lambda-acc

(defthm fhg-args-lambda-binding-list-equiv-congruence-on-lambda-acc
  (implies (lambda-binding-list-equiv lambda-acc lambda-acc-equiv)
           (equal (fhg-args term-lst fn-lst fn-returns-hint-acc
                            fn-more-returns-hint-acc lambda-acc)
                  (fhg-args term-lst fn-lst fn-returns-hint-acc
                            fn-more-returns-hint-acc
                            lambda-acc-equiv)))
  :rule-classes :congruence)

Theorem: fhg-args-fix-redef

(defthm fhg-args-fix-redef
  (equal (fhg-args-fix x)
         (fhg-args (fhg-args->term-lst x)
                   (fhg-args->fn-lst x)
                   (fhg-args->fn-returns-hint-acc x)
                   (fhg-args->fn-more-returns-hint-acc x)
                   (fhg-args->lambda-acc x)))
  :rule-classes :definition)

Theorem: not-symbolp-then-consp-of-car-of-fhg-args->term-lst

(defthm not-symbolp-then-consp-of-car-of-fhg-args->term-lst
  (implies (and (fhg-args-p args)
                (consp (fhg-args->term-lst args))
                (not (symbolp (car (fhg-args->term-lst args)))))
           (consp (car (fhg-args->term-lst args)))))

Theorem: pseudo-term-listp-of-cdr-of-fhg-args->term-lst

(defthm pseudo-term-listp-of-cdr-of-fhg-args->term-lst
  (implies (and (fhg-args-p args)
                (consp (fhg-args->term-lst args)))
           (pseudo-term-listp (cdr (fhg-args->term-lst args)))))

Theorem: pseudo-term-listp-of-cdar-of-fhg-args->term-lst

(defthm pseudo-term-listp-of-cdar-of-fhg-args->term-lst
  (implies
       (and (fhg-args-p args)
            (consp (fhg-args->term-lst args))
            (not (symbolp (car (fhg-args->term-lst args))))
            (not (equal (car (car (fhg-args->term-lst args)))
                        'quote)))
       (pseudo-term-listp (cdr (car (fhg-args->term-lst args))))))

Theorem: symbolp-of-caar-of-fhg-args->term-lst

(defthm symbolp-of-caar-of-fhg-args->term-lst
 (implies
  (and (fhg-args-p args)
       (consp (fhg-args->term-lst args))
       (not (symbolp (car (fhg-args->term-lst args))))
       (not (pseudo-lambdap (car (car (fhg-args->term-lst args))))))
  (symbolp (car (car (fhg-args->term-lst args))))))

Theorem: len-equal-of-formals-of-pseudo-lambdap-and-actuals

(defthm len-equal-of-formals-of-pseudo-lambdap-and-actuals
  (implies
       (and (fhg-args-p args)
            (consp (fhg-args->term-lst args))
            (pseudo-lambdap (car (car (fhg-args->term-lst args)))))
       (equal (len (cadr (car (car (fhg-args->term-lst args)))))
              (len (cdr (car (fhg-args->term-lst args)))))))

Theorem: lemma-8

(defthm lemma-8
 (implies
     (and (fhg-args-p args)
          (consp (fhg-args->term-lst args))
          (assoc-equal (car (car (fhg-args->term-lst args)))
                       (fhg-args->fn-lst args)))
     (func-p (cdr (assoc-equal (car (car (fhg-args->term-lst args)))
                               (fhg-args->fn-lst args))))))

Theorem: lemma-10

(defthm lemma-10
  (implies (and (fhg-args-p args)
                (consp (fhg-args->term-lst args))
                (assoc-equal (car (car (fhg-args->term-lst args)))
                             (fhg-args->fn-lst args)))
           (consp (assoc-equal (car (car (fhg-args->term-lst args)))
                               (fhg-args->fn-lst args)))))

Function: generate-fn-hint-lst

(defun generate-fn-hint-lst (args)
 (declare (xargs :guard (fhg-args-p args)))
 (let ((acl2::__function__ 'generate-fn-hint-lst))
  (declare (ignorable acl2::__function__))
  (b*
   ((args (fhg-args-fix args))
    ((fhg-args a) args)
    ((unless (consp a.term-lst)) a)
    ((cons term rest) a.term-lst)
    ((if (symbolp term))
     (generate-fn-hint-lst (change-fhg-args a :term-lst rest)))
    ((if (equal (car term) 'quote))
     (generate-fn-hint-lst (change-fhg-args a :term-lst rest)))
    ((cons fn-call fn-actuals) term)
    ((if (pseudo-lambdap fn-call))
     (b*
       ((lambda-formals (lambda-formals fn-call))
        (lambda-body (lambda-body fn-call))
        (lambda-actuals fn-actuals)
        (lambda-bd (make-lambda-binding :formals lambda-formals
                                        :actuals lambda-actuals))
        ((unless (mbt (lambda-binding-p lambda-bd)))
         a)
        (a-1 (generate-fn-hint-lst
                  (change-fhg-args
                       a
                       :term-lst (list lambda-body)
                       :lambda-acc (cons lambda-bd a.lambda-acc))))
        (a-2 (generate-fn-hint-lst
                  (change-fhg-args a-1
                                   :term-lst lambda-actuals))))
       (generate-fn-hint-lst (change-fhg-args a-2 :term-lst rest))))
    ((unless (mbt (symbolp fn-call))) a)
    (fn (assoc-equal fn-call a.fn-lst))
    ((unless fn)
     (b* ((a-1 (generate-fn-hint-lst
                    (change-fhg-args a
                                     :term-lst fn-actuals))))
       (generate-fn-hint-lst (change-fhg-args a-1 :term-lst rest))))
    (f (cdr fn))
    (as-1
      (generate-fn-hint
           (make-fhg-single-args
                :fn f
                :actuals fn-actuals
                :fn-returns-hint-acc a.fn-returns-hint-acc
                :fn-more-returns-hint-acc a.fn-more-returns-hint-acc
                :lambda-acc a.lambda-acc)))
    ((fhg-single-args as-1) as-1)
    (a-1
      (change-fhg-args
           a
           :fn-returns-hint-acc as-1.fn-returns-hint-acc
           :fn-more-returns-hint-acc as-1.fn-more-returns-hint-acc))
    (a-2
     (generate-fn-hint-lst (change-fhg-args a-1
                                            :term-lst fn-actuals))))
   (generate-fn-hint-lst (change-fhg-args a-2 :term-lst rest)))))

Theorem: fhg-args-p-of-generate-fn-hint-lst

(defthm fhg-args-p-of-generate-fn-hint-lst
  (b* ((fn-hint-lst (generate-fn-hint-lst args)))
    (fhg-args-p fn-hint-lst))
  :rule-classes :rewrite)

Function: uninterpreted-p

(defun uninterpreted-p (x)
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'uninterpreted-p))
  (declare (ignorable acl2::__function__))
  (and (mbe :logic (and (alistp x)
                        (equal (strip-cars x)
                               '(returns more-returns)))
            :exec (fty::alist-with-carsp x '(returns more-returns)))
       (b* ((returns (cdr (std::da-nth 0 x)))
            (more-returns (cdr (std::da-nth 1 x))))
         (and (hint-pair-listp returns)
              (hint-pair-listp more-returns))))))

Theorem: consp-when-uninterpreted-p

(defthm consp-when-uninterpreted-p
  (implies (uninterpreted-p x) (consp x))
  :rule-classes :compound-recognizer)

Function: uninterpreted-fix$inline

(defun uninterpreted-fix$inline (x)
 (declare (xargs :guard (uninterpreted-p x)))
 (let ((acl2::__function__ 'uninterpreted-fix))
  (declare (ignorable acl2::__function__))
  (mbe
   :logic
   (b* ((returns (hint-pair-list-fix (cdr (std::da-nth 0 x))))
        (more-returns (hint-pair-list-fix (cdr (std::da-nth 1 x)))))
     (list (cons 'returns returns)
           (cons 'more-returns more-returns)))
   :exec x)))

Theorem: uninterpreted-p-of-uninterpreted-fix

(defthm uninterpreted-p-of-uninterpreted-fix
  (b* ((new-x (uninterpreted-fix$inline x)))
    (uninterpreted-p new-x))
  :rule-classes :rewrite)

Theorem: uninterpreted-fix-when-uninterpreted-p

(defthm uninterpreted-fix-when-uninterpreted-p
  (implies (uninterpreted-p x)
           (equal (uninterpreted-fix x) x)))

Function: uninterpreted-equiv$inline

(defun uninterpreted-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (uninterpreted-p acl2::x)
                              (uninterpreted-p acl2::y))))
  (equal (uninterpreted-fix acl2::x)
         (uninterpreted-fix acl2::y)))

Theorem: uninterpreted-equiv-is-an-equivalence

(defthm uninterpreted-equiv-is-an-equivalence
  (and (booleanp (uninterpreted-equiv x y))
       (uninterpreted-equiv x x)
       (implies (uninterpreted-equiv x y)
                (uninterpreted-equiv y x))
       (implies (and (uninterpreted-equiv x y)
                     (uninterpreted-equiv y z))
                (uninterpreted-equiv x z)))
  :rule-classes (:equivalence))

Theorem: uninterpreted-equiv-implies-equal-uninterpreted-fix-1

(defthm uninterpreted-equiv-implies-equal-uninterpreted-fix-1
  (implies (uninterpreted-equiv acl2::x x-equiv)
           (equal (uninterpreted-fix acl2::x)
                  (uninterpreted-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: uninterpreted-fix-under-uninterpreted-equiv

(defthm uninterpreted-fix-under-uninterpreted-equiv
  (uninterpreted-equiv (uninterpreted-fix acl2::x)
                       acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-uninterpreted-fix-1-forward-to-uninterpreted-equiv

(defthm equal-of-uninterpreted-fix-1-forward-to-uninterpreted-equiv
  (implies (equal (uninterpreted-fix acl2::x)
                  acl2::y)
           (uninterpreted-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: equal-of-uninterpreted-fix-2-forward-to-uninterpreted-equiv

(defthm equal-of-uninterpreted-fix-2-forward-to-uninterpreted-equiv
  (implies (equal acl2::x (uninterpreted-fix acl2::y))
           (uninterpreted-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: uninterpreted-equiv-of-uninterpreted-fix-1-forward

(defthm uninterpreted-equiv-of-uninterpreted-fix-1-forward
  (implies (uninterpreted-equiv (uninterpreted-fix acl2::x)
                                acl2::y)
           (uninterpreted-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: uninterpreted-equiv-of-uninterpreted-fix-2-forward

(defthm uninterpreted-equiv-of-uninterpreted-fix-2-forward
  (implies (uninterpreted-equiv acl2::x (uninterpreted-fix acl2::y))
           (uninterpreted-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Function: uninterpreted->returns$inline

(defun uninterpreted->returns$inline (x)
  (declare (xargs :guard (uninterpreted-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'uninterpreted->returns))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (hint-pair-list-fix (cdr (std::da-nth 0 x))))
         :exec (cdr (std::da-nth 0 x)))))

Theorem: hint-pair-listp-of-uninterpreted->returns

(defthm hint-pair-listp-of-uninterpreted->returns
  (b* ((returns (uninterpreted->returns$inline x)))
    (hint-pair-listp returns))
  :rule-classes :rewrite)

Theorem: uninterpreted->returns$inline-of-uninterpreted-fix-x

(defthm uninterpreted->returns$inline-of-uninterpreted-fix-x
  (equal (uninterpreted->returns$inline (uninterpreted-fix x))
         (uninterpreted->returns$inline x)))

Theorem: uninterpreted->returns$inline-uninterpreted-equiv-congruence-on-x

(defthm
  uninterpreted->returns$inline-uninterpreted-equiv-congruence-on-x
  (implies (uninterpreted-equiv x x-equiv)
           (equal (uninterpreted->returns$inline x)
                  (uninterpreted->returns$inline x-equiv)))
  :rule-classes :congruence)

Function: uninterpreted->more-returns$inline

(defun uninterpreted->more-returns$inline (x)
  (declare (xargs :guard (uninterpreted-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'uninterpreted->more-returns))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (hint-pair-list-fix (cdr (std::da-nth 1 x))))
         :exec (cdr (std::da-nth 1 x)))))

Theorem: hint-pair-listp-of-uninterpreted->more-returns

(defthm hint-pair-listp-of-uninterpreted->more-returns
  (b* ((more-returns (uninterpreted->more-returns$inline x)))
    (hint-pair-listp more-returns))
  :rule-classes :rewrite)

Theorem: uninterpreted->more-returns$inline-of-uninterpreted-fix-x

(defthm uninterpreted->more-returns$inline-of-uninterpreted-fix-x
  (equal (uninterpreted->more-returns$inline (uninterpreted-fix x))
         (uninterpreted->more-returns$inline x)))

Theorem: uninterpreted->more-returns$inline-uninterpreted-equiv-congruence-on-x

(defthm
 uninterpreted->more-returns$inline-uninterpreted-equiv-congruence-on-x
 (implies (uninterpreted-equiv x x-equiv)
          (equal (uninterpreted->more-returns$inline x)
                 (uninterpreted->more-returns$inline x-equiv)))
 :rule-classes :congruence)

Function: uninterpreted

(defun uninterpreted (returns more-returns)
  (declare (xargs :guard (and (hint-pair-listp returns)
                              (hint-pair-listp more-returns))))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'uninterpreted))
    (declare (ignorable acl2::__function__))
    (b* ((returns (mbe :logic (hint-pair-list-fix returns)
                       :exec returns))
         (more-returns (mbe :logic (hint-pair-list-fix more-returns)
                            :exec more-returns)))
      (list (cons 'returns returns)
            (cons 'more-returns more-returns)))))

Theorem: uninterpreted-p-of-uninterpreted

(defthm uninterpreted-p-of-uninterpreted
  (b* ((x (uninterpreted returns more-returns)))
    (uninterpreted-p x))
  :rule-classes :rewrite)

Theorem: uninterpreted->returns-of-uninterpreted

(defthm uninterpreted->returns-of-uninterpreted
  (equal
       (uninterpreted->returns (uninterpreted returns more-returns))
       (hint-pair-list-fix returns)))

Theorem: uninterpreted->more-returns-of-uninterpreted

(defthm uninterpreted->more-returns-of-uninterpreted
 (equal
  (uninterpreted->more-returns (uninterpreted returns more-returns))
  (hint-pair-list-fix more-returns)))

Theorem: uninterpreted-of-fields

(defthm uninterpreted-of-fields
  (equal (uninterpreted (uninterpreted->returns x)
                        (uninterpreted->more-returns x))
         (uninterpreted-fix x)))

Theorem: uninterpreted-fix-when-uninterpreted

(defthm uninterpreted-fix-when-uninterpreted
  (equal (uninterpreted-fix x)
         (uninterpreted (uninterpreted->returns x)
                        (uninterpreted->more-returns x))))

Theorem: equal-of-uninterpreted

(defthm equal-of-uninterpreted
  (equal (equal (uninterpreted returns more-returns)
                x)
         (and (uninterpreted-p x)
              (equal (uninterpreted->returns x)
                     (hint-pair-list-fix returns))
              (equal (uninterpreted->more-returns x)
                     (hint-pair-list-fix more-returns)))))

Theorem: uninterpreted-of-hint-pair-list-fix-returns

(defthm uninterpreted-of-hint-pair-list-fix-returns
  (equal (uninterpreted (hint-pair-list-fix returns)
                        more-returns)
         (uninterpreted returns more-returns)))

Theorem: uninterpreted-hint-pair-list-equiv-congruence-on-returns

(defthm uninterpreted-hint-pair-list-equiv-congruence-on-returns
  (implies (hint-pair-list-equiv returns returns-equiv)
           (equal (uninterpreted returns more-returns)
                  (uninterpreted returns-equiv more-returns)))
  :rule-classes :congruence)

Theorem: uninterpreted-of-hint-pair-list-fix-more-returns

(defthm uninterpreted-of-hint-pair-list-fix-more-returns
  (equal (uninterpreted returns
                        (hint-pair-list-fix more-returns))
         (uninterpreted returns more-returns)))

Theorem: uninterpreted-hint-pair-list-equiv-congruence-on-more-returns

(defthm
      uninterpreted-hint-pair-list-equiv-congruence-on-more-returns
  (implies (hint-pair-list-equiv more-returns more-returns-equiv)
           (equal (uninterpreted returns more-returns)
                  (uninterpreted returns more-returns-equiv)))
  :rule-classes :congruence)

Theorem: uninterpreted-fix-redef

(defthm uninterpreted-fix-redef
  (equal (uninterpreted-fix x)
         (uninterpreted (uninterpreted->returns x)
                        (uninterpreted->more-returns x)))
  :rule-classes :definition)

Function: uninterpreted-fn-helper

(defun uninterpreted-fn-helper (cl smtlink-hint)
  (declare (xargs :guard (and (pseudo-term-listp cl)
                              (smtlink-hint-p smtlink-hint))))
  (let ((acl2::__function__ 'uninterpreted-fn-helper))
    (declare (ignorable acl2::__function__))
    (b* ((cl (pseudo-term-list-fix cl))
         (smtlink-hint (smtlink-hint-fix smtlink-hint))
         ((smtlink-hint h) smtlink-hint)
         (fn-lst (make-alist-fn-lst h.functions))
         (g (disjoin cl))
         (args (generate-fn-hint-lst
                    (make-fhg-args :term-lst (list g)
                                   :fn-lst fn-lst
                                   :fn-returns-hint-acc nil
                                   :fn-more-returns-hint-acc nil
                                   :lambda-acc nil)))
         ((fhg-args a) args)
         (fn-returns-hint-lst a.fn-returns-hint-acc)
         (fn-more-returns-hint-lst a.fn-more-returns-hint-acc))
      (make-uninterpreted :returns fn-returns-hint-lst
                          :more-returns fn-more-returns-hint-lst))))

Theorem: uninterpreted-p-of-uninterpreted-fn-helper

(defthm uninterpreted-p-of-uninterpreted-fn-helper
  (b* ((uninterpreted (uninterpreted-fn-helper cl smtlink-hint)))
    (uninterpreted-p uninterpreted))
  :rule-classes :rewrite)

Function: uninterpreted-subgoals

(defun uninterpreted-subgoals (hint-pair-lst g tag)
 (declare (xargs :guard (and (hint-pair-listp hint-pair-lst)
                             (pseudo-termp g)
                             (symbolp tag))))
 (let ((acl2::__function__ 'uninterpreted-subgoals))
  (declare (ignorable acl2::__function__))
  (b*
   ((hint-pair-lst (hint-pair-list-fix hint-pair-lst))
    (g (pseudo-term-fix g))
    ((unless (or (equal tag :return)
                 (equal tag :more-return)))
     (prog2$ (er hard?
                 'uninterpreted-fn-cp=>uninterpreted-subgoals
                 "Tag not supported: ~q0" tag)
             (mv nil nil)))
    ((unless (consp hint-pair-lst))
     (mv nil nil))
    ((cons first-hinted-h rest-hinted-hs)
     hint-pair-lst)
    (h (hint-pair->thm first-hinted-h))
    (h-hint (hint-pair->hints first-hinted-h))
    (merged-hint-please-in-theory
         (treat-in-theory-hint '(hint-please)
                               h-hint))
    (merged-type-hyp-in-theory
         (treat-in-theory-hint '(type-hyp)
                               merged-hint-please-in-theory))
    (merged-expand (treat-expand-hint '((:free (x) (hide x)))
                                      merged-type-hyp-in-theory))
    (first-h-thm
     (if
      (equal tag :return)
      (cons
         (cons 'hint-please
               (cons (cons 'quote (cons merged-expand 'nil))
                     'nil))
         (cons (cons 'type-hyp
                     (cons (cons 'hide
                                 (cons (cons 'cons (cons h '('nil)))
                                       'nil))
                           (cons (cons 'quote (cons tag 'nil))
                                 'nil)))
               (cons g 'nil)))
      (cons
         (cons 'hint-please
               (cons (cons 'quote
                           (cons merged-hint-please-in-theory 'nil))
                     'nil))
         (cons h (cons g 'nil)))))
    (first-not-h-clause
     (if
      (equal tag :return)
      (cons
         'not
         (cons (cons 'type-hyp
                     (cons (cons 'hide
                                 (cons (cons 'cons (cons h '('nil)))
                                       'nil))
                           (cons (cons 'quote (cons tag 'nil))
                                 'nil)))
               'nil))
      (cons 'not (cons h 'nil))))
    ((mv rest-h-thms rest-not-h-clauses)
     (uninterpreted-subgoals rest-hinted-hs g tag)))
   (mv (cons first-h-thm rest-h-thms)
       (cons first-not-h-clause
             rest-not-h-clauses)))))

Theorem: pseudo-term-list-listp-of-uninterpreted-subgoals.list-of-h-thm

(defthm
     pseudo-term-list-listp-of-uninterpreted-subgoals.list-of-h-thm
  (b* (((mv ?list-of-h-thm ?list-of-not-hs)
        (uninterpreted-subgoals hint-pair-lst g tag)))
    (pseudo-term-list-listp list-of-h-thm))
  :rule-classes :rewrite)

Theorem: pseudo-term-listp-of-uninterpreted-subgoals.list-of-not-hs

(defthm pseudo-term-listp-of-uninterpreted-subgoals.list-of-not-hs
  (b* (((mv ?list-of-h-thm ?list-of-not-hs)
        (uninterpreted-subgoals hint-pair-lst g tag)))
    (pseudo-term-listp list-of-not-hs))
  :rule-classes :rewrite)

Theorem: uninterpreted-subgoals-correctness

(defthm uninterpreted-subgoals-correctness
 (implies
  (and
   (pseudo-termp g)
   (alistp b)
   (hint-pair-listp hint-pair-lst)
   (ev-uninterpreted
     (disjoin (mv-nth 1
                      (uninterpreted-subgoals hint-pair-lst g tag)))
     b)
   (ev-uninterpreted
        (conjoin-clauses
             (mv-nth 0
                     (uninterpreted-subgoals hint-pair-lst g tag)))
        b))
  (ev-uninterpreted g b)))

Function: uninterpreted-fn-cp

(defun uninterpreted-fn-cp (cl smtlink-hint)
 (declare (xargs :guard (pseudo-term-listp cl)))
 (let ((acl2::__function__ 'uninterpreted-fn-cp))
  (declare (ignorable acl2::__function__))
  (b*
   (((unless (pseudo-term-listp cl)) nil)
    ((unless (smtlink-hint-p smtlink-hint))
     (list cl))
    (g (disjoin cl))
    ((smtlink-hint h) smtlink-hint)
    (uninterpreted (uninterpreted-fn-helper cl h))
    (hinted-ts-returns (uninterpreted->returns uninterpreted))
    (hinted-ts-more-returns
         (uninterpreted->more-returns uninterpreted))
    ((mv list-of-returns-t-thm
         list-of-returns-not-ts)
     (uninterpreted-subgoals hinted-ts-returns g :return))
    ((mv list-of-more-returns-t-thm
         list-of-more-returns-not-ts)
     (uninterpreted-subgoals hinted-ts-more-returns g :more-return))
    (list-of-t-thm (append list-of-returns-t-thm
                           list-of-more-returns-t-thm))
    (list-of-not-ts (append list-of-returns-not-ts
                            list-of-more-returns-not-ts))
    (next-cp (if h.custom-p (cdr (assoc-equal 'uninterpreted-custom
                                              *smt-architecture*))
               (cdr (assoc-equal 'uninterpreted
                                 *smt-architecture*))))
    ((if (null next-cp)) (list cl))
    (the-hint
         (cons ':clause-processor
               (cons (cons next-cp
                           (cons 'clause
                                 (cons (cons 'quote (cons h 'nil))
                                       '(state))))
                     'nil)))
    (cl0 (cons (cons 'hint-please
                     (cons (cons 'quote (cons the-hint 'nil))
                           'nil))
               (append list-of-not-ts (cons g 'nil)))))
   (cons cl0 list-of-t-thm))))

Theorem: pseudo-term-list-listp-of-uninterpreted-fn-cp

(defthm pseudo-term-list-listp-of-uninterpreted-fn-cp
  (b* ((subgoal-lst (uninterpreted-fn-cp cl smtlink-hint)))
    (pseudo-term-list-listp subgoal-lst))
  :rule-classes :rewrite)

Theorem: correctness-of-uninterpreted-fn-cp

(defthm correctness-of-uninterpreted-fn-cp
 (implies
   (and (pseudo-term-listp cl)
        (alistp b)
        (ev-uninterpreted
             (conjoin-clauses (uninterpreted-fn-cp cl smtlink-hint))
             b))
   (ev-uninterpreted (disjoin cl) b))
 :rule-classes :clause-processor)

Subtopics

Fhg-single-args
Fhg-args
Lambda-binding
Generate-fn-hint-lst: (generate-fn-hint-lst args) generate auxiliary hypotheses from ~ function expansion