		Search-engine friendly clone of the ACL2 documentation.

Semantics

Nats-match-sensitive-chars-p

Lifting of nat-match-sensitive-char-p to lists.

Signature
(nats-match-sensitive-chars-p nats chars) → yes/no
Arguments: nats — Guard (nat-listp nats).; chars — Guard (character-listp chars).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: nats-match-sensitive-chars-p

(defun nats-match-sensitive-chars-p (nats chars)
  (declare (xargs :guard (and (nat-listp nats)
                              (character-listp chars))))
  (cond ((endp nats) (endp chars))
        (t (and (consp chars)
                (nat-match-sensitive-char-p (car nats)
                                            (car chars))
                (nats-match-sensitive-chars-p (cdr nats)
                                              (cdr chars))))))

Theorem: booleanp-of-nats-match-sensitive-chars-p

(defthm booleanp-of-nats-match-sensitive-chars-p
  (b* ((yes/no (nats-match-sensitive-chars-p nats chars)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: nats-match-sensitive-chars-p-when-atom-chars

(defthm nats-match-sensitive-chars-p-when-atom-chars
  (implies (atom chars)
           (equal (nats-match-sensitive-chars-p nats chars)
                  (not (consp nats)))))

Theorem: nats-match-sensitive-chars-p-of-cons-chars

(defthm nats-match-sensitive-chars-p-of-cons-chars
  (equal (nats-match-sensitive-chars-p nats (cons char chars))
         (and (consp nats)
              (nat-match-sensitive-char-p (car nats)
                                          char)
              (nats-match-sensitive-chars-p (cdr nats)
                                            chars))))

Theorem: nats-match-sensitive-chars-p-of-nat-list-fix-nats

(defthm nats-match-sensitive-chars-p-of-nat-list-fix-nats
  (equal (nats-match-sensitive-chars-p (nat-list-fix nats)
                                       chars)
         (nats-match-sensitive-chars-p nats chars)))

Theorem: nats-match-sensitive-chars-p-nat-list-equiv-congruence-on-nats

(defthm
     nats-match-sensitive-chars-p-nat-list-equiv-congruence-on-nats
  (implies (acl2::nat-list-equiv nats nats-equiv)
           (equal (nats-match-sensitive-chars-p nats chars)
                  (nats-match-sensitive-chars-p nats-equiv chars)))
  :rule-classes :congruence)

Theorem: nats-match-sensitive-chars-p-of-make-character-list-chars

(defthm nats-match-sensitive-chars-p-of-make-character-list-chars
 (equal
     (nats-match-sensitive-chars-p nats (make-character-list chars))
     (nats-match-sensitive-chars-p nats chars)))

Theorem: nats-match-sensitive-chars-p-charlisteqv-congruence-on-chars

(defthm nats-match-sensitive-chars-p-charlisteqv-congruence-on-chars
  (implies (str::charlisteqv chars chars-equiv)
           (equal (nats-match-sensitive-chars-p nats chars)
                  (nats-match-sensitive-chars-p nats chars-equiv)))
  :rule-classes :congruence)