• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Real
    • ACL2-tutorial
    • Debugging
    • Miscellaneous
    • Prover-output
    • Built-in-theorems
      • Built-in-theorems-about-arithmetic
      • Built-in-theorems-about-symbols
      • Built-in-theorems-about-characters
      • Built-in-theorems-about-lists
      • Built-in-theorems-about-arrays
      • Built-in-theorems-about-strings
      • Built-in-theorems-about-alists
      • Built-in-theorems-about-total-order
      • Built-in-theorems-about-system-utilities
      • Built-in-theorems-about-cons-pairs
      • Built-in-theorems-for-tau
      • Built-in-theorems-about-bad-atoms
      • Built-in-theorems-about-logical-connectives
      • Built-in-theorems-about-booleans
      • Built-in-theorems-about-random$
      • Built-in-theorems-about-eqlables
    • Macros
    • Interfacing-tools
    • About-ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Built-in-theorems

Built-in-theorems-about-total-order

Built-in theorems about the total order on values.

Theorem: alphorder-reflexive

(defthm alphorder-reflexive
        (implies (not (consp x))
                 (alphorder x x)))

Theorem: alphorder-anti-symmetric

(defthm alphorder-anti-symmetric
        (implies (and (not (consp x))
                      (not (consp y))
                      (alphorder x y)
                      (alphorder y x))
                 (equal x y))
        :rule-classes
        ((:forward-chaining
              :corollary (implies (and (alphorder x y)
                                       (not (consp x))
                                       (not (consp y)))
                                  (iff (alphorder y x) (equal x y)))
              :hints (("Goal" :in-theory (disable alphorder))))))

Theorem: alphorder-transitive

(defthm alphorder-transitive
        (implies (and (alphorder x y)
                      (alphorder y z)
                      (not (consp x))
                      (not (consp y))
                      (not (consp z)))
                 (alphorder x z))
        :rule-classes ((:rewrite :match-free :all)))

Theorem: alphorder-total

(defthm
  alphorder-total
  (implies (and (not (consp x)) (not (consp y)))
           (or (alphorder x y) (alphorder y x)))
  :rule-classes
  ((:forward-chaining :corollary (implies (and (not (alphorder x y))
                                               (not (consp x))
                                               (not (consp y)))
                                          (alphorder y x)))))

Theorem: lexorder-reflexive

(defthm lexorder-reflexive (lexorder x x))

Theorem: lexorder-anti-symmetric

(defthm lexorder-anti-symmetric
        (implies (and (lexorder x y) (lexorder y x))
                 (equal x y))
        :rule-classes :forward-chaining)

Theorem: lexorder-transitive

(defthm lexorder-transitive
        (implies (and (lexorder x y) (lexorder y z))
                 (lexorder x z))
        :rule-classes ((:rewrite :match-free :all)))

Theorem: lexorder-total

(defthm lexorder-total
        (or (lexorder x y) (lexorder y x))
        :rule-classes
        ((:forward-chaining :corollary (implies (not (lexorder x y))
                                                (lexorder y x)))))