remove-guard-holders

(local (in-theory (disable remove-guard-holders-weak)))

(local (defthm weak-badge-userfn-structure-alistp-implies-consp-cdr-assoc-equal
    (implies (and (weak-badge-userfn-structure-alistp alist)
        (cdr (assoc-equal fn alist)))
      (consp (cdr (assoc-equal fn alist))))))

(local (defthm consp-assoc-equal-forced
    (implies (and (force (alistp l)) (assoc-equal name l))
      (consp (assoc-equal name l)))))

(local (defthm weak-badge-userfn-structure-alistp-implies-consp-cddr-assoc-equal
    (implies (and (weak-badge-userfn-structure-alistp alist)
        (cddr (assoc-equal fn alist)))
      (consp (cddr (assoc-equal fn alist))))))

(local (defthm executable-tamep-1
    (implies (and (apply$-badge-alistp-ilks-t bpf)
        (cdr (hons-assoc-equal fn bpf)))
      (consp (cdr (hons-assoc-equal fn bpf))))))

(local (defthm executable-tamep-2
    (implies (and (apply$-badge-alistp-ilks-t bpf)
        (cddr (hons-assoc-equal fn bpf)))
      (consp (cddr (hons-assoc-equal fn bpf))))))

(local (defthm executable-tamep-3
    (implies (and (apply$-badge-alistp-ilks-t bpf)
        (cdddr (hons-assoc-equal fn bpf)))
      (consp (cdddr (hons-assoc-equal fn bpf))))))

(local (defthm executable-tamep-4
    (implies (and (weak-badge-userfn-structure-alistp alist)
        (caddr (assoc-equal fn alist)))
      (consp (caddr (assoc-equal fn alist))))))

(local (defthm executable-tamep-5
    (implies (and (weak-badge-userfn-structure-alistp alist)
        (cdr (caddr (assoc-equal fn alist))))
      (consp (cdr (caddr (assoc-equal fn alist)))))))

(local (defthm executable-tamep-6
    (implies (and (weak-badge-userfn-structure-alistp alist)
        (cddr (caddr (assoc-equal fn alist))))
      (consp (cddr (caddr (assoc-equal fn alist)))))))

(local (defthm executable-tamep-7-8
    (implies (and (apply$-badge-alistp-ilks-t bpf)
        (cdr (hons-assoc-equal fn bpf)))
      (natp (caddr (hons-assoc-equal fn bpf))))
    :rule-classes :type-prescription))

(local (defthm executable-tamep-8
    (implies (and (apply$-badge-alistp-ilks-t bpf)
        (hons-assoc-equal fn bpf))
      (equal (cddddr (hons-assoc-equal fn bpf)) t))))

(local (defthm executable-tamep-9
    (implies (and (badge-userfn-structure-alistp alist)
        (caddr (assoc-equal fn alist)))
      (natp (cadr (caddr (assoc-equal fn alist)))))
    :rule-classes :type-prescription))

(local (defthm executable-tamep-10
    (implies (and (badge-userfn-structure-alistp alist)
        (not (equal (cdddr (caddr (assoc-equal fn alist))) t)))
      (true-listp (cdddr (caddr (assoc-equal fn alist)))))))

(local (defthm symbol-listp-implies-pseudo-term-listp
    (implies (symbol-listp x) (pseudo-term-listp x))))

(local (make-flag flag-translate-declaration-to-guard-gen
    translate-declaration-to-guard-gen))

(local (defthm-flag-translate-declaration-to-guard-gen (defthm pseudo-termp-translate-declaration-to-guard-gen
      (implies (and (pseudo-termp var) (equal tflg t))
        (pseudo-termp (translate-declaration-to-guard-gen x var tflg wrld)))
      :flag translate-declaration-to-guard-gen)
    (defthm pseudo-term-listp-translate-declaration-to-guard-gen
      (implies (and (pseudo-termp var) (equal tflg t))
        (pseudo-term-listp (translate-declaration-to-guard-gen-lst l var tflg wrld)))
      :flag translate-declaration-to-guard-gen-lst)))

(local (defthm syntactically-plausible-lambda-objectp-termination-lemma-1
    (< (acl2-count (mv-nth 5
          (syntactically-plausible-lambda-objectp1 edcls
            formals
            ignores
            ignorables
            type-exprs
            satisfies-exprs
            guard)))
      (+ 5
        (acl2-count edcls)
        (acl2-count formals)
        (acl2-count guard)))
    :rule-classes :linear))

