		Search-engine friendly clone of the ACL2 documentation.

In-terminal-set

Nats-in-termset-when-match-sensitive-chars-in-termset

Lemma to prove leaves-in-termset-when-match-char-val-in-termset.

This is disabled by default because its conclusion is fairly general, not specific to terminal sets.

Definitions and Theorems

Theorem: nats-in-termset-when-match-sensitive-chars-in-termset

(defthm nats-in-termset-when-match-sensitive-chars-in-termset
  (implies (and (nat-listp nats)
                (nats-match-sensitive-chars-p nats chars)
                (chars-sensitive-in-termset-p chars termset))
           (list-in nats termset)))