floor-mod-basic - ACL2 Book

Included Books

building-blocks forcing-types top floor-mod-basic-helper

other

(in-package "ACL2")

other

(table acl2-defaults-table :state-ok t)

include-book

(include-book "../basic-ops/building-blocks")

local

(local (include-book "forcing-types"))

local

(local (include-book "../basic-ops/top"))

local

(local (include-book "floor-mod-basic-helper"))

other

(set-default-hints '((nonlinearp-default-hint++ id
     stable-under-simplificationp
     hist
     nil)))

local

(local (in-theory (disable not-integerp-type-set-rules
      default-times-1
      rationalp-x
      reduce-rationalp-*
      acl2-numberp-x
      rationalp-/
      default-plus-1
      default-plus-2
      floor-positive)))

integerp-mod-1theorem

(defthm integerp-mod-1
  (implies (and (integerp x) (integerp y))
    (integerp (mod x y)))
  :rule-classes (:rewrite :type-prescription))

integerp-mod-2theorem

(defthm integerp-mod-2
  (implies (and (integerp x) (integerp (/ y)))
    (integerp (mod x y)))
  :hints (("Goal" :in-theory (enable mod floor)))
  :rule-classes (:rewrite :type-prescription))

integerp-mod-3theorem

(defthm integerp-mod-3
  (implies (integerp x) (integerp (mod x (expt 2 i))))
  :hints (("Goal" :cases ((equal i 0) (< i 0) (< 0 i))))
  :rule-classes (:rewrite :type-prescription))

local

(local (in-theory (disable integerp-mod-1 integerp-mod-2 integerp-mod-3)))

rationalp-modtheorem

(defthm rationalp-mod
  (implies (rationalp x) (rationalp (mod x y)))
  :rule-classes (:rewrite :type-prescription))

local

(local (in-theory (disable rationalp-mod)))

floor-mod-elimtheorem

(defthm floor-mod-elim
  (implies (acl2-numberp x)
    (equal (+ (mod x y) (* y (floor x y))) x))
  :rule-classes ((:rewrite) (:elim)))

linear-floor-bounds-1theorem

(defthm linear-floor-bounds-1
  (implies (real/rationalp (/ x y))
    (and (< (+ (/ x y) -1) (floor x y))
      (<= (floor x y) (/ x y))))
  :rule-classes ((:generalize) (:linear :trigger-terms ((floor x y)))))

linear-floor-bounds-2theorem

(defthm linear-floor-bounds-2
  (implies (integerp (/ x y)) (equal (floor x y) (/ x y)))
  :rule-classes ((:generalize) (:linear :trigger-terms ((floor x y)))))

linear-floor-bounds-3theorem

(defthm linear-floor-bounds-3
  (implies (and (real/rationalp (/ x y)) (not (integerp (/ x y))))
    (< (floor x y) (/ x y)))
  :rule-classes ((:generalize) (:linear :trigger-terms ((floor x y)))))

mod-bounds-1theorem

(defthm mod-bounds-1
  (implies (and (real/rationalp (/ x y)) (< 0 y))
    (and (<= 0 (mod x y)) (< (mod x y) y)))
  :rule-classes ((:generalize) (:linear))
  :otf-flg t)

mod-bounds-2theorem

(defthm mod-bounds-2
  (implies (and (real/rationalp (/ x y)) (< y 0))
    (and (<= (mod x y) 0) (< y (mod x y))))
  :rule-classes ((:generalize) (:linear))
  :otf-flg t)

mod-bounds-3theorem

(defthm mod-bounds-3
  (implies (and (acl2-numberp y) (integerp (/ x y)) (not (equal y 0)))
    (equal (mod x y) 0))
  :rule-classes ((:generalize) (:linear)))

other

(deftheory floor-bounds
  '((:linear linear-floor-bounds-1) (:linear linear-floor-bounds-2)
    (:linear linear-floor-bounds-3)))

other

(deftheory mod-bounds
  '((:linear mod-bounds-1) (:linear mod-bounds-2)
    (:linear mod-bounds-3)))

other

(deftheory floor-mod-bounds
  '((:linear linear-floor-bounds-1) (:linear linear-floor-bounds-2)
    (:linear linear-floor-bounds-3)
    (:linear mod-bounds-1)
    (:linear mod-bounds-2)
    (:linear mod-bounds-3)))

in-theory

(in-theory (disable floor mod))

floor-nonnegativetheorem

