Recognizer for bip44-coin-type-set.
(bip44-coin-type-setp x) → *
Function:
(defun bip44-coin-type-setp (x) (declare (xargs :guard t)) (if (atom x) (null x) (and (bip44-coin-type-p (car x)) (or (null (cdr x)) (and (consp (cdr x)) (acl2::fast-<< (car x) (cadr x)) (bip44-coin-type-setp (cdr x)))))))
Theorem:
(defthm booleanp-ofbip44-coin-type-setp (booleanp (bip44-coin-type-setp x)))
Theorem:
(defthm setp-when-bip44-coin-type-setp (implies (bip44-coin-type-setp x) (setp x)) :rule-classes (:rewrite))
Theorem:
(defthm bip44-coin-type-p-of-head-when-bip44-coin-type-setp (implies (bip44-coin-type-setp x) (equal (bip44-coin-type-p (head x)) (not (emptyp x)))))
Theorem:
(defthm bip44-coin-type-setp-of-tail-when-bip44-coin-type-setp (implies (bip44-coin-type-setp x) (bip44-coin-type-setp (tail x))))
Theorem:
(defthm bip44-coin-type-setp-of-insert (equal (bip44-coin-type-setp (insert a x)) (and (bip44-coin-type-p a) (bip44-coin-type-setp (sfix x)))))
Theorem:
(defthm bip44-coin-type-p-when-in-bip44-coin-type-setp-binds-free-x (implies (and (in a x) (bip44-coin-type-setp x)) (bip44-coin-type-p a)))
Theorem:
(defthm bip44-coin-type-setp-of-union (equal (bip44-coin-type-setp (union x y)) (and (bip44-coin-type-setp (sfix x)) (bip44-coin-type-setp (sfix y)))))
Theorem:
(defthm bip44-coin-type-setp-of-intersect (implies (and (bip44-coin-type-setp x) (bip44-coin-type-setp y)) (bip44-coin-type-setp (intersect x y))))
Theorem:
(defthm bip44-coin-type-setp-of-difference (implies (bip44-coin-type-setp x) (bip44-coin-type-setp (difference x y))))
Theorem:
(defthm bip44-coin-type-setp-of-delete (implies (bip44-coin-type-setp x) (bip44-coin-type-setp (delete a x))))