Built-in axioms and theorems about input/output.
Theorem:
(defthm open-channel1-forward-to-true-listp-and-consp (implies (open-channel1 x) (and (true-listp x) (consp x))) :rule-classes :forward-chaining)
Theorem:
(defthm open-channels-p-forward (implies (open-channels-p x) (and (ordered-symbol-alistp x) (true-list-listp x))) :rule-classes :forward-chaining)
Theorem:
(defthm true-listp-cadr-assoc-eq-for-open-channels-p (implies (open-channels-p alist) (true-listp (cadr (assoc-eq key alist)))) :rule-classes ((:forward-chaining :trigger-terms ((cadr (assoc-eq key alist))))))
Theorem:
(defthm file-clock-p-forward-to-integerp (implies (file-clock-p x) (natp x)) :rule-classes :forward-chaining)
Theorem:
(defthm readable-file-forward-to-true-listp-and-consp (implies (readable-file x) (and (true-listp x) (consp x))) :rule-classes :forward-chaining)
Theorem:
(defthm readable-files-listp-forward-to-true-list-listp-and-alistp (implies (readable-files-listp x) (and (true-list-listp x) (alistp x))) :rule-classes :forward-chaining)
Theorem:
(defthm readable-files-p-forward-to-readable-files-listp (implies (readable-files-p x) (readable-files-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm written-file-forward-to-true-listp-and-consp (implies (written-file x) (and (true-listp x) (consp x))) :rule-classes :forward-chaining)
Theorem:
(defthm written-file-listp-forward-to-true-list-listp-and-alistp (implies (written-file-listp x) (and (true-list-listp x) (alistp x))) :rule-classes :forward-chaining)
Theorem:
(defthm written-files-p-forward-to-written-file-listp (implies (written-files-p x) (written-file-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm read-file-listp1-forward-to-true-listp-and-consp (implies (read-file-listp1 x) (and (true-listp x) (consp x))) :rule-classes :forward-chaining)
Theorem:
(defthm read-file-listp-forward-to-true-list-listp (implies (read-file-listp x) (true-list-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm read-files-p-forward-to-read-file-listp (implies (read-files-p x) (read-file-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm writable-file-listp1-forward-to-true-listp-and-consp (implies (writable-file-listp1 x) (and (true-listp x) (consp x))) :rule-classes :forward-chaining)
Theorem:
(defthm writable-file-listp-forward-to-true-list-listp (implies (writable-file-listp x) (true-list-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm writeable-files-p-forward-to-writable-file-listp (implies (writeable-files-p x) (writable-file-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm canonical-pathname-is-idempotent (equal (canonical-pathname (canonical-pathname x dir-p state) dir-p state) (canonical-pathname x dir-p state)))
Theorem:
(defthm canonical-pathname-type (or (equal (canonical-pathname x dir-p state) nil) (stringp (canonical-pathname x dir-p state))) :rule-classes :type-prescription)