• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
    • Gl
    • Witness-cp
    • Ccg
    • Install-not-normalized
    • Rewrite$
    • Fgl
      • Fgl-rewrite-rules
      • Fgl-function-mode
      • Fgl-object
      • Fgl-solving
      • Fgl-handling-if-then-elses
      • Fgl-getting-bits-from-objects
      • Fgl-primitive-and-meta-rules
      • Fgl-counterexamples
      • Fgl-interpreter-overview
      • Fgl-correctness-of-binding-free-variables
      • Fgl-debugging
      • Fgl-testbenches
      • Def-fgl-boolean-constraint
      • Fgl-stack
      • Fgl-rewrite-tracing
      • Def-fgl-param-thm
      • Def-fgl-thm
      • Fgl-fast-alist-support
      • Fgl-array-support
      • Advanced-equivalence-checking-with-fgl
      • Fgl-fty-support
      • Fgl-internals
        • Symbolic-arithmetic
          • Aabf-floor-ss-aux
          • Aabf-logapp-russ
          • Aabf-integer-length-s1
          • Aabf-mod-ss-aux
          • Aabf-ite-bss-fn-aux
          • Aabf-sign-abs-not-s
          • Aabf-ite-buu-fn-aux
          • Aabf-ash-ss
          • Aabf-<-=-ss
          • Aabf-+-ss
          • Aabf-truncate-ss
          • Aabf-rem-ss
          • Aabf-mod-ss
          • Aabf-logbitp-n2v
          • Aabf-ite-buu-fn
          • Aabf-ite-bss-fn
          • Aabf-expt-su
          • Aabf-*-ss
          • Aabf-logxor-ss
          • Aabf-logior-ss
          • Aabf-logeqv-ss
          • Aabf-logand-ss
          • Aabf-floor-ss
          • Aabf-logapp-nss-aux
          • Aabf-unary-minus-s
          • Aabf-signext-nss
          • Aabf-logapp-nss
          • Aabf-integer-length-s
          • Aabf-=-ss
          • Aabf-<-ss
          • Aabf-abs-s
          • Aabf-syntactically-zero-p
          • Aabf-scons
          • Aabf-logtail-ns
          • Aabf-loghead-ns
          • Aabf-logext-ns
          • Aabf-syntactically-false-p
          • Aabf-lognot-s
          • Int->aabflist
          • Aabf-ucons
          • Aabf-syntactically-true-p
          • Aabf-syntactically-signext-p
          • Aabf-syntactically-neg1-p
          • Aabf-sign-s
          • Aabf-integer-length-bound-s
          • Int-set-sign
          • Aabf-car
          • Aabf-first/rest/end
          • Non-int-fix
          • Maybe-integer
        • Bfr
        • Fgl-interpreter-state
    • Removable-runes
    • 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

Aabf-logapp-nss

Signature

(aabf-logapp-nss n a b) → a-app-b

Arguments

n — Guard (natp n).

a — Guard (true-listp a).

b — Guard (true-listp b).

Definitions and Theorems

Function: aabf-logapp-nss

(defun aabf-logapp-nss (n a b)
  (declare (xargs :guard (and (natp n)
                              (true-listp a)
                              (true-listp b))))
  (declare (xargs :guard (and)))
  (let ((__function__ 'aabf-logapp-nss))
    (declare (ignorable __function__))
    (b* ((b1 (aabf-car b))
         ((when (aabf-syntactically-signext-p (scdr b)
                                              b1))
          (aabf-signext-nss n a b1)))
      (aabf-logapp-nss-aux n a b))))

Theorem: trivial-theorem-about-aabf-logapp-nss

(defthm trivial-theorem-about-aabf-logapp-nss
  (b* nil
    (b* ((?ignore (aabf-logapp-nss n a b)))
      t))
  :rule-classes nil)

Theorem: true-listp-of-aabf-logapp-nss.a-app-b

(defthm true-listp-of-aabf-logapp-nss.a-app-b
  (b* ((?a-app-b (aabf-logapp-nss n a b)))
    (true-listp a-app-b))
  :rule-classes :type-prescription)

Theorem: aabf-p-of-aabf-logapp-nss

(defthm aabf-p-of-aabf-logapp-nss
  (b* ((a-app-b (aabf-logapp-nss n a b)))
    (implies (and (aabflist-p a man)
                  (aabflist-p b man))
             (and (aabflist-p a-app-b man)))))

Theorem: aabf-eval-of-aabf-logapp-nss

(defthm aabf-eval-of-aabf-logapp-nss
 (b* ((a-app-b (aabf-logapp-nss n a b)))
  (implies
    (and (aabflist-p a man)
         (aabflist-p b man))
    (and (equal (bools->int (aabflist-eval a-app-b env man))
                (logapp (nfix n)
                        (bools->int (aabflist-eval a env man))
                        (bools->int (aabflist-eval b env man))))))))

Theorem: aabf-pred-of-aabf-logapp-nss

(defthm aabf-pred-of-aabf-logapp-nss
  (b* ((a-app-b (aabf-logapp-nss n a b)))
    (implies (and (aabflist-p a man)
                  (aabflist-p b man)
                  (aabflist-pred a man)
                  (aabflist-pred b man))
             (and (aabflist-pred a-app-b man)))))