• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
      • Sat-solver-options
      • Config-p
      • Logical-story
      • Dimacs
      • Gather-benchmarks
      • Cnf
        • Litp
        • Varp
        • Env$
        • Eval-formula
        • Max-index-formula
          • Fast-max-index-formula
        • Max-index-clause
        • Formula-indices
        • Clause-indices
      • Satlink-extra-hook
      • Sat
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Max-index-formula

Fast-max-index-formula

Tail recursive version of max-index-formula.

Signature

(fast-max-index-formula formula max) → *

Arguments

formula — Guard (lit-list-listp formula).

max — Guard (natp max).

Definitions and Theorems

Function: fast-max-index-formula

(defun fast-max-index-formula (formula max)
  (declare (xargs :guard (and (lit-list-listp formula)
                              (natp max))))
  (let ((__function__ 'fast-max-index-formula))
    (declare (ignorable __function__))
    (b* (((when (atom formula)) (lnfix max))
         (max (fast-max-index-clause (car formula)
                                     max)))
      (fast-max-index-formula (cdr formula)
                              max))))

Theorem: fast-max-index-formula-of-lit-list-list-fix-formula

(defthm fast-max-index-formula-of-lit-list-list-fix-formula
  (equal (fast-max-index-formula (lit-list-list-fix formula)
                                 max)
         (fast-max-index-formula formula max)))

Theorem: fast-max-index-formula-lit-list-list-equiv-congruence-on-formula

(defthm
   fast-max-index-formula-lit-list-list-equiv-congruence-on-formula
  (implies (lit-list-list-equiv formula formula-equiv)
           (equal (fast-max-index-formula formula max)
                  (fast-max-index-formula formula-equiv max)))
  :rule-classes :congruence)

Theorem: fast-max-index-formula-of-nfix-max

(defthm fast-max-index-formula-of-nfix-max
  (equal (fast-max-index-formula formula (nfix max))
         (fast-max-index-formula formula max)))

Theorem: fast-max-index-formula-nat-equiv-congruence-on-max

(defthm fast-max-index-formula-nat-equiv-congruence-on-max
  (implies (nat-equiv max max-equiv)
           (equal (fast-max-index-formula formula max)
                  (fast-max-index-formula formula max-equiv)))
  :rule-classes :congruence)