• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
        • Decomp.lisp
          • Svex-env-compat-union
          • Svdecomp-symenv-compat-union
          • Svexlists-rewrite-until-same
          • Svdecomp-normalize-svexlist-eval
          • Svex-decomp-process-env-term
          • Map-alist-term-keys-to-val-terms
          • Envmap-extract-union-env
          • Alist-collect-compositions
          • Envmap-entry-extract-env
          • Svdecomp-env-extract
          • Svex-alist-evaluation-to-symenv
          • Envmap-entry-to-term-alist
          • Svar-lookup
          • Svar-alist-keys
          • Map-alist-const-keys-to-val-terms
          • Svdecomp-svex?-eval-compare-term
          • Svdecomp-equal-svex-evals-metafun
          • Svdecomp-equal-svex-alist-evals-metafun
          • Envmap->svex-alist
          • Envmap-to-term-alist
          • Svdecomp-equal-svexlist-evals-metafun
          • Pseudo-term-fix
          • Svdecomp-symenv->term
          • Svdecomp-svex-alist-eval-metafun
          • Svdecomp-ev-symenv
          • Svdecomp-svexlist-eval-metafun
          • Svdecomp-svex-eval-metafun
          • Svdecomp-ev-envmap
          • Envmap
          • Svex-alist-alist
          • Svdecomp-symenv
          • Svdecomp-get-rewrite-limit
        • Svdecomp-hints
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Decomp.lisp

Svar-alist-keys

Signature

(svar-alist-keys x) → vars

Arguments

x — Guard (svar-alist-p x).

Returns

vars — Type (svarlist-p vars).

Definitions and Theorems

Function: svar-alist-keys

(defun svar-alist-keys (x)
  (declare (xargs :guard (svar-alist-p x)))
  (let ((__function__ 'svar-alist-keys))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (if (mbt (and (consp (car x)) (svar-p (caar x))))
          (cons (caar x)
                (svar-alist-keys (cdr x)))
        (svar-alist-keys (cdr x))))))

Theorem: svarlist-p-of-svar-alist-keys

(defthm svarlist-p-of-svar-alist-keys
  (b* ((vars (svar-alist-keys x)))
    (svarlist-p vars))
  :rule-classes :rewrite)

Theorem: svar-alist-keys-of-append

(defthm svar-alist-keys-of-append
  (equal (svar-alist-keys (append a b))
         (append (svar-alist-keys a)
                 (svar-alist-keys b))))

Theorem: svar-alist-keys-of-svex-env-fix-x

(defthm svar-alist-keys-of-svex-env-fix-x
  (equal (svar-alist-keys (svex-env-fix x))
         (svar-alist-keys x)))

Theorem: svar-alist-keys-svex-env-equiv-congruence-on-x

(defthm svar-alist-keys-svex-env-equiv-congruence-on-x
  (implies (svex-env-equiv x x-equiv)
           (equal (svar-alist-keys x)
                  (svar-alist-keys x-equiv)))
  :rule-classes :congruence)

Theorem: svar-alist-keys-of-svex-alist-fix-x

(defthm svar-alist-keys-of-svex-alist-fix-x
  (equal (svar-alist-keys (svex-alist-fix x))
         (svar-alist-keys x)))

Theorem: svar-alist-keys-svex-alist-equiv-congruence-on-x

(defthm svar-alist-keys-svex-alist-equiv-congruence-on-x
  (implies (svex-alist-equiv x x-equiv)
           (equal (svar-alist-keys x)
                  (svar-alist-keys x-equiv)))
  :rule-classes :congruence)

Theorem: svar-alist-keys-of-true-list-fix

(defthm svar-alist-keys-of-true-list-fix
  (equal (svar-alist-keys (true-list-fix x))
         (svar-alist-keys x)))

Theorem: svar-alist-keys-of-svar-alist-fix-x

(defthm svar-alist-keys-of-svar-alist-fix-x
  (equal (svar-alist-keys (svar-alist-fix x))
         (svar-alist-keys x)))

Theorem: svar-alist-keys-svar-alist-equiv-congruence-on-x

(defthm svar-alist-keys-svar-alist-equiv-congruence-on-x
  (implies (svar-alist-equiv x x-equiv)
           (equal (svar-alist-keys x)
                  (svar-alist-keys x-equiv)))
  :rule-classes :congruence)