• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
      • 4v-sexprs
      • 4v-monotonicity
      • 4v-operations
      • Why-4v-logic
      • 4v-<=
        • 4v-alist-<=
        • 4v-list-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 4v-<=

4v-alist-<=

Extension of 4v-<= to four-valued alists.

We say X <= Y for four-valued alists (i.e., alists whose every value is a four-valued constant), when X[k] <= Y[k] for every key k.

Definitions and Theorems

Theorem: 4v-alist-<=-necc

(defthm 4v-alist-<=-necc
        (implies (not (4v-<= (4v-lookup k x) (4v-lookup k y)))
                 (not (4v-alist-<= x y))))

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

(defthm 4v-alist-<=-witnessing-witness-rule-correct
        (implies (not ((lambda (k y x)
                               (not (4v-<=$inline (4v-lookup k x)
                                                  (4v-lookup k y))))
                       (4v-alist-<=-witness x y)
                       y x))
                 (4v-alist-<= x y))
        :rule-classes nil)

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

(defthm 4v-alist-<=-instancing-instance-rule-correct
        (implies (not (4v-<=$inline (4v-lookup k x)
                                    (4v-lookup k y)))
                 (not (4v-alist-<= x y)))
        :rule-classes nil)

Theorem: 4v-alist-<=-nil

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

Theorem: 4v-alist-<=-refl

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

Theorem: 4v-alist-<=-trans1

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

Theorem: 4v-alist-<=-trans2

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

Theorem: 4v-alist-<=-acons

(defthm 4v-alist-<=-acons
        (implies (and (4v-<= a b) (4v-alist-<= al1 al2))
                 (4v-alist-<= (cons (cons k a) al1)
                              (cons (cons k b) al2))))

Theorem: 4v-alist-<=-list-with-x

(defthm 4v-alist-<=-list-with-x
        (4v-alist-<= (list (cons k (4vx))) x))

Theorem: 4v-alist-<=-cons-x

(defthm 4v-alist-<=-cons-x
        (4v-alist-<= (cons (cons k (4vx)) x) x))

Theorem: 4v-alist-<=-acons-1

(defthm 4v-alist-<=-acons-1
        (implies (not (hons-assoc-equal k a))
                 (iff (4v-alist-<= (cons (cons k v) a) b)
                      (and (4v-<= v (4v-lookup k b))
                           (4v-alist-<= a b)))))