		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhs-cons

Signature
(lhs-cons x y) → cons
Arguments: x — Guard (lhrange-p x).; y — Guard (lhs-p y).
Returns: cons — Type (lhs-p cons).

Definitions and Theorems

Function: lhs-cons

(defun lhs-cons (x y)
  (declare (xargs :guard (and (lhrange-p x) (lhs-p y))))
  (let ((__function__ 'lhs-cons))
    (declare (ignorable __function__))
    (if (atom y)
        (list (lhrange-fix x))
      (let ((comb (lhrange-combine x (car y))))
        (if comb (cons comb (lhs-fix (cdr y)))
          (cons (lhrange-fix x) (lhs-fix y)))))))

Theorem: lhs-p-of-lhs-cons

(defthm lhs-p-of-lhs-cons
  (b* ((cons (lhs-cons x y)))
    (lhs-p cons))
  :rule-classes :rewrite)

Theorem: lhs-cons-of-lhrange-fix-x

(defthm lhs-cons-of-lhrange-fix-x
  (equal (lhs-cons (lhrange-fix x) y)
         (lhs-cons x y)))

Theorem: lhs-cons-lhrange-equiv-congruence-on-x

(defthm lhs-cons-lhrange-equiv-congruence-on-x
  (implies (lhrange-equiv x x-equiv)
           (equal (lhs-cons x y)
                  (lhs-cons x-equiv y)))
  :rule-classes :congruence)

Theorem: lhs-cons-of-lhs-fix-y

(defthm lhs-cons-of-lhs-fix-y
  (equal (lhs-cons x (lhs-fix y))
         (lhs-cons x y)))

Theorem: lhs-cons-lhs-equiv-congruence-on-y

(defthm lhs-cons-lhs-equiv-congruence-on-y
  (implies (lhs-equiv y y-equiv)
           (equal (lhs-cons x y)
                  (lhs-cons x y-equiv)))
  :rule-classes :congruence)

Theorem: lhs-cons-correct

(defthm lhs-cons-correct
  (equal (lhs-eval (lhs-cons x y) env)
         (lhs-eval (cons x y) env)))

Theorem: lhs-cons-correct-zero

(defthm lhs-cons-correct-zero
  (equal (lhs-eval-zx (lhs-cons x y) env)
         (lhs-eval-zx (cons x y) env)))

Theorem: lhs-width-of-lhs-cons

(defthm lhs-width-of-lhs-cons
  (<= (lhs-width (lhs-cons x y))
      (+ (lhrange->w x) (lhs-width y)))
  :rule-classes :linear)

Theorem: lhs-cons-of-lhs-cons

(defthm lhs-cons-of-lhs-cons
  (implies (lhrange-combine x y)
           (equal (lhs-cons x (lhs-cons y z))
                  (lhs-cons (lhrange-combine x y) z))))

Theorem: lhs-cons-of-lhs-cons-when-not-combinable

(defthm lhs-cons-of-lhs-cons-when-not-combinable
  (implies (not (lhrange-combine x y))
           (equal (lhs-cons x (lhs-cons y z))
                  (cons (lhrange-fix x) (lhs-cons y z)))))

Theorem: consp-of-lhs-cons

(defthm consp-of-lhs-cons
  (equal (consp (lhs-cons x y)) t))

Theorem: lhrange->atom-car-lhs-cons

(defthm lhrange->atom-car-lhs-cons
  (equal (lhrange->atom (car (lhs-cons x y)))
         (lhrange->atom x)))

Theorem: lhrange->w-of-car-lhs-cons

(defthm lhrange->w-of-car-lhs-cons
  (<= (lhrange->w x)
      (lhrange->w (car (lhs-cons x y))))
  :rule-classes :linear)