(defthm floor-nonnegative
  (implies (and (real/rationalp (/ x y)) (<= 0 (/ x y)))
    (<= 0 (floor x y)))
  :rule-classes ((:rewrite :backchain-limit-lst (3 1)) (:rewrite :backchain-limit-lst (3 1 1)
      :corollary (implies (and (real/rationalp (/ x y)) (<= 0 y) (<= 0 x))
        (<= 0 (floor x y))))
    (:rewrite :backchain-limit-lst (3 1 1)
      :corollary (implies (and (real/rationalp (/ x y)) (<= y 0) (<= x 0))
        (<= 0 (floor x y))))
    (:type-prescription :corollary (implies (and (real/rationalp (/ x y)) (<= 0 (/ x y)))
        (and (integerp (floor x y)) (<= 0 (floor x y)))))
    (:type-prescription :corollary (implies (and (real/rationalp (/ x y)) (<= 0 y) (<= 0 x))
        (and (integerp (floor x y)) (<= 0 (floor x y)))))
    (:type-prescription :corollary (implies (and (real/rationalp (/ x y)) (<= y 0) (<= x 0))
        (and (integerp (floor x y)) (<= 0 (floor x y))))))
  :hints (("Goal" :in-theory (disable |(< (* x (/ y)) 0) rationalp (* x (/ y))|
       |(< 0 (* x (/ y))) rationalp (* x (/ y))|
       |(< (* x y) 0) rationalp (* x y)|
       |(< 0 (* x y)) rationalp (* x y)|)))
  :otf-flg t)

floor-nonpositivetheorem

(defthm floor-nonpositive
  (implies (and (real/rationalp (/ x y)) (<= (/ x y) 0))
    (<= (floor x y) 0))
  :rule-classes ((:rewrite :backchain-limit-lst (3 1)) (:rewrite :backchain-limit-lst (3 1 1)
      :corollary (implies (and (real/rationalp (/ x y)) (<= 0 y) (<= x 0))
        (<= (floor x y) 0)))
    (:rewrite :backchain-limit-lst (3 1 1)
      :corollary (implies (and (real/rationalp (/ x y)) (<= y 0) (<= 0 x))
        (<= (floor x y) 0)))
    (:type-prescription :corollary (implies (and (real/rationalp (/ x y)) (<= (/ x y) 0))
        (and (integerp (floor x y)) (<= (floor x y) 0))))
    (:type-prescription :corollary (implies (and (real/rationalp (/ x y)) (<= 0 y) (<= x 0))
        (and (integerp (floor x y)) (<= (floor x y) 0))))
    (:type-prescription :corollary (implies (and (real/rationalp (/ x y)) (<= y 0) (<= 0 x))
        (and (integerp (floor x y)) (<= (floor x y) 0))))))

floor-positivetheorem

(defthm floor-positive
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (real/rationalp (/ x y)))
    (equal (< 0 (floor x y))
      (or (and (< 0 y) (<= y x)) (and (< y 0) (<= x y)))))
  :rule-classes ((:rewrite) (:rewrite :backchain-limit-lst (nil 3 1)
      :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (real/rationalp (/ x y))
          (<= 1 (/ x y)))
        (< 0 (floor x y))))
    (:rewrite :backchain-limit-lst (nil 3 1 1)
      :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (real/rationalp (/ x y))
          (< 0 y)
          (<= y x))
        (< 0 (floor x y))))
    (:rewrite :backchain-limit-lst (nil 3 1 1)
      :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (real/rationalp (/ x y))
          (< y 0)
          (<= x y))
        (< 0 (floor x y))))
    (:type-prescription :corollary (implies (and (real/rationalp (/ x y)) (<= 1 (/ x y)))
        (and (integerp (floor x y)) (< 0 (floor x y)))))
    (:type-prescription :corollary (implies (and (real/rationalp (/ x y)) (< 0 y) (<= y x))
        (and (integerp (floor x y)) (< 0 (floor x y)))))
    (:type-prescription :corollary (implies (and (real/rationalp (/ x y)) (< y 0) (<= x y))
        (and (integerp (floor x y)) (< 0 (floor x y))))))
  :otf-flg t)

floor-negativetheorem

