• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
      • Sat-solver-options
      • Config-p
      • Logical-story
      • Dimacs
      • Gather-benchmarks
      • Cnf
        • Litp
          • Lit-negate-cond
          • Lit-negate
          • Make-lit
          • Lit-equiv
          • Lit->var
          • Lit->neg
          • Lit-list
          • Maybe-litp
            • Maybe-lit-fix
          • Lit-fix
          • Lit-list-list
        • Varp
        • Env$
        • Eval-formula
        • Max-index-formula
        • Max-index-clause
        • Formula-indices
        • Clause-indices
      • Satlink-extra-hook
      • Sat
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Fty::basetypes
• Maybe-litp

Maybe-lit-fix

(maybe-lit-fix x) is the identity for maybe-litps, or coerces any non-litp to nil.

Performance note. In the execution this is just an inlined identity function, i.e., it should have zero runtime cost.

Definitions and Theorems

Function: maybe-lit-fix$inline

(defun maybe-lit-fix$inline (x)
  (declare (xargs :guard (maybe-litp x)))
  (mbe :logic (if x (lit-fix x) nil)
       :exec x))

Theorem: maybe-litp-of-maybe-lit-fix

(defthm maybe-litp-of-maybe-lit-fix
  (maybe-litp (maybe-lit-fix x))
  :rule-classes (:rewrite :type-prescription))

Theorem: maybe-lit-fix-when-maybe-litp

(defthm maybe-lit-fix-when-maybe-litp
  (implies (maybe-litp x)
           (equal (maybe-lit-fix x) x)))

Theorem: maybe-lit-fix-under-iff

(defthm maybe-lit-fix-under-iff
  (iff (maybe-lit-fix x) x))

Theorem: maybe-lit-fix-under-lit-equiv

(defthm maybe-lit-fix-under-lit-equiv
  (lit-equiv (maybe-lit-fix x) x))