		Search-engine friendly clone of the ACL2 documentation.

Semantics

String-parsablep

Notion of parsable string.

A string is parsable iff it has at least one parse tree.

Definitions and Theorems

Theorem: string-parsablep-suff

(defthm string-parsablep-suff
  (implies (parse-treep tree string rulename rules)
           (string-parsablep string rulename rules)))

Theorem: booleanp-of-string-parsablep

(defthm booleanp-of-string-parsablep
  (b* ((yes/no (string-parsablep string rulename rules)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: string-parsablep-of-string-fix-string

(defthm string-parsablep-of-string-fix-string
  (equal (string-parsablep (string-fix string)
                           rulename rules)
         (string-parsablep string rulename rules)))

Theorem: string-parsablep-string-equiv-congruence-on-string

(defthm string-parsablep-string-equiv-congruence-on-string
  (implies (string-equiv string string-equiv)
           (equal (string-parsablep string rulename rules)
                  (string-parsablep string-equiv rulename rules)))
  :rule-classes :congruence)

Theorem: string-parsablep-of-rulename-fix-rulename

(defthm string-parsablep-of-rulename-fix-rulename
  (equal (string-parsablep string (rulename-fix rulename)
                           rules)
         (string-parsablep string rulename rules)))

Theorem: string-parsablep-rulename-equiv-congruence-on-rulename

(defthm string-parsablep-rulename-equiv-congruence-on-rulename
  (implies (rulename-equiv rulename rulename-equiv)
           (equal (string-parsablep string rulename rules)
                  (string-parsablep string rulename-equiv rules)))
  :rule-classes :congruence)

Theorem: string-parsablep-of-rulelist-fix-rules

(defthm string-parsablep-of-rulelist-fix-rules
  (equal (string-parsablep string rulename (rulelist-fix rules))
         (string-parsablep string rulename rules)))

Theorem: string-parsablep-rulelist-equiv-congruence-on-rules

(defthm string-parsablep-rulelist-equiv-congruence-on-rules
  (implies (rulelist-equiv rules rules-equiv)
           (equal (string-parsablep string rulename rules)
                  (string-parsablep string rulename rules-equiv)))
  :rule-classes :congruence)

Theorem: treep-of-string-parsablep-witness-when-string-parsablep

(defthm treep-of-string-parsablep-witness-when-string-parsablep
 (implies (string-parsablep string rulename rules)
          (treep (string-parsablep-witness string rulename rules))))

Theorem: not-parse-treep-when-not-string-parsablep

(defthm not-parse-treep-when-not-string-parsablep
  (implies (not (string-parsablep string rulename rules))
           (not (parse-treep tree string rulename rules))))

Theorem: parse-treep-of-string-parsablep-witness-when-string-parsablep

(defthm
      parse-treep-of-string-parsablep-witness-when-string-parsablep
  (implies
       (string-parsablep string rulename rules)
       (parse-treep (string-parsablep-witness string rulename rules)
                    string rulename rules)))