Built-in axioms and theorems about system utilities.
Theorem:
(defthm pseudo-term-listp-forward-to-true-listp (implies (pseudo-term-listp x) (true-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm legal-variable-or-constant-namep-implies-symbolp (implies (not (symbolp x)) (not (legal-variable-or-constant-namep x))))
Theorem:
(defthm termp-implies-pseudo-termp (implies (termp x w) (pseudo-termp x)) :rule-classes (:rewrite :forward-chaining))
Theorem:
(defthm term-listp-implies-pseudo-term-listp (implies (term-listp x w) (pseudo-term-listp x)) :rule-classes (:rewrite :forward-chaining))
Theorem:
(defthm arities-okp-implies-arity (implies (and (arities-okp user-table w) (assoc fn user-table)) (equal (arity fn w) (cdr (assoc fn user-table)))))
Theorem:
(defthm arities-okp-implies-logicp (implies (and (arities-okp user-table w) (assoc fn user-table)) (logicp fn w)))
Theorem:
(defthm pseudo-termp-consp-forward (implies (and (pseudo-termp x) (consp x)) (true-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm plist-worldp-forward-to-assoc-eq-equal-alistp (implies (plist-worldp x) (assoc-eq-equal-alistp x)) :rule-classes :forward-chaining)
Theorem:
(defthm state-p1-forward (implies (state-p1 x) (and (true-listp x) (equal (length x) 11) (open-channels-p (nth 0 x)) (open-channels-p (nth 1 x)) (ordered-symbol-alistp (nth 2 x)) (all-boundp *initial-global-table* (nth 2 x)) (plist-worldp (cdr (assoc 'current-acl2-world (nth 2 x)))) (symbol-alistp (getpropc 'acl2-defaults-table 'table-alist nil (cdr (assoc 'current-acl2-world (nth 2 x))))) (timer-alistp (cdr (assoc 'timer-alist (nth 2 x)))) (print-base-p (cdr (assoc 'print-base (nth 2 x)))) (known-package-alistp (getpropc 'known-package-alist 'global-value nil (cdr (assoc 'current-acl2-world (nth 2 x))))) (integer-listp (nth 3 x)) (true-listp (nth 4 x)) (file-clock-p (nth 5 x)) (readable-files-p (nth 6 x)) (written-files-p (nth 7 x)) (read-files-p (nth 8 x)) (writeable-files-p (nth 9 x)) (symbol-alistp (nth 10 x)))) :rule-classes :forward-chaining)
Theorem:
(defthm state-p-implies-and-forward-to-state-p1 (implies (state-p state-state) (state-p1 state-state)) :rule-classes (:forward-chaining :rewrite))
Theorem:
(defthm update-acl2-oracle-preserves-state-p1 (implies (and (state-p1 state) (true-listp x)) (state-p1 (update-acl2-oracle x state))))
Theorem:
(defthm read-run-time-preserves-state-p1 (implies (state-p1 state) (state-p1 (nth 1 (read-run-time state)))) :rule-classes ((:forward-chaining :trigger-terms ((nth 1 (read-run-time state))))))
Theorem:
(defthm read-acl2-oracle-preserves-state-p1 (implies (state-p1 state) (state-p1 (nth 2 (read-acl2-oracle state)))) :rule-classes ((:forward-chaining :trigger-terms ((nth 2 (read-acl2-oracle state))))))
Theorem:
(defthm nth-0-read-run-time-type-prescription (implies (state-p1 state) (rationalp (nth 0 (read-run-time state)))) :rule-classes ((:type-prescription :typed-term (nth 0 (read-run-time state)))))
Theorem:
(defthm ordered-symbol-alistp-getprops (implies (plist-worldp w) (ordered-symbol-alistp (getprops key world-name w))))
Theorem:
(defthm state-p1-update-main-timer (implies (state-p1 state) (state-p1 (update-nth 2 (add-pair 'main-timer val (nth 2 state)) state))) :rule-classes ((:forward-chaining :trigger-terms ((update-nth 2 (add-pair 'main-timer val (nth 2 state)) state)))))
Theorem:
(defthm state-p1-update-print-base (implies (and (state-p1 state) (force (print-base-p val))) (state-p1 (update-nth 2 (add-pair 'print-base val (nth 2 state)) state))) :rule-classes ((:forward-chaining :trigger-terms ((update-nth 2 (add-pair 'print-base val (nth 2 state)) state)))))
Theorem:
(defthm state-p1-update-nth-2-world (implies (and (state-p1 state) (plist-worldp wrld) (known-package-alistp (getpropc 'known-package-alist 'global-value nil wrld)) (symbol-alistp (getpropc 'acl2-defaults-table 'table-alist nil wrld))) (state-p1 (update-nth 2 (add-pair 'current-acl2-world wrld (nth 2 state)) state))))
Theorem:
(defthm pseudo-term-listp-mfc-clause (pseudo-term-listp (mfc-clause mfc)))
Theorem:
(defthm type-alistp-mfc-type-alist (type-alistp (mfc-type-alist mfc)))
Theorem:
(defthm fn-count-evg-rec-type-prescription (implies (natp acc) (natp (fn-count-evg-rec evg acc calls))) :rule-classes :type-prescription)
Theorem:
(defthm fn-count-evg-rec-bound (< (fn-count-evg-rec evg acc calls) 536870912) :rule-classes :linear)
Theorem:
(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)))))
Theorem:
(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))))))))
Theorem:
(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))))))))
Theorem:
(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))))))))
Theorem:
(defthm 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))))
Theorem:
(defthm 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)))))
Theorem:
(defthm natp-conjoin-clause-sets-bound (natp (conjoin-clause-sets-bound)) :rule-classes :type-prescription)
Theorem:
(defthm d-pos-listp-forward-to-true-listp (implies (d-pos-listp x) (true-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm true-listp-chars-for-tilde-@-clause-id-phrase/periods (true-listp (chars-for-tilde-@-clause-id-phrase/periods lst)) :rule-classes :type-prescription)
Theorem:
(defthm state-p1-read-acl2-oracle (implies (state-p1 state) (state-p1 (mv-nth 2 (read-acl2-oracle state)))))
Theorem:
(defthm all-boundp-initial-global-table (implies (and (state-p1 state) (assoc-eq x *initial-global-table*)) (assoc-equal x (nth 2 state))))
Theorem:
(defthm all-boundp-initial-global-table-alt (implies (and (state-p1 state) (assoc-eq x *initial-global-table*)) (boundp-global1 x state)))