• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
      • Defun
      • Declare
      • System-utilities
      • Stobj
      • State
      • Mutual-recursion
      • Memoize
      • Mbe
      • Io
      • Defpkg
      • Apply$
      • Loop$
      • Programming-with-state
      • Arrays
      • Characters
      • Time$
      • Loop$-primer
      • Fast-alists
      • Defconst
      • Defmacro
      • Evaluation
      • Guard
      • Equality-variants
      • Compilation
      • Hons
      • ACL2-built-ins
        • Let
        • Declare
        • Mbe
        • Apply$
        • Fmt
        • Loop$
        • Return-last
        • Mv-let
        • Df
        • Pseudo-termp
        • Defwarrant
        • Time$
        • Mbt
        • Ec-call
        • Mv-nth
        • Sys-call
        • Msg
        • Er
        • Value-triple
        • Comp
        • O-p
        • Member
        • O<
        • Cw
        • Flet
        • Or
        • Hons
        • Cbd
        • Mv
        • Defbadge
        • Append
        • *ACL2-exports*
        • Eql
        • Comment
        • List
        • Unsigned-byte-p
        • Posp
        • Natp
        • The
        • Nth
        • And
        • Len
        • Time-tracker
        • Term-order
        • True-listp
        • Msgp
        • Booleanp
        • <
        • If
        • Pseudo-term-listp
        • +
        • Not
        • With-global-stobj
        • Bitp
        • Equal
        • Cdr
        • Car
        • String-listp
        • Nat-listp
        • Implies
        • Iff
        • Character-listp
        • Alistp
        • Cons
        • Symbol-listp
        • Macrolet
        • Quote
        • Integerp
        • Consp
        • True-list-listp
        • State-global-let*
        • Compress1
        • Symbolp
        • Stringp
        • *common-lisp-symbols-from-main-lisp-package*
        • Characterp
        • Prog2$
        • *
        • Last-prover-steps
        • Hons-acons
        • Eq
        • Let*
        • With-guard-checking
        • @
        • Length
        • With-local-stobj
        • Hard-error
        • -
        • Zp
        • Search
        • Intersection$
        • Assign
        • Aset1
        • Symbol-name
        • Union$
        • Set-gc-strategy
        • In-tau-intervalp
        • Break-on-error
        • Pand
        • Cons-with-hint
        • Case-match
        • Fast-alist-fork
        • Sys-call+
        • ACL2-count
        • Remove-duplicates
        • Signed-byte-p
        • With-serialize-character
        • Observation
        • Hons-resize
        • Make-tau-interval
        • Logbitp
        • Termp
        • Position
        • Assoc
        • *standard-co*
        • Hons-acons!
        • Take
        • Aref1
        • Update-nth
        • Read-run-time
        • Symbol-package-name
        • Hons-wash
        • Expt
        • Coerce
        • Symbol-alistp
        • Get-internal-time
        • Keywordp
        • Intern
        • Non-exec
        • Case
        • Standard-oi
        • Standard-co
        • Formula
        • Nthcdr
        • Atom
        • Without-evisc
        • Good-bye
        • With-local-state
        • Spec-mv-let
        • Intern-in-package-of-symbol
        • Binary-+
        • <=
        • Ash
        • With-fast-alist
        • Set-difference$
        • Hons-clear
        • Flush-compress
        • Rationalp
        • Por
        • Rassoc
        • Remove-assoc
        • =
        • Pargs
        • Nfix
        • Hons-copy
        • Alphorder
        • Subsetp
        • Logand
          • Ihs/logand-lemmas
          • Logand-defaults
          • Logand*
        • Remove1-assoc
        • No-duplicatesp
        • Mv-list
        • Canonical-pathname
        • Aset2
        • Floor
        • Serialize-read
        • Random$
        • Fmt-to-comment-window
        • F-put-global
        • Compress2
        • Concatenate
        • Fast-alist-clean
        • Assert$
        • Remove
        • Remove1
        • Intersectp
        • Endp
        • Put-assoc
        • Princ$
        • Primitive
        • Keyword-value-listp
        • True-list-fix
        • Swap-stobjs
        • Integer-listp
        • Illegal
        • Hons-get
        • With-output-lock
        • Setenv$
        • Open-output-channel!
        • Fast-alist-free
        • Er-progn
        • Cw-print-base-radix
        • Reverse
        • Cond
        • Complex
        • Add-to-set
        • Truncate
        • Digit-char-p
        • Code-char
        • Set-print-case
        • Set-print-base
        • Read-ACL2-oracle
        • Error1
        • Print-object$
        • Plet
        • Integer-length
        • Zip
        • With-live-state
        • Hons-assoc-equal
        • Extend-pathname
        • Logior
        • Char-code
        • With-guard-checking-event
        • Term-listp
        • Print-object$+
        • Fmx-cw
        • String
        • Mod
        • In-package
        • Unary--
        • Set-print-radix
        • Resize-list
        • Pkg-witness
        • Revappend
        • Null
        • Term-list-listp
        • Make-fast-alist
        • Header
        • Boole$
        • Subseq
        • With-guard-checking-error-triple
        • /
        • Make-list
        • Logxor
        • Char-upcase
        • Char-downcase
        • Strip-cars
        • Set-fmt-hard-right-margin
        • Make-ord
        • Ifix
        • Fast-alist-free-on-exit
        • F-get-global
        • Aref2
        • Standard-char-p
        • Lognot
        • Must-be-equal
        • Integer-range-p
        • Getenv$
        • Binary-append
        • Last
        • Er-hard
        • Eqlablep
        • Cpu-core-count
        • Boolean-listp
        • Allocate-fixnum-range
        • ACL2-numberp
        • Butlast
        • Pairlis$
        • Mod-expt
        • Hons-equal
        • Gc$
        • Substitute
        • Ceiling
        • With-stolen-alist
        • Mv?-let
        • String-upcase
        • String-downcase
        • Round
        • Count
        • Char
        • Sys-call-status
        • Progn$
        • Pprogn
        • Lexorder
        • Hons-summary
        • Break$
        • Assert*
        • Alpha-char-p
        • Strip-cdrs
        • Serialize-write
        • Keyword-listp
        • Logeqv
        • List*
        • Proofs-co
        • Maximum-length
        • Fix
        • Explode-nonnegative-integer
        • Eqlable-listp
        • Dimensions
        • Default
        • Arity
        • Upper-case-p
        • Sublis
        • Max
        • Lower-case-p
        • Evenp
        • Explode-atom
        • Change
        • Zerop
        • String<
        • String-equal
        • Abs
        • Set-print-base-radix
        • Print-base-p
        • Nonnegative-integer-quotient
        • Intern$
        • Getprop
        • Binary-*
        • Aset1-trusted
        • Symbol<
        • String-append
        • Rfix
        • Mv?
        • Logic-fns-list-listp
        • Fast-alist-fork!
        • Er-hard?
        • Char-equal
        • 1+
        • *standard-oi*
        • Sys-call*
        • Pos-listp
        • Mbt*
        • Hons-wash!
        • Hons-clear!
        • Signum
        • Rem
        • Real/rationalp
        • Rational-listp
        • O-first-coeff
        • Logic-fnsp
        • Logic-fns-listp
        • Hons-copy-persistent
        • Gc-strategy
        • Fast-alist-summary
        • String>=
        • String<=
        • Acons
        • O-first-expt
        • Fast-alist-clean!
        • >=
        • >
        • Subst
        • Logcount
        • Getpropc
        • Evens
        • Er-soft
        • Digit-to-char
        • Comp-gcl
        • Atom-listp
        • Arities-okp
        • ACL2-number-listp
        • /=
        • Cadr
        • *standard-ci*
        • Unary-/
        • The-true-list
        • Realfix
        • O-rst
        • Fast-alist-len
        • Complex/complex-rationalp
        • Array2p
        • Array1p
        • Logtest
        • Logandc1
        • Char<
        • Trace-co
        • Putprop
        • Get-real-time
        • Eqlable-alistp
        • Count-keys
        • Assoc-string-equal
        • Logorc1
        • Logandc2
        • 1-
        • Packn
        • Logic-termp
        • Logic-term-list-listp
        • Fmt!
        • Fms
        • Cw!
        • Assoc-keyword
        • String>
        • Numerator
        • Logorc2
        • Denominator
        • Char>=
        • The-number
        • Odds
        • Makunbound-global
        • Make-character-list
        • Make
        • List$
        • Get-cpu-time
        • Fmt-to-comment-window!
        • Fms!
        • F-boundp-global
        • Complex-rationalp
        • Alist-to-doublets
        • Access
        • Min
        • Lognor
        • Listp
        • Identity
        • Char>
        • Char<=
        • Zpf
        • Update-nth-array
        • Standard-char-listp
        • O-finp
        • Number-subtrees
        • Logic-term-listp
        • Last-cdr
        • Fmt1!
        • Fmt-to-comment-window!+
        • Character-alistp
        • Oddp
        • Minusp
        • Lognand
        • Imagpart
        • Conjugate
        • Xor
        • Unquote
        • String-alistp
        • Packn-pos
        • Maybe-flush-and-compress1
        • Kwote
        • Int=
        • Fmt1
        • Fmt-to-comment-window+
        • Cw-print-base-radix!
        • Alist-keys-subsetp
        • Realpart
        • Plusp
        • First
        • Symbol-name-lst
        • R-symbol-alistp
        • R-eqlable-alistp
        • Fmx
        • Cw!+
        • Cons-subtrees
        • Cons-count-bounded
        • Cddr
        • Caar
        • Proper-consp
        • Kwote-lst
        • Improper-consp
        • Cw+
        • Rest
        • Standard-char-p+
        • Mbe1
        • Caddr
        • Pairlis-x2
        • Pairlis-x1
        • O>=
        • O<=
        • O-infp
        • Merge-sort-lexorder
        • Fix-true-list
        • Cdddr
        • Set-fmt-soft-right-margin
        • Real-listp
        • O>
        • Cddar
        • Cdar
        • Cdadr
        • Cdaar
        • Cadar
        • Caadr
        • Caaar
        • Cadddr
        • Caddar
        • Third
        • Tenth
        • Sixth
        • Seventh
        • Second
        • Ninth
        • Fourth
        • Fifth
        • Eighth
        • Cddddr
        • Cdddar
        • Cddadr
        • Cddaar
        • Cdaddr
        • Cdadar
        • Cdaadr
        • Cdaaar
        • Cadadr
        • Cadaar
        • Caaddr
        • Caadar
        • Caaadr
        • Caaaar
        • Hons-shrink-alist!
        • Hons-shrink-alist
        • Flush-hons-get-hash-table-link
        • Delete-assoc
      • Developers-guide
      • System-attachments
      • Advanced-features
      • Set-check-invariant-risk
      • Numbers
      • Irrelevant-formals
      • Efficiency
      • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
      • Redefining-programs
      • Lists
      • Invariant-risk
      • Errors
      • Defabbrev
      • Conses
      • Alists
      • Set-register-invariant-risk
      • Strings
      • Program-wrapper
      • Get-internal-time
      • Basics
      • Packages
      • Oracle-eval
      • Defmacro-untouchable
      • Primitive
      • <<
      • Revert-world
      • Unmemoize
      • Set-duplicate-keys-action
      • Symbols
      • Def-list-constructor
      • Easy-simplify-term
      • Defiteration
      • Fake-oracle-eval
      • Defopen
      • Sleep
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Logand
• Logops-recursive-definitions-theory

Logand*

Recursive definition of logand.

Definitions and Theorems

Theorem: logand*

(defthm logand*
  (implies (and (force (integerp i))
                (force (integerp j)))
           (equal (logand i j)
                  (logcons (b-and (logcar i) (logcar j))
                           (logand (logcdr i) (logcdr j)))))
  :rule-classes
  ((:definition :clique (binary-logand)
                :controller-alist ((binary-logand t t)))))