		Search-engine friendly clone of the ACL2 documentation.

Skip-detection

Sd-problem->

Basic ordering on skip-detect problems.

Signature
(sd-problem-> x y) → *
Arguments: x — Guard (sd-problem-p x).; y — Guard (sd-problem-p y).

Definitions and Theorems

Function: sd-problem->

(defun sd-problem-> (x y)
  (declare (xargs :guard (and (sd-problem-p x)
                              (sd-problem-p y))))
  (let ((__function__ 'sd-problem->))
    (declare (ignorable __function__))
    (> (sd-problem-score x)
       (sd-problem-score y))))

Theorem: sd-problem->-transitive

(defthm sd-problem->-transitive
  (implies (and (sd-problem-> x y)
                (sd-problem-> y z))
           (sd-problem-> x z)))