• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
        • Alias-normalization
          • Alias-norm.lisp
            • Lhs-alias-canonicalize-replace-top
            • Aliases-bound-fix
            • Lhs-pairs-set-aliases
            • Setalias
            • Lhs-replace-range
            • Lhatom-bound-fix
            • Constraintlist-subst-from-svexarr
            • Aliases-add-pair
            • Lhs-alias-canonicalize-top
            • Lhs-varbound-fix
            • Aliases-bound-fix-aux
            • Canonicalize-alias-pairs
            • Aliases-finish-canonicalize
            • Assigns-subst
            • Aliases-put-pairs
            • Getalias
            • Lhs-alias-norm
            • Constraintlist-subst-from-svexarr-nrev
            • Assigns-subst-nrev
            • Svex-subst-from-svexarr-memo-ok
            • Collect-aliases
            • Aliases-fix
            • Aliases-empty
        • Svex-design-flatten-and-normalize
        • Svex-design-compile
        • Svex-composition
        • Compile.lisp
        • Assign->segment-drivers
        • Segment-driver-map-resolve
        • Assigns->segment-drivers
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Alias-norm.lisp

Lhs-replace-range

Signature

(lhs-replace-range start w repl x) → newx

Arguments

start — Guard (natp start).

w — Guard (natp w).

repl — Guard (lhs-p repl).

x — Guard (lhs-p x).

Returns

newx — Type (lhs-p newx).

Definitions and Theorems

Function: lhs-replace-range

(defun lhs-replace-range (start w repl x)
  (declare (xargs :guard (and (natp start)
                              (natp w)
                              (lhs-p repl)
                              (lhs-p x))))
  (let ((__function__ 'lhs-replace-range))
    (declare (ignorable __function__))
    (lhs-concat start x
                (lhs-concat w repl
                            (lhs-rsh (+ (lnfix start) (lnfix w))
                                     x)))))

Theorem: lhs-p-of-lhs-replace-range

(defthm lhs-p-of-lhs-replace-range
  (b* ((newx (lhs-replace-range start w repl x)))
    (lhs-p newx))
  :rule-classes :rewrite)

Theorem: lhs-replace-range-of-nfix-start

(defthm lhs-replace-range-of-nfix-start
  (equal (lhs-replace-range (nfix start)
                            w repl x)
         (lhs-replace-range start w repl x)))

Theorem: lhs-replace-range-nat-equiv-congruence-on-start

(defthm lhs-replace-range-nat-equiv-congruence-on-start
  (implies (nat-equiv start start-equiv)
           (equal (lhs-replace-range start w repl x)
                  (lhs-replace-range start-equiv w repl x)))
  :rule-classes :congruence)

Theorem: lhs-replace-range-of-nfix-w

(defthm lhs-replace-range-of-nfix-w
  (equal (lhs-replace-range start (nfix w)
                            repl x)
         (lhs-replace-range start w repl x)))

Theorem: lhs-replace-range-nat-equiv-congruence-on-w

(defthm lhs-replace-range-nat-equiv-congruence-on-w
  (implies (nat-equiv w w-equiv)
           (equal (lhs-replace-range start w repl x)
                  (lhs-replace-range start w-equiv repl x)))
  :rule-classes :congruence)

Theorem: lhs-replace-range-of-lhs-fix-repl

(defthm lhs-replace-range-of-lhs-fix-repl
  (equal (lhs-replace-range start w (lhs-fix repl)
                            x)
         (lhs-replace-range start w repl x)))

Theorem: lhs-replace-range-lhs-equiv-congruence-on-repl

(defthm lhs-replace-range-lhs-equiv-congruence-on-repl
  (implies (lhs-equiv repl repl-equiv)
           (equal (lhs-replace-range start w repl x)
                  (lhs-replace-range start w repl-equiv x)))
  :rule-classes :congruence)

Theorem: lhs-replace-range-of-lhs-fix-x

(defthm lhs-replace-range-of-lhs-fix-x
  (equal (lhs-replace-range start w repl (lhs-fix x))
         (lhs-replace-range start w repl x)))

Theorem: lhs-replace-range-lhs-equiv-congruence-on-x

(defthm lhs-replace-range-lhs-equiv-congruence-on-x
  (implies (lhs-equiv x x-equiv)
           (equal (lhs-replace-range start w repl x)
                  (lhs-replace-range start w repl x-equiv)))
  :rule-classes :congruence)

Theorem: lhs-vars-normorderedp-of-lhs-replace-range

(defthm lhs-vars-normorderedp-of-lhs-replace-range
 (implies
      (and (lhs-vars-normorderedp n m x)
           (lhs-vars-normorderedp n (+ (nfix m) (nfix start))
                                  repl))
      (lhs-vars-normorderedp n
                             m (lhs-replace-range start w repl x))))