other
(in-package "ACL2")
other
(verify-termination equal-x-constant)
other
(verify-termination match-tests-and-bindings (declare (xargs :verify-guards nil)))
local
(local (defthm symbol-doublet-listp--mv-nth-1-match-tests-and-bindings (implies (symbol-doublet-listp bindings) (symbol-doublet-listp (mv-nth 1 (match-tests-and-bindings x pat tests bindings dups))))))
local
(local (defthm cdr-assoc-equal-type-for-symbol-doublet-listp (implies (symbol-doublet-listp x) (or (consp (cdr (assoc-equal pat x))) (null (cdr (assoc-equal pat x))))) :rule-classes :type-prescription))
local
(local (defthm assoc-equal-type-for-symbol-doublet-listp (implies (symbol-doublet-listp x) (or (consp (assoc-equal pat x)) (null (assoc-equal pat x)))) :rule-classes :type-prescription))
local
(local (defthm symbol-doublet-listp-forward-to-symbol-alistp (implies (symbol-doublet-listp bindings) (symbol-alistp bindings)) :rule-classes :forward-chaining))
local
(local (defthm cdr-preserves-character-listp (implies (character-listp x) (character-listp (cdr x)))))
local
(local (defthm true-listp-mv-nth-2-match-tests-and-bindings (implies (true-listp dups) (true-listp (mv-nth 2 (match-tests-and-bindings x pat tests bindings dups))))))
local
(local (defthm true-listp-car-match-tests-and-bindings (implies (true-listp tests) (true-listp (car (match-tests-and-bindings x pat tests bindings dups))))))
other
(verify-termination match-clause)
other
(verify-termination match-clause-list)