(local (encapsulate nil
    (local (defun all-vars1/all-vars1-lst
        (flg lst ans)
        (if (eq flg 'all-vars1)
          (cond ((variablep lst) (add-to-set-eq lst ans))
            ((fquotep lst) ans)
            (t (all-vars1/all-vars1-lst 'all-vars-lst1 (cdr lst) ans)))
          (cond ((endp lst) ans)
            (t (all-vars1/all-vars1-lst 'all-vars-lst1
                (cdr lst)
                (all-vars1/all-vars1-lst 'all-vars1 (car lst) ans)))))))
    (local (defthm step-1-lemma
        (equal (all-vars1/all-vars1-lst flg lst ans)
          (if (equal flg 'all-vars1)
            (all-vars1 lst ans)
            (all-vars1-lst lst ans)))))
    (local (defthm step-2-lemma
        (implies (and (symbol-listp ans)
            (if (equal flg 'all-vars1)
              (pseudo-termp lst)
              (pseudo-term-listp lst)))
          (symbol-listp (all-vars1/all-vars1-lst flg lst ans)))))
    (defthm symbol-listp-all-vars1
      (implies (and (symbol-listp ans) (pseudo-termp lst))
        (symbol-listp (all-vars1 lst ans)))
      :hints (("Goal" :use (:instance step-2-lemma (flg 'all-vars1)))))))

(local (defthm arglistp1-implies-symbol-listp
    (implies (arglistp1 x) (symbol-listp x))
    :hints (("Goal" :in-theory (enable arglistp1)))))

(local (defthm pseudo-term-listp-revappend
    (implies (true-listp x)
      (equal (pseudo-term-listp (revappend x y))
        (and (pseudo-term-listp x) (pseudo-term-listp y))))))

(local (defthm member-symbol-listp-forward-to-symbolp
    (implies (and (member-equal a x) (symbol-listp x))
      (symbolp a))
    :rule-classes :forward-chaining))

(local (defthm pseudo-term-listp-subst-each-for-var
    (implies (and (pseudo-term-listp new-lst)
        (variablep old)
        (pseudo-termp term))
      (pseudo-term-listp (subst-each-for-var new-lst old term)))))

(local (defthm subset-symbol-listp-forward-to-symbol-listp
    (implies (and (subsetp-equal x y) (true-listp x) (symbol-listp y))
      (symbol-listp x))
    :rule-classes :forward-chaining))

(local (defthm pseudo-term-listp-mv-nth-3-syntactically-plausible-lambda-objectp1
    (implies (and (car (syntactically-plausible-lambda-objectp1 edcls
            formals
            ignores
            ignorables
            type-exprs
            satisfies-exprs
            guard))
        (symbol-listp formals)
        (pseudo-term-listp type-exprs))
      (pseudo-term-listp (mv-nth 3
          (syntactically-plausible-lambda-objectp1 edcls
            formals
            ignores
            ignorables
            type-exprs
            satisfies-exprs
            guard))))))

(local (defthm symbol-listp-set-difference-equal
    (implies (symbol-listp x)
      (symbol-listp (set-difference-equal x y)))))

(local (encapsulate nil
    (local (defthm symbol-listp-revappend-lemma
        (implies (not (symbol-listp y))
          (not (symbol-listp (revappend x y))))))
    (defthm symbol-listp-revappend
      (implies (true-listp x)
        (equal (symbol-listp (revappend x y))
          (and (symbol-listp x) (symbol-listp y)))))))

(local (defthm true-listp-mv-nth-1-syntactically-plausible-lambda-objectp1
    (implies (and (car (syntactically-plausible-lambda-objectp1 edcls
            formals
            ignores
            ignorables
            type-exprs
            satisfies-exprs
            guard))
        (symbol-listp ignores)
        (symbol-listp formals))
      (true-listp (mv-nth 1
          (syntactically-plausible-lambda-objectp1 edcls
            formals
            ignores
            ignorables
            type-exprs
            satisfies-exprs
            guard))))))

(local (defthm true-listp-mv-nth-2-syntactically-plausible-lambda-objectp1
    (implies (and (car (syntactically-plausible-lambda-objectp1 edcls
            formals
            ignores
            ignorables
            type-exprs
            satisfies-exprs
            guard))
        (symbol-listp ignorables)
        (symbol-listp formals))
      (true-listp (mv-nth 2
          (syntactically-plausible-lambda-objectp1 edcls
            formals
            ignores
            ignorables
            type-exprs
            satisfies-exprs
            guard))))))

(local (make-flag flag-expand-all-lambdas
    expand-all-lambdas
    :flag-mapping ((expand-all-lambdas term) (expand-all-lambdas-lst terms))))

(local (defthm len-expand-all-lambdas-lst
    (equal (len (expand-all-lambdas-lst terms)) (len terms))))

(local (defthm pseudo-termp-forward-to-pseudo-term-listp-cdr
    (implies (and (pseudo-termp x) (consp x) (consp (car x)))
      (pseudo-term-listp (cdr x)))
    :rule-classes :forward-chaining))

(local (defthm-flag-expand-all-lambdas (defthm type-of-pseudo-termp
      (implies (pseudo-termp term)
        (pseudo-termp (expand-all-lambdas term)))
      :flag term)
    (defthm pseudo-term-listp-expand-all-lambdas-lst
      (implies (pseudo-term-listp terms)
        (pseudo-term-listp (expand-all-lambdas-lst terms)))
      :flag terms)))

(local (make-flag flag-warrants-for-tamep
    warrants-for-tamep
    :flag-mapping ((warrants-for-tamep term) (warrants-for-tamep-functionp fn)
      (warrants-for-suitably-tamep-listp lst))))

(local (defthm-flag-warrants-for-tamep (defthm true-listp-car-warrants-for-tamep
      (implies (and (ilks-plist-worldp wrld)
          (executable-tamep x wrld)
          (true-listp warrants))
        (true-listp (car (warrants-for-tamep x wrld warrants unwarranteds))))
      :flag term)
    (defthm true-listp-car-warrants-for-tamep-functionp
      (implies (and (ilks-plist-worldp wrld)
          (executable-tamep-functionp fn wrld)
          (true-listp warrants))
        (true-listp (car (warrants-for-tamep-functionp fn wrld warrants unwarranteds))))
      :flag fn)
    (defthm true-listp-car-warrants-for-warrants-for-suitably-tamep-listp
      (implies (and (ilks-plist-worldp wrld)
          (executable-suitably-tamep-listp flags args wrld)
          (true-listp warrants))
        (true-listp (car (warrants-for-suitably-tamep-listp flags
              args
              wrld
              warrants
              unwarranteds))))
      :flag lst)))

(local (defthm-flag-warrants-for-tamep (defthm symbol-listp-mv-nth-1-warrants-for-tamep
      (implies (and (ilks-plist-worldp wrld)
          (executable-tamep x wrld)
          (symbol-listp unwarranteds))
        (symbol-listp (mv-nth 1 (warrants-for-tamep x wrld warrants unwarranteds))))
      :flag term)
    (defthm symbol-listp-mv-nth-1-warrants-for-tamep-functionp
      (implies (and (ilks-plist-worldp wrld)
          (executable-tamep-functionp fn wrld)
          (symbol-listp unwarranteds))
        (symbol-listp (mv-nth 1
            (warrants-for-tamep-functionp fn wrld warrants unwarranteds))))
      :flag fn)
    (defthm symbol-listp-mv-nth-1-warrants-for-warrants-for-suitably-tamep-listp
      (implies (and (ilks-plist-worldp wrld)
          (executable-suitably-tamep-listp flags args wrld)
          (symbol-listp unwarranteds))
        (symbol-listp (mv-nth 1
            (warrants-for-suitably-tamep-listp flags
              args
              wrld
              warrants
              unwarranteds))))
      :flag lst)))

(local (make-flag flag-syntactically-plausible-lambda-objectp
    syntactically-plausible-lambda-objectp
    :flag-mapping ((syntactically-plausible-lambda-objectp main) (syntactically-plausible-lambda-objectsp-within within)
      (syntactically-plausible-lambda-objectsp-within-lst listp))))

(local (defthm-flag-syntactically-plausible-lambda-objectp (defthm weak-splo-extracts-tuple-listp-1
      (implies (syntactically-plausible-lambda-objectp gflg x)
        (weak-splo-extracts-tuple-listp (syntactically-plausible-lambda-objectp gflg x)))
      :flag main)
    (defthm weak-splo-extracts-tuple-listp-2
      (let ((ans (syntactically-plausible-lambda-objectsp-within gflg body)))
        (implies ans
          (or (weak-splo-extracts-tuple-listp ans) (equal ans t))))
      :rule-classes nil
      :flag within)
    (defthm weak-splo-extracts-tuple-listp-3
      (let ((ans (syntactically-plausible-lambda-objectsp-within-lst gflg
             args)))
        (implies ans
          (or (weak-splo-extracts-tuple-listp ans) (equal ans t))))
      :rule-classes nil
      :flag listp)))