• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
      • X86isa
        • Program-execution
        • Sdm-instruction-set-summary
        • Tlb
        • Running-linux
        • Introduction
        • Asmtest
        • X86isa-build-instructions
        • Publications
        • Contributors
        • Machine
          • X86isa-state
          • Syscalls
          • Cpuid
          • Linear-memory
          • Rflag-specifications
          • Characterizing-undefined-behavior
          • Top-level-memory
          • App-view
          • X86-decoder
          • Physical-memory
          • Decoding-and-spec-utils
          • Instructions
            • Two-byte-opcodes
            • One-byte-opcodes
            • Fp-opcodes
            • Instruction-semantic-functions
            • X86-illegal-instruction
            • Implemented-opcodes
            • Opcode-maps
              • Cpuid
              • Opcode-maps-structures
                • Opcode
                • Inst
                • Op/en-p
                • Operands
                • Inst-list-p
                • Operand-type-p
                • Strict-opcode-p
                • Opcode-extension-group-p
                • Superscripts-p
                • Maybe-operands-p
                • Exception-desc-p
                • Count-avx-pfx-cases
                • Mnemonic-p
                • Maybe-3bits-p
                • Op-pfx-p
                • Maybe-vex-p
                • Maybe-evex-p
                • Fn-desc-p
                • Op-mode-p
                • Rex-p
                • Mod-p
                • Avx-pfx-well-formed-p
                • Any-present-in
                  • Superscripts-fix
                  • Strict-opcode-fix
                  • Operand-type-fix
                  • Opcode-extension-group-fix
                  • Maybe-operands-fix
                  • Maybe-evex-fix
                  • Maybe-3bits-fix
                  • Keyword-list-fix
                  • Exception-desc-fix
                  • Rex-fix
                  • Op-pfx-fix
                  • Op-mode-fix
                  • Mod-fix
                  • Mnemonic-fix
                  • Maybe-vex-fix
                  • Fn-desc-fix
                  • Vex-p
                  • Evex-p
                • Implemented-opcodes
                • Chk-exc-fn
                • Filtering-instructions
                • Addressing-method-code-p
                • Operand-type-code-p
                • Eval-pre-map
              • X86-general-protection
              • X86-device-not-available
              • X86-step-unimplemented
              • Privileged-opcodes
              • Three-byte-opcodes
            • Register-readers-and-writers
            • X86-modes
            • Segmentation
            • Other-non-deterministic-computations
            • Environment
            • Paging
          • Implemented-opcodes
          • To-do
          • Proof-utilities
          • Peripherals
          • Model-validation
          • Modelcalls
          • Concrete-simulation-examples
          • Utils
          • Debugging-code-proofs
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Quote
    • Opcode-maps-structures

    Any-present-in

    Is any element of xs present in ys?

    Signature
    (any-present-in xs ys) → *
    Arguments
    xs — Guard (true-listp xs).
    ys — Guard (true-listp ys).

    Definitions and Theorems

    Function: any-present-in

    (defun any-present-in (xs ys)
      (declare (xargs :guard (and (true-listp xs) (true-listp ys))))
      (let ((__function__ 'any-present-in))
        (declare (ignorable __function__))
        (if (endp xs)
            nil
          (if (member-equal (car xs) ys)
              t
            (any-present-in (cdr xs) ys)))))