		Search-engine friendly clone of the ACL2 documentation.

Uri-example

Uri-cst-list-elem-matchp$

Signature
(uri-cst-list-elem-matchp$ trees elem) → yes/no
Arguments: trees — Guard (tree-listp trees).; elem — Guard (elementp elem).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: uri-cst-list-elem-matchp$

(defun uri-cst-list-elem-matchp$ (trees elem)
 (declare (xargs :guard (and (tree-listp trees)
                             (elementp elem))))
 (let ((__function__ 'uri-cst-list-elem-matchp$))
  (declare (ignorable __function__))
  (and
   (tree-list-terminatedp trees)
   (tree-list-match-element-p trees elem *all-uri-grammar-rules*))))

Theorem: booleanp-of-uri-cst-list-elem-matchp$

(defthm booleanp-of-uri-cst-list-elem-matchp$
  (b* ((yes/no (uri-cst-list-elem-matchp$ trees elem)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: uri-cst-list-elem-matchp$-of-tree-list-fix-trees

(defthm uri-cst-list-elem-matchp$-of-tree-list-fix-trees
  (equal (uri-cst-list-elem-matchp$ (tree-list-fix trees)
                                    elem)
         (uri-cst-list-elem-matchp$ trees elem)))

Theorem: uri-cst-list-elem-matchp$-tree-list-equiv-congruence-on-trees

(defthm
      uri-cst-list-elem-matchp$-tree-list-equiv-congruence-on-trees
  (implies (tree-list-equiv trees trees-equiv)
           (equal (uri-cst-list-elem-matchp$ trees elem)
                  (uri-cst-list-elem-matchp$ trees-equiv elem)))
  :rule-classes :congruence)

Theorem: uri-cst-list-elem-matchp$-of-element-fix-elem

(defthm uri-cst-list-elem-matchp$-of-element-fix-elem
  (equal (uri-cst-list-elem-matchp$ trees (element-fix elem))
         (uri-cst-list-elem-matchp$ trees elem)))

Theorem: uri-cst-list-elem-matchp$-element-equiv-congruence-on-elem

(defthm uri-cst-list-elem-matchp$-element-equiv-congruence-on-elem
  (implies (element-equiv elem elem-equiv)
           (equal (uri-cst-list-elem-matchp$ trees elem)
                  (uri-cst-list-elem-matchp$ trees elem-equiv)))
  :rule-classes :congruence)