		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhsarr-to-svexarr

Signature
(lhsarr-to-svexarr n lhsarr svexarr) → svexarr
Arguments: n — Guard (natp n).

Definitions and Theorems

Function: lhsarr-to-svexarr

(defun lhsarr-to-svexarr (n lhsarr svexarr)
  (declare (xargs :stobjs (lhsarr svexarr)))
  (declare (xargs :guard (natp n)))
  (declare (xargs :guard (and (<= n (lhss-length lhsarr))
                              (<= (lhss-length lhsarr)
                                  (svexs-length svexarr)))))
  (let ((__function__ 'lhsarr-to-svexarr))
    (declare (ignorable __function__))
    (b* (((when (mbe :logic (zp (- (lhss-length lhsarr) (nfix n)))
                     :exec (eql n (lhss-length lhsarr))))
          (svexarr-fix svexarr))
         (lhs (get-lhs n lhsarr))
         (svex (lhs->svex lhs))
         (svexarr (set-svex n svex svexarr)))
      (lhsarr-to-svexarr (1+ (lnfix n))
                         lhsarr svexarr))))

Theorem: len-of-lhsarr-to-svexarr

(defthm len-of-lhsarr-to-svexarr
  (<= (len svexarr)
      (len (lhsarr-to-svexarr n lhsarr svexarr)))
  :rule-classes :linear)

Theorem: len-of-lhsarr-to-svexarr-equal

(defthm len-of-lhsarr-to-svexarr-equal
  (implies (<= (len lhsarr) (len svexarr))
           (equal (len (lhsarr-to-svexarr n lhsarr svexarr))
                  (len svexarr))))

Theorem: lhsarr-to-svexarr-of-nfix-n

(defthm lhsarr-to-svexarr-of-nfix-n
  (equal (lhsarr-to-svexarr (nfix n)
                            lhsarr svexarr)
         (lhsarr-to-svexarr n lhsarr svexarr)))

Theorem: lhsarr-to-svexarr-nat-equiv-congruence-on-n

(defthm lhsarr-to-svexarr-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (lhsarr-to-svexarr n lhsarr svexarr)
                  (lhsarr-to-svexarr n-equiv lhsarr svexarr)))
  :rule-classes :congruence)

Theorem: lhsarr-to-svexarr-of-lhslist-fix-lhsarr

(defthm lhsarr-to-svexarr-of-lhslist-fix-lhsarr
  (equal (lhsarr-to-svexarr n (lhslist-fix lhsarr)
                            svexarr)
         (lhsarr-to-svexarr n lhsarr svexarr)))

Theorem: lhsarr-to-svexarr-lhslist-equiv-congruence-on-lhsarr

(defthm lhsarr-to-svexarr-lhslist-equiv-congruence-on-lhsarr
  (implies (lhslist-equiv lhsarr lhsarr-equiv)
           (equal (lhsarr-to-svexarr n lhsarr svexarr)
                  (lhsarr-to-svexarr n lhsarr-equiv svexarr)))
  :rule-classes :congruence)

Theorem: lookup-in-lhsarr-to-svexarr

(defthm lookup-in-lhsarr-to-svexarr
  (svex-equiv (nth m (lhsarr-to-svexarr n lhsarr svexarr))
              (if (or (< (nfix m) (nfix n))
                      (<= (lhss-length lhsarr) (nfix m)))
                  (nth m svexarr)
                (lhs->svex (nth m lhsarr)))))