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.
Theorem:
(defthm 4v-alist-<=-necc (implies (not (4v-<= (4v-lookup k x) (4v-lookup k y))) (not (4v-alist-<= x y))))
Theorem:
(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:
(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:
(defthm 4v-alist-<=-nil (4v-alist-<= nil x))
Theorem:
(defthm 4v-alist-<=-refl (4v-alist-<= x x))
Theorem:
(defthm 4v-alist-<=-trans1 (implies (and (4v-alist-<= a b) (4v-alist-<= b c)) (4v-alist-<= a c)))
Theorem:
(defthm 4v-alist-<=-trans2 (implies (and (4v-alist-<= b c) (4v-alist-<= a b)) (4v-alist-<= a c)))
Theorem:
(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:
(defthm 4v-alist-<=-list-with-x (4v-alist-<= (list (cons k (4vx))) x))
Theorem:
(defthm 4v-alist-<=-cons-x (4v-alist-<= (cons (cons k (4vx)) x) x))
Theorem:
(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)))))