• Top
  • Documentation
  • Books
  • 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-<=
            • 4v-sexpr-alist-<=-alt
        • 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
  • Math
  • Testing-utilities

• 4v-sexpr-<=

4v-sexpr-alist-<=

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

We say X <= Y for sexpr alists when X[k] <= Y[k] for all keys k.

Definitions and Theorems

Theorem: 4v-sexpr-alist-<=-necc

(defthm 4v-sexpr-alist-<=-necc
  (implies (not (4v-sexpr-<= (cdr (hons-assoc-equal k a))
                             (cdr (hons-assoc-equal k b))))
           (not (4v-sexpr-alist-<= a b))))

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

(defthm 4v-sexpr-alist-<=-witnessing-witness-rule-correct
  (implies (not ((lambda (k b a)
                   (not (4v-sexpr-<= (cdr (hons-assoc-equal k a))
                                     (cdr (hons-assoc-equal k b)))))
                 (4v-sexpr-alist-<=-witness a b)
                 b a))
           (4v-sexpr-alist-<= a b))
  :rule-classes nil)

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

(defthm 4v-sexpr-alist-<=-instancing-instance-rule-correct
  (implies (not (4v-sexpr-<= (cdr (hons-assoc-equal k a))
                             (cdr (hons-assoc-equal k b))))
           (not (4v-sexpr-alist-<= a b)))
  :rule-classes nil)

Theorem: 4v-sexpr-alist-<=-refl

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

Theorem: 4v-sexpr-alist-<=-trans1

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

Theorem: 4v-sexpr-alist-<=-trans2

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

Theorem: hons-assoc-equal-sexpr-monotonic

(defthm hons-assoc-equal-sexpr-monotonic
  (implies (4v-sexpr-alist-<= a b)
           (4v-sexpr-<= (cdr (hons-assoc-equal k a))
                        (cdr (hons-assoc-equal k b)))))

Subtopics

4v-sexpr-alist-<=-alt

Just a different way to define <= for sexpr alists.