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

• 4v

4v-monotonicity

The monotonicity property satisfied by all 4v-operations.

All of our primitive four-valued operations satisfy the following monotonicity property, where <= denotes 4v-<=:

Whenever a <= b, f(a) <= f(b).

A higher-arity function is monotonic if it is monotonic with respect to each of its arguments, e.g., a binary function is monotonic if:

Whenever a1 <= a2, f(a1, b1) <= f(a2, b2), and
Whenever b1 <= b2, f(a1, b1) <= f(a2, b2).

This monotonicity requirement ensures that our operations respect the special status of X as an unknown. For instance, an operation h would not be monotonic if h(X) = T but h(T) = F.

Another way of looking at this is, if h is monotonic and we know that h(X) = T, then this means that h(v) = T for any value v, regardless of whether it is T, F, X, or Z.

On the other hand, if we only know that h(X) = X, then we cannot conclude anything about h(T). It only means that if we are unsure of the value of the input, then we are unsure of the value of the output.

Definitions and Theorems

Function: p4vm-suffix-args

(defun p4vm-suffix-args (args)
       (if (atom args)
           nil
           (cons (intern-in-package-of-symbol
                      (concatenate 'string
                                   (symbol-name (car args))
                                   "1")
                      (car args))
                 (p4vm-suffix-args (cdr args)))))

Function: p4vm-4v-<=-args

(defun p4vm-4v-<=-args (args suff-args)
       (if (atom args)
           nil
           (cons (list '4v-<= (car args) (car suff-args))
                 (p4vm-4v-<=-args (cdr args)
                                  (cdr suff-args)))))

Theorem: 4v-fix-is-monotonic

(defthm 4v-fix-is-monotonic
        (implies (and (4v-<= a a1))
                 (4v-<= (4v-fix a) (4v-fix a1))))

Theorem: 4v-unfloat-is-monotonic

(defthm 4v-unfloat-is-monotonic
        (implies (and (4v-<= a a1))
                 (4v-<= (4v-unfloat a) (4v-unfloat a1))))

Theorem: 4v-not-is-monotonic

(defthm 4v-not-is-monotonic
        (implies (and (4v-<= a a1))
                 (4v-<= (4v-not a) (4v-not a1))))

Theorem: 4v-xdet-is-monotonic

(defthm 4v-xdet-is-monotonic
        (implies (and (4v-<= a a1))
                 (4v-<= (4v-xdet a) (4v-xdet a1))))

Theorem: 4v-and-is-monotonic

(defthm 4v-and-is-monotonic
        (implies (and (4v-<= a a1) (4v-<= b b1))
                 (4v-<= (4v-and a b) (4v-and a1 b1))))

Theorem: 4v-or-is-monotonic

(defthm 4v-or-is-monotonic
        (implies (and (4v-<= a a1) (4v-<= b b1))
                 (4v-<= (4v-or a b) (4v-or a1 b1))))

Theorem: 4v-xor-is-monotonic

(defthm 4v-xor-is-monotonic
        (implies (and (4v-<= a a1) (4v-<= b b1))
                 (4v-<= (4v-xor a b) (4v-xor a1 b1))))

Theorem: 4v-iff-is-monotonic

(defthm 4v-iff-is-monotonic
        (implies (and (4v-<= a a1) (4v-<= b b1))
                 (4v-<= (4v-iff a b) (4v-iff a1 b1))))

Theorem: 4v-res-is-monotonic

(defthm 4v-res-is-monotonic
        (implies (and (4v-<= a a1) (4v-<= b b1))
                 (4v-<= (4v-res a b) (4v-res a1 b1))))

Theorem: 4v-ite-is-monotonic

(defthm 4v-ite-is-monotonic
        (implies (and (4v-<= c c1)
                      (4v-<= a a1)
                      (4v-<= b b1))
                 (4v-<= (4v-ite c a b)
                        (4v-ite c1 a1 b1))))

Theorem: 4v-ite*-is-monotonic

(defthm 4v-ite*-is-monotonic
        (implies (and (4v-<= c c1)
                      (4v-<= a a1)
                      (4v-<= b b1))
                 (4v-<= (4v-ite* c a b)
                        (4v-ite* c1 a1 b1))))

Theorem: 4v-zif-is-monotonic

(defthm 4v-zif-is-monotonic
        (implies (and (4v-<= c c1)
                      (4v-<= a a1)
                      (4v-<= b b1))
                 (4v-<= (4v-zif c a b)
                        (4v-zif c1 a1 b1))))

Theorem: 4v-tristate-is-monotonic

(defthm 4v-tristate-is-monotonic
        (implies (and (4v-<= c c1) (4v-<= a a1))
                 (4v-<= (4v-tristate c a)
                        (4v-tristate c1 a1))))

Theorem: 4v-pullup-is-monotonic

(defthm 4v-pullup-is-monotonic
        (implies (and (4v-<= a a1))
                 (4v-<= (4v-pullup a) (4v-pullup a1))))

Theorem: 4v-wand-is-monotonic

(defthm 4v-wand-is-monotonic
        (implies (and (4v-<= a a1) (4v-<= b b1))
                 (4v-<= (4v-wand a b) (4v-wand a1 b1))))

Theorem: 4v-wor-is-monotonic

(defthm 4v-wor-is-monotonic
        (implies (and (4v-<= a a1) (4v-<= b b1))
                 (4v-<= (4v-wor a b) (4v-wor a1 b1))))

Subtopics

4v-sexpr-<=

Extension of the four-valued lattice ordering to sexprs.