Function:
(defun imap-cst-command-auth-conc? (cst) (declare (xargs :guard (treep cst))) (declare (xargs :guard (imap-cst-matchp cst "command-auth"))) (let ((__function__ 'imap-cst-command-auth-conc?)) (declare (ignorable __function__)) (cond ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "append")) 1) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "create")) 2) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "delete")) 3) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "examine")) 4) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "list")) 5) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "lsub")) 6) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "rename")) 7) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "select")) 8) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "status")) 9) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "subscribe")) 10) ((equal (tree-nonleaf->rulename? (nth 0 (nth 0 (tree-nonleaf->branches cst)))) (rulename "unsubscribe")) 11) (t (prog2$ (acl2::impossible) 1)))))
Theorem:
(defthm posp-of-imap-cst-command-auth-conc? (b* ((number (imap-cst-command-auth-conc? cst))) (posp number)) :rule-classes :rewrite)
Theorem:
(defthm imap-cst-command-auth-conc?-possibilities (b* ((number (imap-cst-command-auth-conc? cst))) (or (equal number 1) (equal number 2) (equal number 3) (equal number 4) (equal number 5) (equal number 6) (equal number 7) (equal number 8) (equal number 9) (equal number 10) (equal number 11))) :rule-classes ((:forward-chaining :trigger-terms ((imap-cst-command-auth-conc? cst)))))
Theorem:
(defthm imap-cst-command-auth-conc?-of-tree-fix-cst (equal (imap-cst-command-auth-conc? (tree-fix cst)) (imap-cst-command-auth-conc? cst)))
Theorem:
(defthm imap-cst-command-auth-conc?-tree-equiv-congruence-on-cst (implies (tree-equiv cst cst-equiv) (equal (imap-cst-command-auth-conc? cst) (imap-cst-command-auth-conc? cst-equiv))) :rule-classes :congruence)
Theorem:
(defthm imap-cst-command-auth-conc?-1-iff-match-conc (implies (imap-cst-matchp cst "command-auth") (iff (equal (imap-cst-command-auth-conc? cst) 1) (imap-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "append"))))
Theorem:
(defthm imap-cst-command-auth-conc?-2-iff-match-conc (implies (imap-cst-matchp cst "command-auth") (iff (equal (imap-cst-command-auth-conc? cst) 2) (imap-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "create"))))
Theorem:
(defthm imap-cst-command-auth-conc?-3-iff-match-conc (implies (imap-cst-matchp cst "command-auth") (iff (equal (imap-cst-command-auth-conc? cst) 3) (imap-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "delete"))))
Theorem:
(defthm imap-cst-command-auth-conc?-4-iff-match-conc (implies (imap-cst-matchp cst "command-auth") (iff (equal (imap-cst-command-auth-conc? cst) 4) (imap-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "examine"))))
Theorem:
(defthm imap-cst-command-auth-conc?-5-iff-match-conc (implies (imap-cst-matchp cst "command-auth") (iff (equal (imap-cst-command-auth-conc? cst) 5) (imap-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "list"))))
Theorem:
(defthm imap-cst-command-auth-conc?-6-iff-match-conc (implies (imap-cst-matchp cst "command-auth") (iff (equal (imap-cst-command-auth-conc? cst) 6) (imap-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "lsub"))))
Theorem:
(defthm imap-cst-command-auth-conc?-7-iff-match-conc (implies (imap-cst-matchp cst "command-auth") (iff (equal (imap-cst-command-auth-conc? cst) 7) (imap-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "rename"))))
Theorem:
(defthm imap-cst-command-auth-conc?-8-iff-match-conc (implies (imap-cst-matchp cst "command-auth") (iff (equal (imap-cst-command-auth-conc? cst) 8) (imap-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "select"))))
Theorem:
(defthm imap-cst-command-auth-conc?-9-iff-match-conc (implies (imap-cst-matchp cst "command-auth") (iff (equal (imap-cst-command-auth-conc? cst) 9) (imap-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "status"))))
Theorem:
(defthm imap-cst-command-auth-conc?-10-iff-match-conc (implies (imap-cst-matchp cst "command-auth") (iff (equal (imap-cst-command-auth-conc? cst) 10) (imap-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "subscribe"))))
Theorem:
(defthm imap-cst-command-auth-conc?-11-iff-match-conc (implies (imap-cst-matchp cst "command-auth") (iff (equal (imap-cst-command-auth-conc? cst) 11) (imap-cst-list-list-conc-matchp (tree-nonleaf->branches cst) "unsubscribe"))))