• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
    • Gl
      • Term-level-reasoning
      • Glmc
      • Other-resources
      • Optimization
      • Reference
        • Def-gl-thm
        • Shape-specs
        • Symbolic-objects
        • Gl-aside
        • Def-gl-param-thm
        • Symbolic-arithmetic
          • Bfr-floor-ss-aux
          • Bfr-integer-length-s1
          • Bfr-mod-ss-aux
          • Bfr-logapp-russ
          • Bfr-sign-abs-not-s
          • Bfr-ash-ss
          • Bfr-+-ss
          • Bfr-truncate-ss
          • Bfr-logapp-nus-aux
          • Bfr-ite-bss-fn-aux
          • Bfr-rem-ss
          • Bfr-mod-ss
          • Bfr-logbitp-n2v
          • Bfr-logapp-nus
          • Bfr-logapp-nss
          • Bfr-ite-bvv-fn-aux
          • Bfr-<-=-ss
          • Bfr-*-ss
          • Bfr-logxor-ss
          • Bfr-logior-ss
          • Bfr-logeqv-ss
          • Bfr-logand-ss
          • Bfr-ite-bvv-fn
          • Bfr-ite-bss-fn
          • Bfr-floor-ss
          • Bfr-expt-su
          • Bfr-logtail-ns
          • Bfr-loghead-nu
          • Bfr-loghead-ns
          • Bfr-logext-ns
          • Bfr-integer-length-s
          • Syntactically-true-p
          • Int-set-sign
          • Bfr-unary-minus-s
          • Bfr-lognot-s
          • Bfr-=-ss
          • Bfr-<-ss
          • Bfr-abs-s
          • Syntactically-zero-p
          • Bfr-=-uu
          • S-take
          • Integer-length-bound-s
          • Bfr-sign-s
          • Non-int-fix
          • Maybe-integer
          • All-nil
        • Bfr
        • Def-gl-boolean-constraint
        • Gl-mbe
        • Bvec
        • Flex-bindings
        • Auto-bindings
        • Gl-interp
        • Gl-set-uninterpreted
        • Def-gl-clause-processor
        • Def-glcp-ctrex-rewrite
        • ACL2::always-equal
        • Gl-hint
        • Def-gl-rewrite
        • Def-gl-branch-merge
        • Gl-force-check
        • Gl-concretize
        • Gl-assert
        • Gl-param-thm
        • Gl-simplify-satlink-mode
        • Gl-satlink-mode
        • Gl-bdd-mode
        • Gl-aig-bddify-mode
        • Gl-fraig-satlink-mode
      • Debugging
      • Basic-tutorial
    • Witness-cp
    • Ccg
    • Install-not-normalized
    • Rewrite$
    • Removable-runes
    • Fgl
    • Efficiency
    • Rewrite-bounds
    • Bash
    • Def-dag-measure
    • Bdd
    • Remove-hyps
    • Contextual-rewriting
    • Simp
    • Rewrite$-hyps
    • Bash-term-to-dnf
    • Use-trivial-ancestors-check
    • Minimal-runes
    • Clause-processor-tools
    • Fn-is-body
    • Without-subsumption
    • Rewrite-equiv-hint
    • Def-bounds
    • Rewrite$-context
    • Try-gl-concls
    • Hint-utils
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Symbolic-arithmetic

Bfr-unary-minus-s

Signature

(bfr-unary-minus-s x) → ms

Arguments

x — Guard (true-listp x).

Returns

ms — Type (true-listp ms).

Definitions and Theorems

Function: bfr-unary-minus-s

(defun bfr-unary-minus-s (x)
  (declare (xargs :guard (true-listp x)))
  (let ((__function__ 'bfr-unary-minus-s))
    (declare (ignorable __function__))
    (bfr-+-ss t nil (bfr-lognot-s x))))

Theorem: true-listp-of-bfr-unary-minus-s

(defthm true-listp-of-bfr-unary-minus-s
  (b* ((ms (bfr-unary-minus-s x)))
    (true-listp ms))
  :rule-classes :type-prescription)

Theorem: bfr-unary-minus-s-correct

(defthm bfr-unary-minus-s-correct
  (b* ((ms (bfr-unary-minus-s x)))
    (and (equal (bfr-list->s ms env)
                (- (bfr-list->s x env))))))

Theorem: bfr-unary-minus-s-deps

(defthm bfr-unary-minus-s-deps
  (b* ((ms (bfr-unary-minus-s x)))
    (implies (and (not (pbfr-list-depends-on varname param x)))
             (and (not (pbfr-list-depends-on varname param ms))))))