• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
      • X86isa
        • Program-execution
        • Introduction
        • X86isa-build-instructions
        • Publications
        • Contributors
        • Machine
        • Implemented-opcodes
        • Proof-utilities
          • System-level-marking-view-proof-utilities
          • Non-marking-view-proof-utilities
          • App-view-proof-utilities
          • Subset-p
          • Disjoint-p
          • Pos
          • Member-p
          • No-duplicates-p
          • Common-system-level-utils
            • Separate-mapped-mem
          • Debugging-code-proofs
          • General-memory-utils
          • X86-row-wow-thms
        • To-do
        • Concrete-simulation-examples
        • Model-validation
        • Utils
        • Debugging-code-proofs
      • Execloader
      • Axe
    • Testing-utilities
    • Math
  • Proof-utilities

Common-system-level-utils

Reasoning in the system-level view

This book contains lemmas that come in useful in both the marking and non-marking sub-views of the system-level view.

Subtopics

Separate-mapped-mem