(defthm floor-negative
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (real/rationalp (/ x y)))
    (equal (< (floor x y) 0)
      (or (and (< 0 x) (< y 0)) (and (< x 0) (< 0 y)))))
  :rule-classes ((:rewrite) (:rewrite :backchain-limit-lst (nil 3 1)
      :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (real/rationalp (/ x y))
          (< (/ x y) 0))
        (< (floor x y) 0)))
    (:rewrite :backchain-limit-lst (nil 3 1 1)
      :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (real/rationalp (/ x y))
          (< 0 x)
          (< y 0))
        (< (floor x y) 0)))
    (:rewrite :backchain-limit-lst (nil 3 1 1)
      :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (real/rationalp (/ x y))
          (< x 0)
          (< 0 y))
        (< (floor x y) 0)))
    (:type-prescription :corollary (implies (and (real/rationalp (/ x y)) (< (/ x y) 0))
        (and (integerp (floor x y)) (< (floor x y) 0))))
    (:type-prescription :corollary (implies (and (real/rationalp (/ x y)) (< 0 x) (< y 0))
        (and (integerp (floor x y)) (< (floor x y) 0))))
    (:type-prescription :corollary (implies (and (real/rationalp (/ x y)) (< x 0) (< 0 y))
        (and (integerp (floor x y)) (< (floor x y) 0)))))
  :otf-flg t)

floor-zerotheorem

(defthm floor-zero
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (acl2-numberp y)
      (real/rationalp (/ x y)))
    (equal (equal (floor x y) 0)
      (or (equal y 0)
        (and (<= 0 x) (< x y))
        (and (<= x 0) (< y x)))))
  :rule-classes ((:rewrite) (:rewrite :backchain-limit-lst (3 1)
      :corollary (implies (and (real/rationalp (/ x y)) (equal y 0))
        (equal (floor x y) 0)))
    (:rewrite :backchain-limit-lst (3 1 1)
      :corollary (implies (and (real/rationalp (/ x y)) (<= 0 (/ x y)) (< (/ x y) 1))
        (equal (floor x y) 0)))
    (:rewrite :backchain-limit-lst (3 1 1)
      :corollary (implies (and (real/rationalp (/ x y)) (<= 0 x) (< x y))
        (equal (floor x y) 0)))
    (:rewrite :backchain-limit-lst (3 1 1)
      :corollary (implies (and (real/rationalp (/ x y)) (<= x 0) (< y x))
        (equal (floor x y) 0)))
    (:type-prescription :corollary (implies (and (real/rationalp (/ x y)) (equal y 0))
        (equal (floor x y) 0)))
    (:type-prescription :corollary (implies (and (real/rationalp (/ x y)) (<= 0 (/ x y)) (< (/ x y) 1))
        (equal (floor x y) 0)))
    (:type-prescription :corollary (implies (and (real/rationalp (/ x y)) (<= 0 x) (< x y))
        (equal (floor x y) 0)))
    (:type-prescription :corollary (implies (and (real/rationalp (/ x y)) (<= x 0) (< y x))
        (equal (floor x y) 0))))
  :hints (("Goal" :cases ((< 0 (floor x y)) (< (floor x y) 0)))))

floor-x-y-=-1theorem

(defthm floor-x-y-=-1
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (real/rationalp (/ x y)))
    (equal (equal (floor x y) 1)
      (or (and (< 0 y) (<= y x) (< x (* 2 y)))
        (and (< y 0) (<= x y) (< (* 2 y) x)))))
  :rule-classes ((:rewrite) (:rewrite :backchain-limit-lst (3 1 1 1)
      :corollary (implies (and (real/rationalp (/ x y))
          (< 0 y)
          (<= y x)
          (< x (* 2 y)))
        (equal (floor x y) 1)))
    (:rewrite :backchain-limit-lst (3 1 1 1)
      :corollary (implies (and (real/rationalp (/ x y))
          (< y 0)
          (<= x y)
          (< (* 2 y) x))
        (equal (floor x y) 1))))
  :hints (("Goal" :cases ((< (floor x y) 1) (< 1 (floor x y)))) ("Subgoal 3.6" :in-theory (enable floor)))
  :otf-flg t)

floor-x-y-=--1theorem

(defthm floor-x-y-=--1
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (real/rationalp (/ x y)))
    (equal (equal (floor x y) -1)
      (or (and (< 0 y) (< x 0) (<= (- x) y))
        (and (< y 0) (< 0 x) (<= x (- y))))))
  :rule-classes ((:rewrite) (:rewrite :backchain-limit-lst (3 1 1 1)
      :corollary (implies (and (real/rationalp (/ x y)) (< 0 y) (< x 0) (<= (- x) y))
        (equal (floor x y) -1)))
    (:rewrite :backchain-limit-lst (3 1 1 1)
      :corollary (implies (and (real/rationalp (/ x y)) (< y 0) (< 0 x) (<= x (- y)))
        (equal (floor x y) -1))))
  :hints (("Goal" :cases ((< -1 (floor x y)) (< (floor x y) -1)))))

