• 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-loghead-nu

Signature

(bfr-loghead-nu n a) → head

Arguments

n — Guard (natp n).

a — Guard (true-listp a).

Returns

head — Type (true-listp head).

Definitions and Theorems

Function: bfr-loghead-nu

(defun bfr-loghead-nu (n a)
  (declare (xargs :guard (and (natp n) (true-listp a))))
  (let ((__function__ 'bfr-loghead-nu))
    (declare (ignorable __function__))
    (b* (((when (or (zp n) (atom a))) '(nil))
         ((mv first rest) (car/cdr a)))
      (bfr-scons first (bfr-loghead-nu (1- n) rest)))))

Theorem: true-listp-of-bfr-loghead-nu

(defthm true-listp-of-bfr-loghead-nu
  (b* ((head (bfr-loghead-nu n a)))
    (true-listp head))
  :rule-classes :type-prescription)

Theorem: bfr-loghead-nu-correct

(defthm bfr-loghead-nu-correct
  (b* ((head (bfr-loghead-nu n a)))
    (and (equal (bfr-list->s head env)
                (loghead (nfix n)
                         (bfr-list->u a env))))))

Theorem: bfr-loghead-nu-deps

(defthm bfr-loghead-nu-deps
 (b* ((head (bfr-loghead-nu n a)))
   (implies (and (not (pbfr-list-depends-on varname param a)))
            (and (not (pbfr-list-depends-on varname param head))))))