• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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-mod-ss-aux

    Signature
    (aabf-mod-ss-aux a b not-b man) → (mv m new-man)
    Arguments
    a — Guard (true-listp a).
    b — Guard (true-listp b).
    not-b — Guard (true-listp not-b).

    Definitions and Theorems

    Function: aabf-mod-ss-aux

    (defun aabf-mod-ss-aux (a b not-b man)
     (declare (xargs :guard (and (true-listp a)
                                 (true-listp b)
                                 (true-listp not-b))))
     (declare (xargs :guard (and (aabflist-p a man)
                                 (aabflist-p b man)
                                 (aabflist-p not-b man))))
     (let ((__function__ 'aabf-mod-ss-aux))
      (declare (ignorable __function__))
      (mbe
       :logic
       (b* (((mv & mod man)
             (aabf-floor-ss-aux a b not-b man)))
         (mv mod man))
       :exec
       (b*
         (((mv first rest endp)
           (aabf-first/rest/end a))
          ((when endp)
           (aabf-nest (aabf-ite-bss first
                                    (aabf-+-ss (aabf-false)
                                               (list (aabf-true))
                                               b)
                                    nil)
                      man))
          (bound (aabf-integer-length-bound-s b man))
          ((mv rm man)
           (aabf-nest (aabf-scons first (aabf-mod-ss-aux rest b not-b))
                      man)))
        (aabf-nest
          (aabf-ite-bss
               (aabf-<-ss rm b)
               rm
               (aabf-loghead-ns bound (aabf-+-ss (aabf-true) not-b rm)))
          man)))))

    Theorem: trivial-theorem-about-aabf-mod-ss-aux

    (defthm trivial-theorem-about-aabf-mod-ss-aux
      (b* nil
        (b* ((?ignore (aabf-mod-ss-aux a b not-b man)))
          t))
      :rule-classes nil)

    Theorem: true-listp-of-aabf-mod-ss-aux.m

    (defthm true-listp-of-aabf-mod-ss-aux.m
      (b* (((mv acl2::?m ?new-man)
            (aabf-mod-ss-aux a b not-b man)))
        (true-listp m))
      :rule-classes :type-prescription)

    Theorem: aabf-extension-p-of-aabf-mod-ss-aux

    (defthm aabf-extension-p-of-aabf-mod-ss-aux
      (b* (((mv acl2::?m ?new-man)
            (aabf-mod-ss-aux a b not-b man)))
        (aabf-extension-p new-man man)))

    Theorem: aabf-p-of-aabf-mod-ss-aux

    (defthm aabf-p-of-aabf-mod-ss-aux
      (b* (((mv m new-man)
            (aabf-mod-ss-aux a b not-b man)))
        (implies (and (aabflist-p a man)
                      (aabflist-p b man)
                      (aabflist-p not-b man))
                 (and (aabflist-p m new-man)))))

    Theorem: aabf-eval-of-aabf-mod-ss-aux

    (defthm aabf-eval-of-aabf-mod-ss-aux
     (b* (((mv m new-man)
           (aabf-mod-ss-aux a b not-b man)))
      (implies
       (and
          (aabflist-p a man)
          (aabflist-p b man)
          (aabflist-p not-b man)
          (and (< 0
                  (bools->int (aabflist-eval b env man)))
               (equal (bools->int (aabflist-eval not-b env man))
                      (lognot (bools->int (aabflist-eval b env man))))))
       (and (equal (bools->int (aabflist-eval m env new-man))
                   (mod (bools->int (aabflist-eval a env man))
                        (bools->int (aabflist-eval b env man))))))))

    Theorem: aabf-pred-of-aabf-mod-ss-aux

    (defthm aabf-pred-of-aabf-mod-ss-aux
      (b* (((mv m new-man)
            (aabf-mod-ss-aux a b not-b man)))
        (implies (and (aabflist-p a man)
                      (aabflist-p b man)
                      (aabflist-p not-b man)
                      (aabflist-pred a man)
                      (aabflist-pred b man)
                      (aabflist-pred not-b man))
                 (and (aabflist-pred m new-man)))))