floor-=-x/ytheorem

(defthm floor-=-x/y
  (equal (equal (floor x y) (* x (/ y))) (integerp (/ x y)))
  :rule-classes ((:rewrite) (:generalize)
    (:rewrite :corollary (implies (and (equal r (/ x y)) (integerp r))
        (equal (floor x y) r)))
    (:rewrite :corollary (implies (integerp (/ x y)) (equal (floor x y) (/ x y))))
    (:rewrite :corollary (implies (equal (* x (/ y)) z)
        (equal (equal (floor x y) z) (integerp z))))))

mod-nonnegativetheorem

(defthm mod-nonnegative
  (implies (and (real/rationalp (/ x y)) (< 0 y))
    (<= 0 (mod x y)))
  :rule-classes ((:rewrite :backchain-limit-lst (3 1)) (:type-prescription :corollary (implies (and (real/rationalp x) (real/rationalp y) (< 0 y))
        (and (real/rationalp (mod x y)) (<= 0 (mod x y)))))))

mod-nonpositivetheorem

(defthm mod-nonpositive
  (implies (and (real/rationalp (/ x y)) (< y 0))
    (<= (mod x y) 0))
  :rule-classes ((:rewrite :backchain-limit-lst (3 1)) (:type-prescription :corollary (implies (and (real/rationalp x) (real/rationalp y) (< y 0))
        (and (real/rationalp (mod x y)) (<= (mod x y) 0))))))

mod-positivetheorem

(defthm mod-positive
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (acl2-numberp y)
      (real/rationalp (/ x y)))
    (equal (< 0 (mod x y))
      (or (and (equal y 0) (< 0 x))
        (and (< 0 y) (not (integerp (/ x y)))))))
  :rule-classes ((:rewrite) (:rewrite :backchain-limit-lst (nil 1 1)
      :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (equal y 0)
          (< 0 x))
        (< 0 (mod x y))))
    (:rewrite :backchain-limit-lst (nil 3 3 1)
      :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (real/rationalp (/ x y))
          (not (integerp (/ x y)))
          (< 0 y))
        (< 0 (mod x y))))
    (:type-prescription :corollary (implies (and (real/rationalp x) (equal y 0) (< 0 x))
        (and (real/rationalp (mod x y)) (< 0 (mod x y)))))
    (:type-prescription :corollary (implies (and (real/rationalp x)
          (real/rationalp y)
          (not (integerp (/ x y)))
          (< 0 y))
        (and (real/rationalp (mod x y)) (< 0 (mod x y)))))))

mod-negativetheorem

(defthm mod-negative
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (acl2-numberp y)
      (real/rationalp (/ x y)))
    (equal (< (mod x y) 0)
      (or (and (equal y 0) (< x 0))
        (and (< y 0) (not (integerp (/ x y)))))))
  :rule-classes ((:rewrite) (:rewrite :backchain-limit-lst (nil 1 1)
      :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (equal y 0)
          (< x 0))
        (< (mod x y) 0)))
    (:rewrite :backchain-limit-lst (nil 3 3 1)
      :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (real/rationalp (/ x y))
          (not (integerp (/ x y)))
          (< y 0))
        (< (mod x y) 0)))
    (:type-prescription :corollary (implies (and (real/rationalp x) (equal y 0) (< x 0))
        (and (real/rationalp (mod x y)) (< (mod x y) 0))))
    (:type-prescription :corollary (implies (and (real/rationalp y)
          (real/rationalp x)
          (not (integerp (/ x y)))
          (< y 0))
        (and (real/rationalp (mod x y)) (< (mod x y) 0))))))

mod-x-y-=-xtheorem

(defthm mod-x-y-=-x
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (acl2-numberp x)
      (acl2-numberp y)
      (real/rationalp (/ x y)))
    (equal (equal (mod x y) x)
      (or (equal y 0)
        (and (<= 0 x) (< x y))
        (and (<= x 0) (< y x)))))
  :rule-classes ((:rewrite) (:rewrite :backchain-limit-lst (1 3 1)
      :corollary (implies (and (acl2-numberp x) (real/rationalp (/ x y)) (equal y 0))
        (equal (mod x y) x)))
    (:rewrite :backchain-limit-lst (1 3 1 1)
      :corollary (implies (and (acl2-numberp x)
          (real/rationalp (/ x y))
          (<= 0 x)
          (< x y))
        (equal (mod x y) x)))
    (:rewrite :backchain-limit-lst (1 3 1 1)
      :corollary (implies (and (acl2-numberp x)
          (real/rationalp (/ x y))
          (<= x 0)
          (< y x))
        (equal (mod x y) x)))))

