• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • 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
          • Rb-alt
          • Unwind-x86-interpreter-in-marking-view
          • Get-prefixes-alt
          • Get-prefixes-in-system-level-marking-view
          • Program-at-alt
          • Rb-in-system-level-marking-view
          • Xlate-equiv-memory-and-rml08
          • Reasoning-about-page-tables
          • Las-to-pas-two-n-ind-hint
          • Find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux
          • Replace-element
        • Non-marking-view-proof-utilities
        • App-view-proof-utilities
        • Subset-p
        • Disjoint-p
        • Pos
        • Member-p
        • No-duplicates-p
        • Common-system-level-utils
        • Debugging-code-proofs
        • General-memory-utils
        • X86-row-wow-thms
      • To-do
      • Concrete-simulation-examples
      • Model-validation
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• System-level-marking-view-proof-utilities

Find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux

Signature

(find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux vars calls) 
  → 
*

Arguments

vars — Guard (true-listp vars).

Definitions and Theorems

Function: find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux

(defun find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux (vars calls)
 (declare (xargs :guard (true-listp vars)))
 (declare (xargs :guard (equal (len vars) 2)))
 (let
  ((__function__ 'find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux))
  (declare (ignorable __function__))
  (if (atom calls)
      nil
    (b* ((one-call (car calls))
         ((unless (and (true-listp one-call)
                       (equal 3 (len one-call))))
          nil)
         (mv-nth-term-1 (nth 1 one-call))
         ((unless (and (true-listp mv-nth-term-1)
                       (equal 3 (len mv-nth-term-1))))
          nil)
         (term-1 (nth 2 mv-nth-term-1))
         ((unless (and (true-listp term-1)
                       (equal 5 (len term-1))))
          nil)
         ((list n-var addr-var) vars))
      (cons (list (cons n-var (nth 1 term-1))
                  (cons addr-var (nth 2 term-1)))
            (find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux
                 vars (cdr calls)))))))