• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Riscv
        • Semantics
        • States
        • Features
          • Feat-base
          • Feat
          • Feat->xnum
          • Feat->xlen
          • Feat-64p
          • Feat-32p
          • Feat-embedp
          • Feat-mp
            • Feat-rv64im
            • Feat-rv64i
            • Feat-rv64em
            • Feat-rv64e
            • Feat-rv32im
            • Feat-rv32i
            • Feat-rv32em
            • Feat-rv32e
          • Instructions
          • Decoding
          • Encoding
          • Reads-over-writes
          • Rv32im
          • Rv64im
          • Execution
        • Instant-runoff-voting
        • Imp-language
        • Sidekick
        • Leftist-trees
        • Java
        • Taspi
        • Bitcoin
        • Des
        • Ethereum
        • X86isa
        • Sha-2
        • Yul
        • Zcash
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Poseidon
        • Where-do-i-place-my-book
        • Axe
        • Bigmems
        • Builtins
        • Execloader
        • Aleo
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Std
      • Community
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Features

    Feat-mp

    Check if the features indicate the M extension.

    Signature
    (feat-mp feat) → yes/no
    Arguments
    feat — Guard (featp feat).
    Returns
    yes/no — Type (booleanp yes/no).

    Definitions and Theorems

    Function: feat-mp

    (defun feat-mp (feat)
      (declare (xargs :guard (featp feat)))
      (let ((__function__ 'feat-mp))
        (declare (ignorable __function__))
        (feat->m feat)))

    Theorem: booleanp-of-feat-mp

    (defthm booleanp-of-feat-mp
      (b* ((yes/no (feat-mp feat)))
        (booleanp yes/no))
      :rule-classes :rewrite)

    Theorem: feat-mp-of-feat-fix-feat

    (defthm feat-mp-of-feat-fix-feat
      (equal (feat-mp (feat-fix feat))
             (feat-mp feat)))

    Theorem: feat-mp-feat-equiv-congruence-on-feat

    (defthm feat-mp-feat-equiv-congruence-on-feat
      (implies (feat-equiv feat feat-equiv)
               (equal (feat-mp feat)
                      (feat-mp feat-equiv)))
      :rule-classes :congruence)