mod-zerotheorem

(defthm mod-zero
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (acl2-numberp x)
      (acl2-numberp y)
      (real/rationalp (/ x y)))
    (equal (equal (mod x y) 0)
      (or (equal x 0) (and (not (equal y 0)) (integerp (/ x y))))))
  :rule-classes ((:rewrite :backchain-limit-lst (1 1 3 3)
     :corollary (implies (and (acl2-numberp x)
         (acl2-numberp y)
         (real/rationalp (/ x y))
         (not (integerp (/ x y))))
       (equal (equal (mod x y) 0) (equal x 0)))) (:rewrite :backchain-limit-lst (1 3 1)
      :corollary (implies (and (acl2-numberp x) (real/rationalp (/ x y)) (equal y 0))
        (equal (equal (mod x y) 0) (equal x 0))))
    (:rewrite :backchain-limit-lst (1 3 1)
      :corollary (implies (and (acl2-numberp y) (integerp (/ x y)) (not (equal y 0)))
        (equal (mod x y) 0)))
    (:rewrite :backchain-limit-lst (3 1)
      :corollary (implies (and (real/rationalp (/ x y)) (equal x 0))
        (equal (mod x y) 0)))
    (:type-prescription :corollary (implies (and (acl2-numberp y) (integerp (/ x y)) (not (equal y 0)))
        (equal (mod x y) 0)))
    (:type-prescription :corollary (implies (and (real/rationalp (/ x y)) (equal x 0))
        (equal (mod x y) 0)))
    (:type-prescription :corollary (implies (and (real/rationalp x)
          (not (equal x 0))
          (equal y 0)
          (not (integerp (/ x y))))
        (and (real/rationalp (mod x y)) (not (equal (mod x y) 0)))))
    (:type-prescription :corollary (implies (and (real/rationalp x)
          (real/rationalp y)
          (not (equal x 0))
          (not (integerp (/ x y))))
        (and (real/rationalp (mod x y)) (not (equal (mod x y) 0)))))))

mod-zero-2theorem

(defthm mod-zero-2
  (equal (mod x x) 0)
  :hints (("Goal" :cases ((equal x 0))))
  :rule-classes (:rewrite :type-prescription))

local

(local (in-theory (disable mod-zero-2 mod-zero)))

mod-x-y-=-x+ytheorem

(defthm mod-x-y-=-x+y
  (implies (and (acl2-numberp y) (real/rationalp (/ x y)))
    (equal (equal (mod x y) (+ x y))
      (or (equal y 0)
        (and (< 0 y) (< x 0) (<= (- x) y))
        (and (< y 0) (< 0 x) (<= x (- y))))))
  :rule-classes ((:rewrite :corollary (implies (and (syntaxp (rewriting-goal-literal x mfc state))
         (acl2-numberp y)
         (real/rationalp (/ x y))
         (equal (+ x y) z))
       (equal (equal (mod x y) z)
         (or (equal y 0)
           (and (< 0 y) (< x 0) (<= (- x) y))
           (and (< y 0) (< 0 x) (<= x (- y))))))) (:rewrite :backchain-limit-lst (3 1 1 1)
      :corollary (implies (and (real/rationalp (/ x y)) (< 0 y) (< x 0) (<= (- x) y))
        (equal (mod x y) (+ x y))))
    (:rewrite :backchain-limit-lst (3 1 1 1)
      :corollary (implies (and (real/rationalp (/ x y)) (< y 0) (< 0 x) (<= x (- y)))
        (equal (mod x y) (+ x y)))))
  :hints (("Goal" :cases ((< (mod x y) (+ x y)) (< (+ x y) (mod x y))))))

mod-x-y-=-x-ytheorem

