Technical lemmas to show that opening input/output channels does not
produce a symbol like
Theorem:
(defthm print-base-p-implies-posp (implies (print-base-p x) (posp x)) :rule-classes :forward-chaining)
Theorem:
(defthm print-base-p-bound (implies (print-base-p x) (<= x 16)) :rule-classes :forward-chaining)
Theorem:
(defthm make-output-channel-not-standard-co (implies (posp clock) (not (equal (make-output-channel str clock) *standard-co*))))
Theorem:
(defthm make-input-channel-not-standard-ci (implies (posp clock) (not (equal (make-input-channel str clock) *standard-ci*))))
Theorem:
(defthm make-input-channel-not-standard-oi (implies (posp clock) (not (equal (make-input-channel str clock) *standard-oi*))))
Theorem:
(defthm open-output-channel-is-not-standard-co (implies (state-p1 state) (not (equal (mv-nth 0 (open-output-channel fname type state)) *standard-co*))))
Theorem:
(defthm open-input-channel-is-not-standard-ci (implies (state-p1 state) (not (equal (mv-nth 0 (open-input-channel fname type state)) *standard-ci*))))
Theorem:
(defthm open-input-channel-is-not-standard-oi (implies (state-p1 state) (not (equal (mv-nth 0 (open-input-channel fname type state)) *standard-oi*))))