• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
      • 4v-sexprs
        • 4v-sexpr-vars
        • 4v-sexpr-eval
        • 4v-sexpr-to-faig
        • 4v-sexpr-restrict-with-rw
        • 4vs-constructors
        • 4v-sexpr-compose-with-rw
        • 4v-sexpr-restrict
        • 4v-sexpr-alist-extract
        • 4v-sexpr-compose
        • 4v-nsexpr-p
        • 4v-sexpr-purebool-p
        • 4v-sexpr-<=
          • 4v-sexpr-alist-<=
        • Sfaig
        • Sexpr-equivs
        • 3v-syntax-sexprp
        • Sexpr-rewriting
        • 4v-sexpr-ind
        • 4v-alist-extract
      • 4v-monotonicity
      • 4v-operations
      • Why-4v-logic
      • 4v-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 4v-sexprs
• 4v-monotonicity

4v-sexpr-<=

Extension of the four-valued lattice ordering to sexprs.

We say X <= Y for sexprs if X always evaluates to a smaller value than Y evaluates to in every environment, in the sense of 4v-<=.

When X <= Y, we sometimes call X a conservative approximation of Y.

Definitions and Theorems

Theorem: 4v-sexpr-<=-necc

(defthm 4v-sexpr-<=-necc
        (implies (not (4v-<= (4v-sexpr-eval x env)
                             (4v-sexpr-eval y env)))
                 (not (4v-sexpr-<= x y))))

Theorem: 4v-sexpr-<=-witnessing-witness-rule-correct

(defthm
  4v-sexpr-<=-witnessing-witness-rule-correct
  (implies (not ((lambda (env y x)
                         (not (4v-<=$inline (4v-sexpr-eval x env)
                                            (4v-sexpr-eval y env))))
                 (4v-sexpr-<=-witness x y)
                 y x))
           (4v-sexpr-<= x y))
  :rule-classes nil)

Theorem: 4v-sexpr-<=-instancing-instance-rule-correct

(defthm 4v-sexpr-<=-instancing-instance-rule-correct
        (implies (not (4v-<=$inline (4v-sexpr-eval x env)
                                    (4v-sexpr-eval y env)))
                 (not (4v-sexpr-<= x y)))
        :rule-classes nil)

Theorem: 4v-sexpr-<=-nil

(defthm 4v-sexpr-<=-nil (4v-sexpr-<= nil x))

Theorem: 4v-sexpr-<=-refl

(defthm 4v-sexpr-<=-refl (4v-sexpr-<= x x))

Theorem: 4v-sexpr-<=-trans1

(defthm 4v-sexpr-<=-trans1
        (implies (and (4v-sexpr-<= a b)
                      (4v-sexpr-<= b c))
                 (4v-sexpr-<= a c)))

Theorem: 4v-sexpr-<=-trans2

(defthm 4v-sexpr-<=-trans2
        (implies (and (4v-sexpr-<= b c)
                      (4v-sexpr-<= a b))
                 (4v-sexpr-<= a c)))

Subtopics

4v-sexpr-alist-<=

Extension of 4v-sexpr-<= to alists.