		Search-engine friendly clone of the ACL2 documentation.

Svar-split-segment

Svar-split-segment->rest

Get the rest field from a svar-split-segment.

Signature
(svar-split-segment->rest x) → rest
Arguments: x — Guard (svar-split-p x).
Returns: rest — Type (svar-split-p rest).

This is an ordinary field accessor created by defprod.

Definitions and Theorems

Function: svar-split-segment->rest$inline

(defun svar-split-segment->rest$inline (x)
  (declare (xargs :guard (svar-split-p x)))
  (declare (xargs :guard (equal (svar-split-kind x) :segment)))
  (let ((__function__ 'svar-split-segment->rest))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((x (and (equal (svar-split-kind x) :segment)
                      x)))
           (svar-split-fix (std::da-nth 2 (cdr x))))
         :exec (std::da-nth 2 (cdr x)))))

Theorem: svar-split-p-of-svar-split-segment->rest

(defthm svar-split-p-of-svar-split-segment->rest
  (b* ((rest (svar-split-segment->rest$inline x)))
    (svar-split-p rest))
  :rule-classes :rewrite)

Theorem: svar-split-segment->rest$inline-of-svar-split-fix-x

(defthm svar-split-segment->rest$inline-of-svar-split-fix-x
  (equal (svar-split-segment->rest$inline (svar-split-fix x))
         (svar-split-segment->rest$inline x)))

Theorem: svar-split-segment->rest$inline-svar-split-equiv-congruence-on-x

(defthm
   svar-split-segment->rest$inline-svar-split-equiv-congruence-on-x
  (implies (svar-split-equiv x x-equiv)
           (equal (svar-split-segment->rest$inline x)
                  (svar-split-segment->rest$inline x-equiv)))
  :rule-classes :congruence)

Theorem: svar-split-segment->rest-when-wrong-kind

(defthm svar-split-segment->rest-when-wrong-kind
  (implies (not (equal (svar-split-kind x) :segment))
           (equal (svar-split-segment->rest x)
                  (svar-split-fix nil))))