		Search-engine friendly clone of the ACL2 documentation.

Fty-pseudo-term-utilities

Fty-check-if-call

FTY version of check-if-call.

Signature
(fty-check-if-call term) → (mv yes/no test then else)
Arguments: term — Guard (pseudo-termp term).
Returns: yes/no — Type (booleanp yes/no).; test — Type (pseudo-termp test).; then — Type (pseudo-termp then).; else — Type (pseudo-termp else).

Definitions and Theorems

Function: fty-check-if-call

(defun fty-check-if-call (term)
  (declare (xargs :guard (pseudo-termp term)))
  (let ((__function__ 'fty-check-if-call))
    (declare (ignorable __function__))
    (check-if-call (pseudo-term-fix term))))

Theorem: booleanp-of-fty-check-if-call.yes/no

(defthm booleanp-of-fty-check-if-call.yes/no
  (b* (((mv ?yes/no ?test ?then ?else)
        (fty-check-if-call term)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-fty-check-if-call.test

(defthm pseudo-termp-of-fty-check-if-call.test
  (b* (((mv ?yes/no ?test ?then ?else)
        (fty-check-if-call term)))
    (pseudo-termp test))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-fty-check-if-call.then

(defthm pseudo-termp-of-fty-check-if-call.then
  (b* (((mv ?yes/no ?test ?then ?else)
        (fty-check-if-call term)))
    (pseudo-termp then))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-fty-check-if-call.else

(defthm pseudo-termp-of-fty-check-if-call.else
  (b* (((mv ?yes/no ?test ?then ?else)
        (fty-check-if-call term)))
    (pseudo-termp else))
  :rule-classes :rewrite)

Theorem: pseudo-term-count-of-check-if-call.test

(defthm pseudo-term-count-of-check-if-call.test
  (implies (pseudo-termp term)
           (b* (((mv yes/no test & &)
                 (check-if-call term)))
             (implies yes/no
                      (< (pseudo-term-count test)
                         (pseudo-term-count term)))))
  :rule-classes :linear)

Theorem: pseudo-term-count-of-fty-check-if-call.test

(defthm pseudo-term-count-of-fty-check-if-call.test
  (b* (((mv ?yes/no ?test ?then ?else)
        (fty-check-if-call term)))
    (implies yes/no
             (< (pseudo-term-count test)
                (pseudo-term-count term))))
  :rule-classes :linear)

Theorem: pseudo-term-count-of-check-if-call.then

(defthm pseudo-term-count-of-check-if-call.then
  (implies (pseudo-termp term)
           (b* (((mv yes/no & then &)
                 (check-if-call term)))
             (implies yes/no
                      (< (pseudo-term-count then)
                         (pseudo-term-count term)))))
  :rule-classes :linear)

Theorem: pseudo-term-count-of-fty-check-if-call.then

(defthm pseudo-term-count-of-fty-check-if-call.then
  (b* (((mv ?yes/no ?test ?then ?else)
        (fty-check-if-call term)))
    (implies yes/no
             (< (pseudo-term-count then)
                (pseudo-term-count term))))
  :rule-classes :linear)

Theorem: pseudo-term-count-of-check-if-call.else

(defthm pseudo-term-count-of-check-if-call.else
  (implies (pseudo-termp term)
           (b* (((mv yes/no & & else)
                 (check-if-call term)))
             (implies yes/no
                      (< (pseudo-term-count else)
                         (pseudo-term-count term)))))
  :rule-classes :linear)

Theorem: pseudo-term-count-of-fty-check-if-call.else

(defthm pseudo-term-count-of-fty-check-if-call.else
  (b* (((mv ?yes/no ?test ?then ?else)
        (fty-check-if-call term)))
    (implies yes/no
             (< (pseudo-term-count else)
                (pseudo-term-count term))))
  :rule-classes :linear)

Theorem: pseudo-term-count-of-check-if-call

(defthm pseudo-term-count-of-check-if-call
  (implies (pseudo-termp term)
           (b* (((mv yes/no test then else)
                 (check-if-call term)))
             (implies yes/no
                      (< (+ (pseudo-term-count test)
                            (pseudo-term-count then)
                            (pseudo-term-count else))
                         (pseudo-term-count term)))))
  :rule-classes :linear)

Theorem: pseudo-term-count-of-fty-check-if-call

(defthm pseudo-term-count-of-fty-check-if-call
  (b* (((mv ?yes/no ?test ?then ?else)
        (fty-check-if-call term)))
    (implies yes/no
             (< (+ (pseudo-term-count test)
                   (pseudo-term-count then)
                   (pseudo-term-count else))
                (pseudo-term-count term))))
  :rule-classes :linear)