		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhatom-normorderedp

Signature
(lhatom-normorderedp bound offset x) → *
Arguments: bound — Guard (integerp bound).; offset — Guard (natp offset).; x — Guard (lhatom-p x).

Definitions and Theorems

Function: lhatom-normorderedp

(defun lhatom-normorderedp (bound offset x)
  (declare (xargs :guard (and (integerp bound)
                              (natp offset)
                              (lhatom-p x))))
  (let ((__function__ 'lhatom-normorderedp))
    (declare (ignorable __function__))
    (or (eq (lhatom-kind x) :z)
        (and (svar-indexedp (lhatom-var->name x))
             (let ((idx (svar-index (lhatom-var->name x))))
               (or (< idx (lifix bound))
                   (and (eql idx (lifix bound))
                        (<= (lhatom-var->rsh x)
                            (lnfix offset)))))))))

Theorem: lhatom-normorderedp-of-ifix-bound

(defthm lhatom-normorderedp-of-ifix-bound
  (equal (lhatom-normorderedp (ifix bound)
                              offset x)
         (lhatom-normorderedp bound offset x)))

Theorem: lhatom-normorderedp-int-equiv-congruence-on-bound

(defthm lhatom-normorderedp-int-equiv-congruence-on-bound
  (implies (int-equiv bound bound-equiv)
           (equal (lhatom-normorderedp bound offset x)
                  (lhatom-normorderedp bound-equiv offset x)))
  :rule-classes :congruence)

Theorem: lhatom-normorderedp-of-nfix-offset

(defthm lhatom-normorderedp-of-nfix-offset
  (equal (lhatom-normorderedp bound (nfix offset)
                              x)
         (lhatom-normorderedp bound offset x)))

Theorem: lhatom-normorderedp-nat-equiv-congruence-on-offset

(defthm lhatom-normorderedp-nat-equiv-congruence-on-offset
  (implies (nat-equiv offset offset-equiv)
           (equal (lhatom-normorderedp bound offset x)
                  (lhatom-normorderedp bound offset-equiv x)))
  :rule-classes :congruence)

Theorem: lhatom-normorderedp-of-lhatom-fix-x

(defthm lhatom-normorderedp-of-lhatom-fix-x
  (equal (lhatom-normorderedp bound offset (lhatom-fix x))
         (lhatom-normorderedp bound offset x)))

Theorem: lhatom-normorderedp-lhatom-equiv-congruence-on-x

(defthm lhatom-normorderedp-lhatom-equiv-congruence-on-x
  (implies (lhatom-equiv x x-equiv)
           (equal (lhatom-normorderedp bound offset x)
                  (lhatom-normorderedp bound offset x-equiv)))
  :rule-classes :congruence)

Theorem: lhatom-normorderedp-implies-index

(defthm lhatom-normorderedp-implies-index
  (implies (and (lhatom-normorderedp bound offset x)
                (equal (lhatom-kind x) :var))
           (svar-index (lhatom-var->name x)))
  :rule-classes (:rewrite :type-prescription))

Theorem: lhatom-normorderedp-implies-index-bound

(defthm lhatom-normorderedp-implies-index-bound
  (implies (and (lhatom-normorderedp bound offset x)
                (equal (lhatom-kind x) :var))
           (<= (svar-index (lhatom-var->name x))
               (ifix bound)))
  :rule-classes :linear)

Theorem: lhatom-normorderedp-implies-rsh-when-at-bound

(defthm lhatom-normorderedp-implies-rsh-when-at-bound
  (implies (and (lhatom-normorderedp bound offset x)
                (equal (lhatom-kind x) :var)
                (equal (svar-index (lhatom-var->name x))
                       (ifix bound)))
           (<= (lhatom-var->rsh x) (nfix offset)))
  :rule-classes :linear)

Theorem: lhatom-normorderedp-of-greater

(defthm lhatom-normorderedp-of-greater
  (implies (and (lhatom-normorderedp bound1 offset1 x)
                (<= (ifix bound1) (ifix bound))
                (<= (nfix offset1) (nfix offset)))
           (lhatom-normorderedp bound offset x)))

Theorem: lhatom-normorderedp-of-greater-bound

(defthm lhatom-normorderedp-of-greater-bound
  (implies (and (lhatom-normorderedp bound1 offset1 x)
                (< (ifix bound1) (ifix bound)))
           (lhatom-normorderedp bound offset x)))

Theorem: lhatom-normorderedp-of-z

(defthm lhatom-normorderedp-of-z
  (lhatom-normorderedp bound offset :z))

Theorem: lhatom-normorderedp-implies-svarlist-bounded

(defthm lhatom-normorderedp-implies-svarlist-bounded
  (implies (lhatom-normorderedp bound offset x)
           (svarlist-boundedp (lhatom-vars x)
                              (+ 1 (ifix bound)))))

Theorem: lhatom-normorderedp-implies-svar-indexedp

(defthm lhatom-normorderedp-implies-svar-indexedp
  (implies (and (lhatom-normorderedp idx offset x)
                (equal (lhatom-kind x) :var))
           (svar-indexedp (lhatom-var->name x)))
  :rule-classes :forward-chaining)