(defthm mod-x-y-=-x-y
  (implies (and (acl2-numberp y) (real/rationalp (/ x y)))
    (equal (equal (mod x y) (+ x (- y)))
      (or (equal y 0)
        (and (< 0 y) (<= y x) (< x (* 2 y)))
        (and (< y 0) (<= x y) (< (* 2 y) x)))))
  :rule-classes ((:rewrite :corollary (implies (and (syntaxp (rewriting-goal-literal x mfc state))
         (acl2-numberp y)
         (real/rationalp (/ x y))
         (equal (+ x (- y)) z))
       (equal (equal (mod x y) z)
         (or (equal y 0)
           (and (< 0 y) (<= y x) (< x (* 2 y)))
           (and (< y 0) (<= x y) (< (* 2 y) x)))))) (:rewrite :backchain-limit-lst (3 1 1 1)
      :corollary (implies (and (real/rationalp (/ x y))
          (< 0 y)
          (<= y x)
          (< x (* 2 y)))
        (equal (mod x y) (+ x (- y)))))
    (:rewrite :backchain-limit-lst (3 1 1 1)
      :corollary (implies (and (real/rationalp (/ x y))
          (< y 0)
          (<= x y)
          (< (* 2 y) x))
        (equal (mod x y) (+ x (- y))))))
  :hints (("Goal" :cases ((< (mod x y) (+ x (- y))) (< (+ x (- y)) (mod x y)))
     :in-theory (enable mod))))

|(floor x 2)|theorem

(defthm |(floor x 2)|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (integerp x))
    (equal (floor x 2)
      (if (integerp (* 1/2 x))
        (* 1/2 x)
        (+ -1/2 (* 1/2 x)))))
  :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (not (integerp (* 1/2 x))))
        (equal (floor x 2) (+ -1/2 (* 1/2 x)))))
    (:generalize :corollary (implies (integerp x)
        (or (equal (floor x 2) (* 1/2 x))
          (equal (floor x 2) (+ -1/2 (* 1/2 x))))))))

|(mod x 2)|theorem

(defthm |(mod x 2)|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (integerp x))
    (equal (mod x 2)
      (if (integerp (* 1/2 x))
        0
        1)))
  :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (not (integerp (* 1/2 x))))
        (equal (mod x 2) 1)))
    (:generalize :corollary (implies (integerp x)
        (or (equal (mod x 2) 0) (equal (mod x 2) 1))))))

|(floor (* 2 x) 1)|theorem

(defthm |(floor (* 2 x) 1)|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (real/rationalp x))
    (equal (floor (* 2 x) 1)
      (if (< (mod x 1) 1/2)
        (* 2 (floor x 1))
        (+ 1 (* 2 (floor x 1))))))
  :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (real/rationalp x)
          (< (mod x 1) 1/2))
        (equal (floor (* 2 x) 1) (* 2 (floor x 1)))))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (real/rationalp x)
          (<= 1/2 (mod x 1)))
        (equal (floor (* 2 x) 1) (+ 1 (* 2 (floor x 1))))))
    (:generalize :corollary (implies (real/rationalp x)
        (or (equal (floor (* 2 x) 1) (* 2 (floor x 1)))
          (equal (floor (* 2 x) 1) (+ 1 (* 2 (floor x 1)))))))))

|(mod (* 2 x) 1)|theorem

(defthm |(mod (* 2 x) 1)|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (real/rationalp x))
    (equal (mod (* 2 x) 1)
      (if (< (mod x 1) 1/2)
        (* 2 (mod x 1))
        (+ -1 (* 2 (mod x 1))))))
  :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (real/rationalp x)
          (< (mod x 1) 1/2))
        (equal (mod (* 2 x) 1) (* 2 (mod x 1)))))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (real/rationalp x)
          (<= 1/2 (mod x 1)))
        (equal (mod (* 2 x) 1) (+ -1 (* 2 (mod x 1))))))
    (:generalize :corollary (implies (real/rationalp x)
        (or (equal (mod (* 2 x) 1) (* 2 (mod x 1)))
          (equal (mod (* 2 x) 1) (+ -1 (* 2 (mod x 1))))))))
  :hints (("Goal" :in-theory (enable mod))))

|(floor x 0)|theorem

(defthm |(floor x 0)| (equal (floor x 0) 0))

|(floor 0 y)|theorem

(defthm |(floor 0 y)| (equal (floor 0 y) 0))

|(mod x 0)|theorem

(defthm |(mod x 0)|
  (equal (mod x 0)
    (if (acl2-numberp x)
      x
      0)))

|(mod 0 y)|theorem

(defthm |(mod 0 y)| (equal (mod 0 y) 0))

|(floor x 1)|theorem

(defthm |(floor x 1)|
  (implies (integerp x) (equal (floor x 1) x)))

|(mod x 1)|theorem

(defthm |(mod x 1)|
  (implies (integerp x) (equal (mod x 1) 0)))