		Search-engine friendly clone of the ACL2 documentation.

Http-example

Http-cst-uri-host-conc1

Signature
(http-cst-uri-host-conc1 cst) → cstss
Arguments: cst — Guard (treep cst).
Returns: cstss — Type (tree-list-listp cstss).

Definitions and Theorems

Function: http-cst-uri-host-conc1

(defun http-cst-uri-host-conc1 (cst)
  (declare (xargs :guard (treep cst)))
  (declare (xargs :guard (and (http-cst-matchp cst "uri-host")
                              (equal (http-cst-uri-host-conc? cst)
                                     1))))
  (let ((__function__ 'http-cst-uri-host-conc1))
    (declare (ignorable __function__))
    (tree-nonleaf->branches cst)))

Theorem: tree-list-listp-of-http-cst-uri-host-conc1

(defthm tree-list-listp-of-http-cst-uri-host-conc1
  (b* ((cstss (http-cst-uri-host-conc1 cst)))
    (tree-list-listp cstss))
  :rule-classes :rewrite)

Theorem: http-cst-uri-host-conc1-match

(defthm http-cst-uri-host-conc1-match
  (implies (and (http-cst-matchp cst "uri-host")
                (equal (http-cst-uri-host-conc? cst) 1))
           (b* ((cstss (http-cst-uri-host-conc1 cst)))
             (http-cst-list-list-conc-matchp cstss "ip-literal")))
  :rule-classes :rewrite)

Theorem: http-cst-uri-host-conc1-of-tree-fix-cst

(defthm http-cst-uri-host-conc1-of-tree-fix-cst
  (equal (http-cst-uri-host-conc1 (tree-fix cst))
         (http-cst-uri-host-conc1 cst)))

Theorem: http-cst-uri-host-conc1-tree-equiv-congruence-on-cst

(defthm http-cst-uri-host-conc1-tree-equiv-congruence-on-cst
  (implies (tree-equiv cst cst-equiv)
           (equal (http-cst-uri-host-conc1 cst)
                  (http-cst-uri-host-conc1 cst-equiv)))
  :rule-classes :congruence)