• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • 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
        • Max-index-clause
          • Fast-max-index-clause
        • Formula-indices
        • Clause-indices
      • Satlink-extra-hook
      • Sat
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Cnf

Max-index-clause

Maximum index of any identifier used anywhere in a clause.

Signature

(max-index-clause clause) → max

Arguments

clause — Guard (lit-listp clause).

Returns

max — Type (natp max).

Definitions and Theorems

Function: max-index-clause

(defun max-index-clause (clause)
       (declare (xargs :guard (lit-listp clause)))
       (let ((__function__ 'max-index-clause))
            (declare (ignorable __function__))
            (mbe :logic (if (atom clause)
                            0
                            (max (lit->var (car clause))
                                 (max-index-clause (cdr clause))))
                 :exec (fast-max-index-clause clause 0))))

Theorem: natp-of-max-index-clause

(defthm natp-of-max-index-clause
        (b* ((max (max-index-clause clause)))
            (natp max))
        :rule-classes :type-prescription)

Theorem: fast-max-index-clause-removal

(defthm fast-max-index-clause-removal
        (equal (fast-max-index-clause clause max)
               (max (nfix max)
                    (max-index-clause clause))))

Theorem: max-index-clause-of-lit-list-fix-clause

(defthm max-index-clause-of-lit-list-fix-clause
        (equal (max-index-clause (lit-list-fix clause))
               (max-index-clause clause)))

Theorem: max-index-clause-lit-list-equiv-congruence-on-clause

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

Subtopics

Fast-max-index-clause

Tail-recursive version of max-index-clause.