• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • C
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
        • Builtin-defaxioms/defthms
          • Builtin-defthms
          • Builtin-defaxioms
          • Builtin-defaxioms/defthms-by-rule-classes
            • Builtin-defaxioms/defthms-without-rule-classes
            • Builtin-defaxioms/defthms-of-class-type-prescription
            • Builtin-defaxioms/defthms-of-class-rewrite
            • Builtin-defaxioms/defthms-of-class-forward-chaining
            • Builtin-defaxioms/defthms-of-class-definition
            • Builtin-defaxioms/defthms-of-class-congruence
            • Builtin-defaxioms/defthms-of-class-linear
            • Builtin-defaxioms/defthms-of-class-compound-recognizer
            • Builtin-defaxioms/defthms-of-class-tau-system
            • Builtin-defaxioms/defthms-of-class-equivalence
            • Builtin-defaxioms/defthms-of-class-elim
            • Builtin-defaxioms/defthms-of-class-well-founded-relation
            • Builtin-defaxioms/defthms-of-class-type-set-inverter
            • Builtin-defaxioms/defthms-of-class-rewrite-quoted-constant
            • Builtin-defaxioms/defthms-of-class-refinement
            • Builtin-defaxioms/defthms-of-class-generalize
            • Builtin-defaxioms/defthms-of-class-clause-processor
            • Builtin-defaxioms/defthms-of-class-built-in-clause
            • Builtin-defaxioms/defthms-of-class-meta
            • Builtin-defaxioms/defthms-of-class-induction
          • Builtin-defaxioms/defthms-by-types/functions
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Builtin-defaxioms/defthms-by-rule-classes

Builtin-defaxioms/defthms-of-class-linear

Built-in axioms and theorems of the :linear rule class.

Definition: char-code-linear

(defaxiom char-code-linear
  (< (char-code x) 256)
  :rule-classes :linear)

Theorem: to-df-monotonicity

(defthm to-df-monotonicity
  (implies (and (<= x y)
                (rationalp x)
                (rationalp y))
           (<= (to-df x) (to-df y)))
  :rule-classes (:linear :rewrite))

Theorem: fn-count-evg-rec-bound

(defthm fn-count-evg-rec-bound
  (< (fn-count-evg-rec evg acc calls)
     536870912)
  :rule-classes :linear)

Theorem: acl2-count-car-cdr-linear

(defthm acl2-count-car-cdr-linear
  (implies (consp x)
           (equal (acl2-count x)
                  (+ 1 (acl2-count (car x))
                     (acl2-count (cdr x)))))
  :rule-classes :linear)

Theorem: random$-linear

(defthm random$-linear
  (and (<= 0 (car (random$ n state)))
       (implies (posp n)
                (< (car (random$ n state)) n)))
  :rule-classes :linear)

Theorem: array2p-linear

(defthm array2p-linear
 (implies
  (array2p name l)
  (and
   (<
    0
    (car
     (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))))
   (<
    0
    (cadr
     (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))))
   (<
    (*
     (car
      (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))
     (cadr
      (cadr
           (assoc-keyword :dimensions (cdr (assoc-eq :header l))))))
    (cadr
        (assoc-keyword :maximum-length (cdr (assoc-eq :header l)))))
   (<=
    (cadr
         (assoc-keyword :maximum-length (cdr (assoc-eq :header l))))
    (array-maximum-length-bound))))
 :rule-classes ((:linear :match-free :all)))

Theorem: array1p-linear

(defthm array1p-linear
 (implies
  (array1p name l)
  (and
   (<
    0
    (car
     (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))))
   (<
    (car
      (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))
    (cadr
        (assoc-keyword :maximum-length (cdr (assoc-eq :header l)))))
   (<=
    (cadr
         (assoc-keyword :maximum-length (cdr (assoc-eq :header l))))
    (array-maximum-length-bound))))
 :rule-classes ((:linear :match-free :all)))

Theorem: df-round-monotonicity

(defthm df-round-monotonicity
  (implies (and (<= x y)
                (rationalp x)
                (rationalp y))
           (<= (df-round x) (df-round y)))
  :rule-classes (:linear :rewrite))

Theorem: constrained-to-df-monotonicity

(defthm constrained-to-df-monotonicity
  (implies (and (<= x y)
                (rationalp x)
                (rationalp y))
           (<= (constrained-to-df x)
               (constrained-to-df y)))
  :rule-classes (:linear :rewrite))