		Search-engine friendly clone of the ACL2 documentation.

Uri-example

Uri-cst-ipv4address-conc

Signature
(uri-cst-ipv4address-conc cst) → cstss
Arguments: cst — Guard (treep cst).
Returns: cstss — Type (tree-list-listp cstss).

Definitions and Theorems

Function: uri-cst-ipv4address-conc

(defun uri-cst-ipv4address-conc (cst)
  (declare (xargs :guard (treep cst)))
  (declare (xargs :guard (uri-cst-matchp cst "ipv4address")))
  (let ((__function__ 'uri-cst-ipv4address-conc))
    (declare (ignorable __function__))
    (tree-nonleaf->branches cst)))

Theorem: tree-list-listp-of-uri-cst-ipv4address-conc

(defthm tree-list-listp-of-uri-cst-ipv4address-conc
  (b* ((cstss (uri-cst-ipv4address-conc cst)))
    (tree-list-listp cstss))
  :rule-classes :rewrite)

Theorem: uri-cst-ipv4address-conc-match

(defthm uri-cst-ipv4address-conc-match
 (implies
     (uri-cst-matchp cst "ipv4address")
     (b* ((cstss (uri-cst-ipv4address-conc cst)))
       (uri-cst-list-list-conc-matchp
            cstss
            "dec-octet \".\" dec-octet \".\" dec-octet \".\" dec-octet")))
 :rule-classes :rewrite)

Theorem: uri-cst-ipv4address-conc-of-tree-fix-cst

(defthm uri-cst-ipv4address-conc-of-tree-fix-cst
  (equal (uri-cst-ipv4address-conc (tree-fix cst))
         (uri-cst-ipv4address-conc cst)))

Theorem: uri-cst-ipv4address-conc-tree-equiv-congruence-on-cst

(defthm uri-cst-ipv4address-conc-tree-equiv-congruence-on-cst
  (implies (tree-equiv cst cst-equiv)
           (equal (uri-cst-ipv4address-conc cst)
                  (uri-cst-ipv4address-conc cst-equiv)))
  :rule-classes :congruence)