		Search-engine friendly clone of the ACL2 documentation.

Pnumber

Pnumber-count

Measure for recurring over pnumber structures.

Signature
(pnumber-count x) → count
Arguments: x — Guard (pnumberp x).
Returns: count — Type (natp count).

Definitions and Theorems

Function: pnumber-count

(defun pnumber-count (x)
 (declare (xargs :guard (pnumberp x)))
 (case (pnumber-kind x)
  (:digit 1)
  (:dot-digit 1)
  (:number-digit
       (+ 3
          (pnumber-count (pnumber-number-digit->number x))))
  (:number-nondigit
       (+ 3
          (pnumber-count (pnumber-number-nondigit->number x))))
  (:number-locase-e-sign
       (+ 3
          (pnumber-count (pnumber-number-locase-e-sign->number x))))
  (:number-upcase-e-sign
       (+ 3
          (pnumber-count (pnumber-number-upcase-e-sign->number x))))
  (:number-locase-p-sign
       (+ 3
          (pnumber-count (pnumber-number-locase-p-sign->number x))))
  (:number-upcase-p-sign
       (+ 3
          (pnumber-count (pnumber-number-upcase-p-sign->number x))))
  (:number-dot (+ 2
                  (pnumber-count (pnumber-number-dot->number x))))))

Theorem: natp-of-pnumber-count

(defthm natp-of-pnumber-count
  (b* ((count (pnumber-count x)))
    (natp count))
  :rule-classes :type-prescription)

Theorem: pnumber-count-of-pnumber-fix-x

(defthm pnumber-count-of-pnumber-fix-x
  (equal (pnumber-count (pnumber-fix x))
         (pnumber-count x)))

Theorem: pnumber-count-pnumber-equiv-congruence-on-x

(defthm pnumber-count-pnumber-equiv-congruence-on-x
  (implies (pnumber-equiv x x-equiv)
           (equal (pnumber-count x)
                  (pnumber-count x-equiv)))
  :rule-classes :congruence)

Theorem: pnumber-count-of-pnumber-number-digit

(defthm pnumber-count-of-pnumber-number-digit
  (implies (dec-digit-char-p digit)
           (< (+ (pnumber-count number))
              (pnumber-count (pnumber-number-digit number digit))))
  :rule-classes :linear)

Theorem: pnumber-count-of-pnumber-number-digit->number

(defthm pnumber-count-of-pnumber-number-digit->number
  (implies (equal (pnumber-kind x) :number-digit)
           (< (pnumber-count (pnumber-number-digit->number x))
              (pnumber-count x)))
  :rule-classes :linear)

Theorem: pnumber-count-of-pnumber-number-nondigit

(defthm pnumber-count-of-pnumber-number-nondigit
 (implies
      (str::letter/uscore-char-p nondigit)
      (< (+ (pnumber-count number))
         (pnumber-count (pnumber-number-nondigit number nondigit))))
 :rule-classes :linear)

Theorem: pnumber-count-of-pnumber-number-nondigit->number

(defthm pnumber-count-of-pnumber-number-nondigit->number
  (implies (equal (pnumber-kind x)
                  :number-nondigit)
           (< (pnumber-count (pnumber-number-nondigit->number x))
              (pnumber-count x)))
  :rule-classes :linear)

Theorem: pnumber-count-of-pnumber-number-locase-e-sign

(defthm pnumber-count-of-pnumber-number-locase-e-sign
 (implies
     t
     (< (+ (pnumber-count number))
        (pnumber-count (pnumber-number-locase-e-sign number sign))))
 :rule-classes :linear)

Theorem: pnumber-count-of-pnumber-number-locase-e-sign->number

(defthm pnumber-count-of-pnumber-number-locase-e-sign->number
  (implies
       (equal (pnumber-kind x)
              :number-locase-e-sign)
       (< (pnumber-count (pnumber-number-locase-e-sign->number x))
          (pnumber-count x)))
  :rule-classes :linear)

Theorem: pnumber-count-of-pnumber-number-upcase-e-sign

(defthm pnumber-count-of-pnumber-number-upcase-e-sign
 (implies
     t
     (< (+ (pnumber-count number))
        (pnumber-count (pnumber-number-upcase-e-sign number sign))))
 :rule-classes :linear)

Theorem: pnumber-count-of-pnumber-number-upcase-e-sign->number

(defthm pnumber-count-of-pnumber-number-upcase-e-sign->number
  (implies
       (equal (pnumber-kind x)
              :number-upcase-e-sign)
       (< (pnumber-count (pnumber-number-upcase-e-sign->number x))
          (pnumber-count x)))
  :rule-classes :linear)

Theorem: pnumber-count-of-pnumber-number-locase-p-sign

(defthm pnumber-count-of-pnumber-number-locase-p-sign
 (implies
     t
     (< (+ (pnumber-count number))
        (pnumber-count (pnumber-number-locase-p-sign number sign))))
 :rule-classes :linear)

Theorem: pnumber-count-of-pnumber-number-locase-p-sign->number

(defthm pnumber-count-of-pnumber-number-locase-p-sign->number
  (implies
       (equal (pnumber-kind x)
              :number-locase-p-sign)
       (< (pnumber-count (pnumber-number-locase-p-sign->number x))
          (pnumber-count x)))
  :rule-classes :linear)

Theorem: pnumber-count-of-pnumber-number-upcase-p-sign

(defthm pnumber-count-of-pnumber-number-upcase-p-sign
 (implies
     t
     (< (+ (pnumber-count number))
        (pnumber-count (pnumber-number-upcase-p-sign number sign))))
 :rule-classes :linear)

Theorem: pnumber-count-of-pnumber-number-upcase-p-sign->number

(defthm pnumber-count-of-pnumber-number-upcase-p-sign->number
  (implies
       (equal (pnumber-kind x)
              :number-upcase-p-sign)
       (< (pnumber-count (pnumber-number-upcase-p-sign->number x))
          (pnumber-count x)))
  :rule-classes :linear)

Theorem: pnumber-count-of-pnumber-number-dot

(defthm pnumber-count-of-pnumber-number-dot
  (implies t
           (< (+ (pnumber-count number))
              (pnumber-count (pnumber-number-dot number))))
  :rule-classes :linear)

Theorem: pnumber-count-of-pnumber-number-dot->number

(defthm pnumber-count-of-pnumber-number-dot->number
  (implies (equal (pnumber-kind x) :number-dot)
           (< (pnumber-count (pnumber-number-dot->number x))
              (pnumber-count x)))
  :rule-classes :linear)