other
(in-package "ACL2")
other
(verify-termination-boot-strap packn1)
local
(local (defthm character-listp-explode-atom-lemma (implies (character-listp z) (characterp (car (explode-nonnegative-integer x y z))))))
local
(local (defthm character-listp-explode-atom (character-listp (explode-atom x y)) :hints (("Goal" :in-theory (enable explode-atom))) :rule-classes (:rewrite (:forward-chaining :trigger-terms ((explode-atom x y))))))
other
(verify-termination-boot-strap packn)
other
(verify-termination-boot-strap keyword-listp)
other
(verify-termination-boot-strap first-keyword)
other
(verify-termination-boot-strap symbol-name-equal)
other
(verify-termination-boot-strap fix-pkg)
other
(verify-termination-boot-strap unmake-true-list-cons-nest)
other
(verify-termination-boot-strap flatten-ands-in-lit)
other
(verify-termination-boot-strap union-equal-to-end)
other
(verify-termination-boot-strap flatten-ands-in-lit!)
other
(verify-guards warranted-fns-of-world)
other
(partial-encapsulate (((canonical-pathname * * state) => *)) nil (local (defun canonical-pathname (x dir-p state) (declare (xargs :mode :logic)) (declare (ignore dir-p state)) (if (stringp x) x nil))) (defthm canonical-pathname-is-idempotent (equal (canonical-pathname (canonical-pathname x dir-p state) dir-p state) (canonical-pathname x dir-p state))) (defthm canonical-pathname-type (or (equal (canonical-pathname x dir-p state) nil) (stringp (canonical-pathname x dir-p state))) :rule-classes :type-prescription))
other
(partial-encapsulate (((magic-ev-fncall * * state * *) => (mv * *))) nil (logic) (local (defun magic-ev-fncall (fn args state hard-error-returns-nilp aok) (declare (xargs :mode :logic) (ignore fn args state hard-error-returns-nilp aok)) (mv nil nil))))
other
(partial-encapsulate (((mfc-ap-fn * * state *) => *) ((mfc-relieve-hyp-fn * * * * * * state *) => *) ((mfc-relieve-hyp-ttree * * * * * * state *) => (mv * *)) ((mfc-rw+-fn * * * * * state *) => *) ((mfc-rw+-ttree * * * * * state *) => (mv * *)) ((mfc-rw-fn * * * * state *) => *) ((mfc-rw-ttree * * * * state *) => (mv * *)) ((mfc-ts-fn * * state *) => *) ((mfc-ts-ttree * * state *) => (mv * *))) nil (logic) (set-ignore-ok t) (set-irrelevant-formals-ok t) (local (defun mfc-ts-fn (term mfc state forcep) t)) (local (defun mfc-ts-ttree (term mfc state forcep) (mv t t))) (local (defun mfc-rw-fn (term obj equiv-info mfc state forcep) t)) (local (defun mfc-rw-ttree (term obj equiv-info mfc state forcep) (mv t t))) (local (defun mfc-rw+-fn (term alist obj equiv-info mfc state forcep) t)) (local (defun mfc-rw+-ttree (term alist obj equiv-info mfc state forcep) (mv t t))) (local (defun mfc-relieve-hyp-fn (hyp alist rune target bkptr mfc state forcep) t)) (local (defun mfc-relieve-hyp-ttree (hyp alist rune target bkptr mfc state forcep) (mv t t))) (local (defun mfc-ap-fn (term mfc state forcep) t)))
other
(set-brr-data-attachments)
other
(verify-termination-boot-strap cbd-fn)
other
(verify-guards cbd-fn :hints (("Goal" :in-theory (enable state-p1))))
encapsulate
(encapsulate ((too-many-ifs-post-rewrite (args val) t :guard (and (pseudo-term-listp args) (pseudo-termp val)))) (local (defun too-many-ifs-post-rewrite (args val) (list args val))))
encapsulate
(encapsulate nil (logic) (local (defun-nx pseudo-termp-flg (flg x lst) (declare (xargs :verify-guards nil :normalize nil :measure (case flg (term (acl2-count x)) (otherwise (acl2-count lst))))) (case flg (term (if (consp x) (cond ((equal (car x) 'quote) (and (consp (cdr x)) (equal (cddr x) nil))) ((true-listp x) (and (pseudo-termp-flg 'list nil (cdr x)) (cond ((symbolp (car x)) t) ((true-listp (car x)) (and (equal (length (car x)) 3) (equal (caar x) 'lambda) (symbol-listp (cadar x)) (pseudo-termp-flg 'term (caddar x) nil) (equal (length (cadar x)) (length (cdr x))))) (t nil)))) (t nil)) (symbolp x))) (otherwise (if (consp lst) (and (pseudo-termp-flg 'term (car lst) nil) (pseudo-termp-flg 'list nil (cdr lst))) (equal lst nil)))))) (local (defthm pseudo-termp-flg-equivalences (equal (pseudo-termp-flg flg x lst) (case flg (term (pseudo-termp x)) (otherwise (pseudo-term-listp lst)))) :hints (("goal" :induct (pseudo-termp-flg flg x lst))))) (local (in-theory (disable (:definition pseudo-termp-flg)))) (verify-termination-boot-strap max) (verify-termination-boot-strap var-counts1) (local (defun-nx var-counts1-flg (flg rhs arg lst acc) (declare (xargs :verify-guards nil :normalize nil :measure (case flg (term (acl2-count rhs)) (otherwise (acl2-count lst))) :hints nil :well-founded-relation o< :mode :logic) (ignorable rhs arg lst acc)) (case flg (term (cond ((equal arg rhs) (+ 1 acc)) ((consp rhs) (cond ((equal 'quote (car rhs)) acc) ((equal (car rhs) 'if) (max (var-counts1-flg 'term (caddr rhs) arg nil acc) (var-counts1-flg 'term (cadddr rhs) arg nil acc))) (t (var-counts1-flg 'list nil arg (cdr rhs) acc)))) (t acc))) (otherwise (if (consp lst) (var-counts1-flg 'list nil arg (cdr lst) (var-counts1-flg 'term (car lst) arg nil acc)) acc))))) (local (defthm var-counts1-flg-equivalences (equal (var-counts1-flg flg rhs arg lst acc) (case flg (term (var-counts1 arg rhs acc)) (otherwise (var-counts1-lst arg lst acc)))))) (local (in-theory (disable (:definition var-counts1-flg)))) (local (defthm natp-var-counts1 (case flg (term (implies (natp acc) (natp (var-counts1 arg rhs acc)))) (otherwise (implies (natp acc) (natp (var-counts1-lst arg lst acc))))) :hints (("Goal" :induct (var-counts1-flg flg rhs arg lst acc))) :rule-classes nil)) (local (defthm natp-var-counts1-term (implies (natp acc) (natp (var-counts1 arg rhs acc))) :hints (("Goal" :use ((:instance natp-var-counts1 (flg 'term))))) :rule-classes :type-prescription)) (local (defthm natp-var-counts1-list (implies (natp acc) (natp (var-counts1-lst arg lst acc))) :hints (("Goal" :use ((:instance natp-var-counts1 (flg 'list))))) :rule-classes :type-prescription)) (verify-guards var-counts1) (verify-termination-boot-strap var-counts) (local (defthm integer-listp-var-counts (integer-listp (var-counts lhs-args rhs)))) (local (defthm len-var-counts (equal (len (var-counts lhs-args rhs)) (len lhs-args)))) (verify-termination-boot-strap count-ifs) (verify-termination-boot-strap ifix) (verify-termination-boot-strap abs) (verify-termination-boot-strap expt) (local (defthm natp-expt (implies (and (integerp base) (integerp n) (<= 0 n)) (integerp (expt base n))) :rule-classes :type-prescription)) (verify-termination-boot-strap signed-byte-p) (verify-termination-boot-strap too-many-ifs0) (verify-termination-boot-strap too-many-ifs-pre-rewrite-builtin) (verify-termination-boot-strap occur-cnt-bounded) (local (defun-nx occur-cnt-bounded-flg (flg term2 term1 lst a m bound-m) (declare (xargs :verify-guards nil :normalize nil :measure (case flg (term (acl2-count term2)) (otherwise (acl2-count lst)))) (ignorable term2 term1 lst a m bound-m)) (case flg (term (cond ((equal term1 term2) (if (< bound-m a) -1 (+ a m))) ((consp term2) (if (equal 'quote (car term2)) a (occur-cnt-bounded-flg 'list nil term1 (cdr term2) a m bound-m))) (t a))) (otherwise (if (consp lst) (let ((new (occur-cnt-bounded-flg 'term (car lst) term1 nil a m bound-m))) (if (equal new -1) -1 (occur-cnt-bounded-flg 'list nil term1 (cdr lst) new m bound-m))) a))))) (local (defthm occur-cnt-bounded-flg-equivalences (equal (occur-cnt-bounded-flg flg term2 term1 lst a m bound-m) (case flg (term (occur-cnt-bounded term1 term2 a m bound-m)) (otherwise (occur-cnt-bounded-lst term1 lst a m bound-m)))))) (local (in-theory (disable (:definition occur-cnt-bounded-flg)))) (local (defthm integerp-occur-cnt-bounded (case flg (term (implies (and (integerp a) (integerp m)) (integerp (occur-cnt-bounded term1 term2 a m bound-m)))) (otherwise (implies (and (integerp a) (integerp m)) (integerp (occur-cnt-bounded-lst term1 lst a m bound-m))))) :rule-classes nil :hints (("Goal" :induct (occur-cnt-bounded-flg flg term2 term1 lst a m bound-m))))) (local (defthm integerp-occur-cnt-bounded-term (implies (and (integerp a) (integerp m)) (integerp (occur-cnt-bounded term1 term2 a m bound-m))) :rule-classes :type-prescription :hints (("goal" :use ((:instance integerp-occur-cnt-bounded (flg 'term))))))) (local (defthm integerp-occur-cnt-bounded-list (implies (and (integerp a) (integerp m)) (integerp (occur-cnt-bounded-lst term1 lst a m bound-m))) :rule-classes :type-prescription :hints (("goal" :use ((:instance integerp-occur-cnt-bounded (flg 'list))))))) (local (defthm signed-byte-p-*fixnum-bits*-occur-cnt-bounded-flg (case flg (term (implies (and (force (signed-byte-p *fixnum-bits* a)) (signed-byte-p *fixnum-bits* m) (signed-byte-p *fixnum-bits* (+ bound-m m)) (force (<= 0 a)) (<= 0 m) (<= 0 bound-m) (<= a (+ bound-m m))) (and (<= -1 (occur-cnt-bounded term1 term2 a m bound-m)) (<= (occur-cnt-bounded term1 term2 a m bound-m) (+ bound-m m))))) (otherwise (implies (and (force (signed-byte-p *fixnum-bits* a)) (signed-byte-p *fixnum-bits* m) (signed-byte-p *fixnum-bits* (+ bound-m m)) (force (<= 0 a)) (<= 0 m) (<= 0 bound-m) (<= a (+ bound-m m))) (and (<= -1 (occur-cnt-bounded-lst term1 lst a m bound-m)) (<= (occur-cnt-bounded-lst term1 lst a m bound-m) (+ bound-m m)))))) :rule-classes nil :hints (("Goal" :induct (occur-cnt-bounded-flg flg term2 term1 lst a m bound-m))))) (local (defthm signed-byte-p-*fixnum-bits*-occur-cnt-bounded-flg-term (implies (and (force (signed-byte-p *fixnum-bits* a)) (signed-byte-p *fixnum-bits* m) (signed-byte-p *fixnum-bits* (+ bound-m m)) (force (<= 0 a)) (<= 0 m) (<= 0 bound-m) (<= a (+ bound-m m))) (and (<= -1 (occur-cnt-bounded term1 term2 a m bound-m)) (<= (occur-cnt-bounded term1 term2 a m bound-m) (+ bound-m m)))) :rule-classes :linear :hints (("Goal" :use ((:instance signed-byte-p-*fixnum-bits*-occur-cnt-bounded-flg (flg 'term))))))) (local (defthm signed-byte-p-*fixnum-bits*-occur-cnt-bounded-flg-list (implies (and (force (signed-byte-p *fixnum-bits* a)) (signed-byte-p *fixnum-bits* m) (signed-byte-p *fixnum-bits* (+ bound-m m)) (force (<= 0 a)) (<= 0 m) (<= 0 bound-m) (<= a (+ bound-m m))) (and (<= -1 (occur-cnt-bounded-lst term1 lst a m bound-m)) (<= (occur-cnt-bounded-lst term1 lst a m bound-m) (+ bound-m m)))) :rule-classes :linear :hints (("Goal" :use ((:instance signed-byte-p-*fixnum-bits*-occur-cnt-bounded-flg (flg 'list))))))) (verify-guards occur-cnt-bounded) (verify-termination-boot-strap too-many-ifs1) (verify-termination-boot-strap too-many-ifs-post-rewrite-builtin))
other
(defattach too-many-ifs-post-rewrite too-many-ifs-post-rewrite-builtin)
encapsulate
(encapsulate ((too-many-ifs-pre-rewrite (args counts) t :guard (and (pseudo-term-listp args) (integer-listp counts) (equal (len args) (len counts))))) (local (defun too-many-ifs-pre-rewrite (args counts) (list args counts))))
other
(defattach (too-many-ifs-pre-rewrite too-many-ifs-pre-rewrite-builtin))
other
(verify-termination-boot-strap pseudo-variantp)
other
(verify-termination-boot-strap member-char-stringp)
other
(verify-termination-boot-strap terminal-substringp1)
other
(verify-termination-boot-strap terminal-substringp)
other
(verify-termination-boot-strap evg-occur)
other
(verify-termination-boot-strap min-fixnat$inline)
other
(verify-termination-boot-strap fn-count-evg-rec (declare (xargs :verify-guards nil)))
fn-count-evg-rec-type-prescriptiontheorem
(defthm fn-count-evg-rec-type-prescription (implies (natp acc) (natp (fn-count-evg-rec evg acc calls))) :rule-classes :type-prescription)
fn-count-evg-rec-boundtheorem
(defthm fn-count-evg-rec-bound (< (fn-count-evg-rec evg acc calls) 536870912) :rule-classes :linear)
other
(verify-guards fn-count-evg-rec)
other
(verify-termination-boot-strap occur)
other
(verify-termination-boot-strap worse-than-builtin-clocked)
other
(verify-termination-boot-strap worse-than-builtin)
other
(verify-termination-boot-strap worse-than-or-equal-builtin)
other
(verify-termination-boot-strap ancestor-listp)
other
(verify-termination-boot-strap earlier-ancestor-biggerp)
other
(verify-termination-boot-strap fn-count-1)
fn-count-1-typetheorem
(defthm fn-count-1-type (implies (and (integerp fn-count-acc) (integerp p-fn-count-acc)) (and (integerp (car (fn-count-1 flag term fn-count-acc p-fn-count-acc))) (integerp (mv-nth 0 (fn-count-1 flag term fn-count-acc p-fn-count-acc))) (integerp (mv-nth 1 (fn-count-1 flag term fn-count-acc p-fn-count-acc))) (integerp (nth 0 (fn-count-1 flag term fn-count-acc p-fn-count-acc))) (integerp (nth 1 (fn-count-1 flag term fn-count-acc p-fn-count-acc))))) :rule-classes ((:forward-chaining :trigger-terms ((fn-count-1 flag term fn-count-acc p-fn-count-acc)))))
other
(verify-guards fn-count-1)
other
(verify-termination-boot-strap var-fn-count-1)
symbol-listp-cdr-assoc-equaltheorem
(defthm symbol-listp-cdr-assoc-equal (implies (symbol-list-listp x) (symbol-listp (cdr (assoc-equal key x)))))
integerp-nth-0-var-fn-count-1theorem
(defthm integerp-nth-0-var-fn-count-1 (implies (integerp var-count-acc) (integerp (nth 0 (var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table)))) :rule-classes ((:forward-chaining :trigger-terms ((var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table)) :corollary (implies (integerp var-count-acc) (and (integerp (nth 0 (var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table))) (integerp (mv-nth 0 (var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table))) (integerp (car (var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table))))))))
integerp-nth-1-var-fn-count-1theorem
(defthm integerp-nth-1-var-fn-count-1 (implies (integerp fn-count-acc) (integerp (nth 1 (var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table)))) :rule-classes ((:forward-chaining :trigger-terms ((var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table)) :corollary (implies (integerp fn-count-acc) (and (integerp (nth 1 (var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table))) (integerp (mv-nth 1 (var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table))))))))
integerp-nth-2-var-fn-count-1theorem
(defthm integerp-nth-2-var-fn-count-1 (implies (integerp p-fn-count-acc) (integerp (nth 2 (var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table)))) :rule-classes ((:forward-chaining :trigger-terms ((var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table)) :corollary (implies (integerp p-fn-count-acc) (and (integerp (nth 2 (var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table))) (integerp (mv-nth 2 (var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table))))))))
other
(verify-guards var-fn-count-1)
other
(verify-termination-boot-strap equal-mod-commuting)
other
(verify-termination-boot-strap ancestors-check1)
other
(verify-termination-boot-strap ancestors-check-builtin)
member-equal-mod-commutingfunction
(defun member-equal-mod-commuting (x lst wrld) (declare (xargs :guard (and (pseudo-termp x) (pseudo-term-listp lst) (plist-worldp wrld)))) (cond ((endp lst) nil) ((equal-mod-commuting x (car lst) wrld) lst) (t (member-equal-mod-commuting x (cdr lst) wrld))))
strip-ancestor-literalsfunction
(defun strip-ancestor-literals (ancestors) (declare (xargs :guard (ancestor-listp ancestors))) (cond ((endp ancestors) nil) (t (cons (access ancestor (car ancestors) :lit) (strip-ancestor-literals (cdr ancestors))))))
encapsulate
(encapsulate nil (local (defthm ancestors-check1-property (mv-let (on-ancestors assumed-true) (ancestors-check1 lit-atm lit var-cnt fn-cnt p-fn-cnt ancestors tokens) (implies (and on-ancestors assumed-true) (member-equal-mod-commuting lit (strip-ancestor-literals ancestors) nil))) :rule-classes nil)) (defthmd ancestors-check-builtin-property (mv-let (on-ancestors assumed-true) (ancestors-check-builtin lit ancestors tokens) (implies (and on-ancestors assumed-true) (member-equal-mod-commuting lit (strip-ancestor-literals ancestors) nil))) :hints (("Goal" :use ((:instance ancestors-check1-property (lit-atm lit) (var-cnt 0) (fn-cnt 0) (p-fn-cnt 0)) (:instance ancestors-check1-property (lit-atm lit) (var-cnt (nth 0 (var-fn-count-1 nil lit 0 0 0 nil nil))) (fn-cnt (nth 1 (var-fn-count-1 nil lit 0 0 0 nil nil))) (p-fn-cnt (nth 2 (var-fn-count-1 nil lit 0 0 0 nil nil)))) (:instance ancestors-check1-property (lit-atm (cadr lit)) (var-cnt (nth 0 (var-fn-count-1 nil (cadr lit) 0 0 0 nil nil))) (fn-cnt (nth 1 (var-fn-count-1 nil (cadr lit) 0 0 0 nil nil))) (p-fn-cnt (nth 2 (var-fn-count-1 nil (cadr lit) 0 0 0 nil nil)))))))))
encapsulate
(encapsulate ((ancestors-check (lit ancestors tokens) (mv t t) :guard (and (pseudo-termp lit) (ancestor-listp ancestors) (true-listp tokens)))) (local (defun ancestors-check (lit ancestors tokens) (ancestors-check-builtin lit ancestors tokens))) (defthmd ancestors-check-constraint (implies (and (pseudo-termp lit) (ancestor-listp ancestors) (true-listp tokens)) (mv-let (on-ancestors assumed-true) (ancestors-check lit ancestors tokens) (implies (and on-ancestors assumed-true) (member-equal-mod-commuting lit (strip-ancestor-literals ancestors) nil)))) :hints (("Goal" :use ancestors-check-builtin-property))))
other
(defattach (ancestors-check ancestors-check-builtin) :hints (("Goal" :by ancestors-check-builtin-property)))
other
(defattach worse-than worse-than-builtin)
other
(defattach worse-than-or-equal worse-than-or-equal-builtin)
other
(verify-termination-boot-strap hons-copy-with-state)
other
(verify-termination-boot-strap identity-with-state)
other
(defattach (acl2x-expansion-alist identity-with-state))
other
(defattach rw-cache-debug rw-cache-debug-builtin)
other
(defattach rw-cache-debug-action rw-cache-debug-action-builtin)
other
(defattach rw-cacheable-failure-reason rw-cacheable-failure-reason-builtin)
other
(verify-termination-boot-strap all-digits-p)
other
(verify-termination-boot-strap (d-pos-listp (declare (xargs :guard-hints (("Goal" :use ((:instance coerce-inverse-2 (x (symbol-name (car lst)))) (:instance character-listp-coerce (str (symbol-name (car lst))))) :expand ((len (coerce (symbol-name (car lst)) 'list))) :in-theory (disable coerce-inverse-2 character-listp-coerce)))))))
other
(verify-termination-boot-strap pos-listp)
other
(verify-guards pos-listp)
d-pos-listp-forward-to-true-listptheorem
(defthm d-pos-listp-forward-to-true-listp (implies (d-pos-listp x) (true-listp x)) :rule-classes :forward-chaining)
other
(verify-termination-boot-strap clause-id-p)
encapsulate
(encapsulate (((print-clause-id-okp *) => * :formals (cl-id) :guard (clause-id-p cl-id))) (local (defun print-clause-id-okp (x) x)))
other
(defattach print-clause-id-okp print-clause-id-okp-builtin)
encapsulate
(encapsulate (((oncep-tp * *) => * :formals (rune wrld) :guard (and (plist-worldp wrld) (and (consp rune) (consp (cdr rune)) (symbolp (cadr rune)))))) (logic) (local (defun oncep-tp (rune wrld) (oncep-tp-builtin rune wrld))))
other
(defattach oncep-tp oncep-tp-builtin)
other
(verify-termination-boot-strap chars-for-tilde-@-clause-id-phrase/periods)
other
(verify-termination-boot-strap chars-for-tilde-@-clause-id-phrase/primes)
pos-listp-forward-to-integer-listptheorem
(defthm pos-listp-forward-to-integer-listp (implies (pos-listp x) (integer-listp x)) :rule-classes :forward-chaining)
other
(verify-termination-boot-strap chars-for-tilde-@-clause-id-phrase)
true-listp-chars-for-tilde-@-clause-id-phrase/periodstheorem
(defthm true-listp-chars-for-tilde-@-clause-id-phrase/periods (true-listp (chars-for-tilde-@-clause-id-phrase/periods lst)) :rule-classes :type-prescription)
true-listp-explode-atomtheorem
(defthm true-listp-explode-atom (true-listp (explode-atom n print-base)) :rule-classes :type-prescription)
encapsulate
(encapsulate nil (local (defthm character-listp-chars-for-tilde-@-clause-id-phrase/periods (character-listp (chars-for-tilde-@-clause-id-phrase/periods lst)))) (verify-termination-boot-strap string-for-tilde-@-clause-id-phrase))
other
(verify-termination-boot-strap strict-merge-symbol< (declare (xargs :measure (+ (len l1) (len l2)))))
symbol-listp-strict-merge-sort-symbol<encapsulate
(encapsulate nil (local (defthm len-strict-merge-symbol< (<= (len (strict-merge-symbol< l1 l2 acc)) (+ (len l1) (len l2) (len acc))) :rule-classes :linear)) (local (defthm len-evens (equal (len l) (+ (len (evens l)) (len (odds l)))) :rule-classes :linear)) (local (defthm symbol-listp-evens (implies (symbol-listp x) (symbol-listp (evens x))) :hints (("Goal" :induct (evens x))))) (local (defthm symbol-listp-odds (implies (symbol-listp x) (symbol-listp (odds x))))) (local (defthm symbol-listp-strict-merge-symbol< (implies (and (symbol-listp l1) (symbol-listp l2) (symbol-listp acc)) (symbol-listp (strict-merge-symbol< l1 l2 acc))))) (verify-termination-boot-strap strict-merge-sort-symbol< (declare (xargs :measure (len l) :verify-guards nil))) (defthm symbol-listp-strict-merge-sort-symbol< (implies (symbol-listp x) (symbol-listp (strict-merge-sort-symbol< x)))) (verify-guards strict-merge-sort-symbol<) (verify-termination-boot-strap sort-symbol-listp))
other
(verify-termination-boot-strap ld-history)
other
(verify-termination-boot-strap ld-history-entry-input)
other
(verify-termination-boot-strap ld-history-entry-error-flg)
other
(verify-termination-boot-strap ld-history-entry-stobjs-out/value)
other
(verify-termination-boot-strap ld-history-entry-stobjs-out)
other
(verify-termination-boot-strap ld-history-entry-value)
other
(verify-termination-boot-strap ld-history-entry-user-data)
other
(verify-termination-boot-strap set-ld-history-entry-user-data-default)
other
(defattach set-ld-history-entry-user-data set-ld-history-entry-user-data-default)
other
(deftheory definition-minimal-theory (definition-runes *definition-minimal-theory* nil world))
other
(deftheory executable-counterpart-minimal-theory (definition-runes *built-in-executable-counterparts* t world))
other
(deftheory minimal-theory (union-theories (theory 'definition-minimal-theory) (union-theories '((:executable-counterpart force)) (theory 'executable-counterpart-minimal-theory))))
*acl2-primitives*constant
(defconst *acl2-primitives* (strip-cars *primitive-formals-and-guards*))
other
(deftheory acl2-primitives (definition-runes *acl2-primitives* nil world))
in-theory
(in-theory (if (cadr *tau-status-boot-strap-settings*) (enable (:executable-counterpart tau-system)) (disable (:executable-counterpart tau-system))))
in-theory
(in-theory (disable (:e print-call-history)))
other
(verify-termination-boot-strap formals)
meta-extract-formulafunction
(defund meta-extract-formula (name state) (declare (xargs :stobjs state :guard (symbolp name))) (let ((wrld (w state))) (or (getpropc name 'theorem nil wrld) (cond ((logicp name wrld) (mv-let (flg prop origins) (constraint-info name wrld) (declare (ignore origins)) (cond ((unknown-constraints-p prop) *t*) (flg (ec-call (conjoin prop))) (t prop)))) (t *t*)))))
other
(verify-termination-boot-strap type-set-quote)
other
(verify-guards type-set-quote)
typespec-checkfunction
(defun typespec-check (ts x) (declare (xargs :guard (integerp ts))) (if (bad-atom x) (< ts 0) (not (eql 0 (logand (type-set-quote x) ts)))))
meta-extract-rw+-termfunction
(defun meta-extract-rw+-term (term alist equiv rhs state) (declare (xargs :mode :program :stobjs state :guard (and (symbol-alistp alist) (pseudo-term-listp (strip-cdrs alist)) (pseudo-termp term)))) (non-exec (let ((lhs (sublis-var alist term))) (case equiv ((nil) `(equal ,LHS ,RHS)) ((t) `(iff ,LHS ,RHS)) (otherwise (if (symbolp equiv) (if (equivalence-relationp equiv (w state)) `(,EQUIV ,LHS ,RHS) *t*) *t*))))))
meta-extract-contextual-factfunction
(defun meta-extract-contextual-fact (obj mfc state) (declare (xargs :mode :program :stobjs state)) (non-exec (case-match obj ((':typeset term . &) `(typespec-check ',(MFC-TS TERM MFC STATE :FORCEP NIL :TTREEP NIL) ,TERM)) ((':rw+ term alist obj equiv . &) (meta-extract-rw+-term term alist equiv (mfc-rw+ term alist obj equiv mfc state :forcep nil :ttreep nil) state)) ((':rw term obj equiv . &) (meta-extract-rw+-term term nil equiv (mfc-rw term obj equiv mfc state :forcep nil :ttreep nil) state)) ((':ap term . &) (if (mfc-ap term mfc state :forcep nil) `(not ,TERM) *t*)) ((':relieve-hyp hyp alist rune target bkptr . &) (if (mfc-relieve-hyp hyp alist rune target bkptr mfc state :forcep nil :ttreep nil) (sublis-var alist hyp) *t*)) (& *t*))))
rewrite-rule-term-execfunction
(defun rewrite-rule-term-exec (x) (declare (xargs :guard (and (weak-rewrite-rule-p x) (or (eq (access rewrite-rule x :subclass) 'meta) (true-listp (access rewrite-rule x :hyps)))))) (if (eq (access rewrite-rule x :subclass) 'meta) *t* `(implies ,(CONJOIN (ACCESS REWRITE-RULE X :HYPS)) (,(ACCESS REWRITE-RULE X :EQUIV) ,(ACCESS REWRITE-RULE X :LHS) ,(ACCESS REWRITE-RULE X :RHS)))))
rewrite-rule-termfunction
(defun rewrite-rule-term (x) (declare (xargs :guard t)) (ec-call (rewrite-rule-term-exec x)))
linear-lemma-term-execfunction
(defun linear-lemma-term-exec (x) (declare (xargs :guard (and (weak-linear-lemma-p x) (true-listp (access linear-lemma x :hyps))))) `(implies ,(CONJOIN (ACCESS LINEAR-LEMMA X :HYPS)) ,(ACCESS LINEAR-LEMMA X :CONCL)))
linear-lemma-termfunction
(defun linear-lemma-term (x) (declare (xargs :guard t)) (ec-call (linear-lemma-term-exec x)))
meta-extract-global-factmacro
(defmacro meta-extract-global-fact (obj state) `(meta-extract-global-fact+ ,OBJ ,STATE ,STATE))
fncall-termfunction
(defun fncall-term (fn arglist state) (declare (xargs :stobjs state :guard (and (symbolp fn) (true-listp arglist)))) (cond ((logicp fn (w state)) (mv-let (erp val) (magic-ev-fncall fn arglist state t nil) (cond (erp *t*) (t (fcons-term* 'equal (fcons-term fn (kwote-lst arglist)) (kwote val)))))) (t *t*)))
logically-equivalent-statesfunction
(defun logically-equivalent-states (st1 st2) (declare (xargs :guard t)) (non-exec (equal (w st1) (w st2))))
meta-extract-global-fact+function
(defun meta-extract-global-fact+ (obj st state) (declare (xargs :mode :program :stobjs state)) (non-exec (cond ((logically-equivalent-states st state) (case-match obj ((':formula name) (meta-extract-formula name st)) ((':lemma fn n) (let* ((lemmas (getpropc fn 'lemmas nil (w st))) (rule (nth n lemmas))) (if (< (nfix n) (len lemmas)) (rewrite-rule-term rule) *t*))) ((':linear-lemma fn n) (let* ((lemmas (getpropc fn 'linear-lemmas nil (w st))) (rule (nth n lemmas))) (if (< (nfix n) (len lemmas)) (linear-lemma-term rule) *t*))) ((':fncall fn arglist) (non-exec (fncall-term fn arglist st))) (& *t*))) (t *t*))))
other
(defun-nx read-user-stobj-alist (st state) (declare (xargs :guard (symbolp st) :stobjs state)) (cdr (assoc-eq st (user-stobj-alist1 state))))
other
(defun-nx write-user-stobj-alist (st val state) (declare (xargs :guard (symbolp st) :stobjs state)) (update-user-stobj-alist1 (put-assoc-eq st val (user-stobj-alist1 state)) state))