floor-mod - ACL2 Book

Included Books

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

other

(in-package "ACL2")

other

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

include-book

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

include-book

(include-book "../basic-ops/common")

local

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

local

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

local

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

local

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

local

(local (set-default-hints '((nonlinearp-default-hint stable-under-simplificationp
       hist
       pspv))))

local

(local (defthm acl2-count-of-cdr-weak
    (<= (acl2-count (cdr x)) (acl2-count x))
    :rule-classes ((:rewrite) (:linear))))

local

(local (defthm acl2-count-of-cdr-strong
    (implies (consp x) (< (acl2-count (cdr x)) (acl2-count x)))
    :rule-classes ((:rewrite) (:linear))))

local

(local (defthm acl2-count-of-car-weak
    (<= (acl2-count (car x)) (acl2-count x))
    :rule-classes ((:rewrite) (:linear))))

local

(local (defthm acl2-count-of-car-strong
    (implies (consp x) (< (acl2-count (car x)) (acl2-count x)))
    :rule-classes ((:rewrite) (:linear))))

local

(local (defthm acl2-count-positive-when-consp
    (implies (consp x) (< 0 (acl2-count x)))
    :rule-classes :type-prescription))

local

(local (defthm equal-of-acl2-count-of-cdr
    (implies (equal (acl2-count x) (acl2-count (cdr x)))
      (not (consp x)))
    :rule-classes :forward-chaining))

local

(local (in-theory (disable not-integerp-type-set-rules
      mod-x-y-=-x+y
      simplify-terms-such-as-ax+bx-=-0
      reduce-additive-constant-equal
      floor-zero
      floor-=-x/y
      simplify-products-gather-exponents-<
      integerp-mod-1
      integerp-mod-2
      integerp-mod-3
      expt-type-prescription-nonpositive-base-odd-exponent
      expt-type-prescription-nonpositive-base-even-exponent
      expt-type-prescription-negative-base-odd-exponent
      expt-type-prescription-negative-base-even-exponent
      expt-type-prescription-integerp-base
      expt-type-prescription-positive-base
      expt-type-prescription-integerp-base-b
      expt-type-prescription-integerp-base-a
      default-plus-1
      default-plus-2
      default-times-1
      default-times-2
      default-divide
      default-minus
      default-expt-1
      default-expt-2
      default-mod-2
      mod-positive
      mod-negative
      mod-nonpositive
      mod-x-y-=-x-y
      floor-zero
      mod-zero
      rationalp-x
      integerp-/-expt-2
      floor-positive
      floor-negative
      acl2-numberp-x
      integer-abs
      acl2-count
      numeric-constant-p
      meta-rationalp-correct
      floor-=-x/y)))

floor-recfunction

(defun floor-rec
  (x y)
  (declare (xargs :measure (abs (floor x y))
      :hints (("Goal" :in-theory (disable |(denominator (+ x r))|)))))
  (cond ((not (real/rationalp x)) t)
    ((not (real/rationalp y)) t)
    ((equal y 0) t)
    ((< y 0) (cond ((< 0 x) (1- (floor-rec (+ x y) y)))
        ((< y x) t)
        (t (1+ (floor-rec (- x y) y)))))
    (t (cond ((< x 0) (1- (floor-rec (+ x y) y)))
        ((< x y) t)
        (t (1+ (floor-rec (- x y) y)))))))

mod-recfunction

(defun mod-rec
  (x y)
  (declare (xargs :measure (abs (floor x y))
      :hints (("Goal" :in-theory (disable |(denominator (+ x r))|)))))
  (cond ((not (real/rationalp x)) t)
    ((not (real/rationalp y)) t)
    ((equal y 0) t)
    ((< y 0) (cond ((< 0 x) (mod-rec (+ x y) y))
        ((< y x) t)
        (t (mod-rec (- x y) y))))
    (t (cond ((< x 0) (mod-rec (+ x y) y))
        ((< x y) t)
        (t (mod-rec (- x y) y))))))

floor-indtheorem

(defthm floor-ind
  t
  :rule-classes ((:induction :pattern (floor x y) :scheme (floor-rec x y))))

mod-indtheorem

(defthm mod-ind
  t
  :rule-classes ((:induction :pattern (mod x y) :scheme (mod-rec x y))))

in-theory

(in-theory (disable floor-ind mod-ind))

justify-floor-recursiontheorem

(defthm justify-floor-recursion
  (and (implies (and (< 0 x) (real/rationalp y) (< 1 y))
      (< (floor x y) x))
    (implies (and (< x -1) (real/rationalp y) (<= 2 y))
      (< x (floor x y))))
  :hints (("Subgoal 1.2.2" :cases ((< i -1))))
  :otf-flg t)

|(floor (+ x y) z)|theorem

(defthm |(floor (+ x y) z)|
  (implies (and (real/rationalp (/ x z)) (real/rationalp (/ y z)))
    (equal (floor (+ x y) z)
      (cond ((not (acl2-numberp z)) 0)
        ((equal z 0) 0)
        ((< 0 z) (if (< (+ (mod x z) (mod y z)) z)
            (+ (floor x z) (floor y z))
            (+ 1 (floor x z) (floor y z))))
        (t (if (< z (+ (mod x z) (mod y z)))
            (+ (floor x z) (floor y z))
            (+ 1 (floor x z) (floor y z))))))))

|(floor (+ x y) z) rewriting goal literal|theorem

(defthm |(floor (+ x y) z) rewriting goal literal|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (real/rationalp (/ x z))
      (real/rationalp (/ y z)))
    (equal (floor (+ x y) z)
      (cond ((not (acl2-numberp z)) 0)
        ((equal z 0) 0)
        ((< 0 z) (if (< (+ (mod x z) (mod y z)) z)
            (+ (floor x z) (floor y z))
            (+ 1 (floor x z) (floor y z))))
        (t (if (< z (+ (mod x z) (mod y z)))
            (+ (floor x z) (floor y z))
            (+ 1 (floor x z) (floor y z))))))))

not-too-many-addends-1function

(defun not-too-many-addends-1
  (x n)
  (cond ((< 3 n) nil)
    ((eq (fn-symb x) 'binary-+) (not-too-many-addends-1 (arg2 x) (+ 1 n)))
    (t t)))

not-too-many-addendsfunction

(defun not-too-many-addends
  (x)
  (not-too-many-addends-1 x 0))

|(floor (+ x y) z) where (< z 0)|theorem

(defthm |(floor (+ x y) z) where (< z 0)|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (not-too-many-addends y))
      (real/rationalp (/ x z))
      (real/rationalp (/ y z))
      (< z 0))
    (equal (floor (+ x y) z)
      (if (< z (+ (mod x z) (mod y z)))
        (+ (floor x z) (floor y z))
        (+ 1 (floor x z) (floor y z)))))
  :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (syntaxp (not-too-many-addends y))
          (real/rationalp (/ x z))
          (real/rationalp (/ y z))
          (< z 0)
          (< z (+ (mod x z) (mod y z))))
        (equal (floor (+ x y) z) (+ (floor x z) (floor y z)))))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (syntaxp (not-too-many-addends y))
          (real/rationalp (/ x z))
          (real/rationalp (/ y z))
          (< z 0)
          (<= (+ (mod x z) (mod y z)) z))
        (equal (floor (+ x y) z) (+ 1 (floor x z) (floor y z)))))))

|(floor (+ x y) z) where (< 0 z)|theorem

(defthm |(floor (+ x y) z) where (< 0 z)|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (not-too-many-addends y))
      (real/rationalp (/ x z))
      (real/rationalp (/ y z))
      (< 0 z))
    (equal (floor (+ x y) z)
      (if (< (+ (mod x z) (mod y z)) z)
        (+ (floor x z) (floor y z))
        (+ 1 (floor x z) (floor y z)))))
  :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (syntaxp (not-too-many-addends y))
          (real/rationalp (/ x z))
          (real/rationalp (/ y z))
          (< 0 z)
          (< (+ (mod x z) (mod y z)) z))
        (equal (floor (+ x y) z) (+ (floor x z) (floor y z)))))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (syntaxp (not-too-many-addends y))
          (real/rationalp (/ x z))
          (real/rationalp (/ y z))
          (< 0 z)
          (<= z (+ (mod x z) (mod y z))))
        (equal (floor (+ x y) z) (+ 1 (floor x z) (floor y z)))))))

in-theory

(in-theory (disable |(floor (+ x y) z)|
    |(floor (+ x y) z) rewriting goal literal|))

|(floor (+ 1 x) y)|theorem

(defthm |(floor (+ 1 x) y)|
  (implies (and (real/rationalp x) (real/rationalp y) (< 1 y))
    (equal (floor (+ 1 x) y)
      (if (< (+ 1 (mod x y)) y)
        (floor x y)
        (+ 1 (floor x y)))))
  :hints (("Goal" :in-theory (enable |(floor (+ x y) z)|))))

|(mod (+ x y) z)|theorem

(defthm |(mod (+ x y) z)|
  (implies (and (real/rationalp (/ x z)) (real/rationalp (/ y z)))
    (equal (mod (+ x y) z)
      (if (<= 0 z)
        (if (< (+ (mod x z) (mod y z)) z)
          (+ (mod x z) (mod y z))
          (+ (mod x z) (mod y z) (- z)))
        (if (< z (+ (mod x z) (mod y z)))
          (+ (mod x z) (mod y z))
          (+ (mod x z) (mod y z) (- z)))))))

|(mod (+ x y) z) rewriting goal literal|theorem

(defthm |(mod (+ x y) z) rewriting goal literal|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (real/rationalp (/ x z))
      (real/rationalp (/ y z)))
    (equal (mod (+ x y) z)
      (if (<= 0 z)
        (if (< (+ (mod x z) (mod y z)) z)
          (+ (mod x z) (mod y z))
          (+ (mod x z) (mod y z) (- z)))
        (if (< z (+ (mod x z) (mod y z)))
          (+ (mod x z) (mod y z))
          (+ (mod x z) (mod y z) (- z)))))))

|(mod (+ x y) z) where (<= z 0)|theorem

(defthm |(mod (+ x y) z) where (<= z 0)|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (not-too-many-addends y))
      (real/rationalp (/ x z))
      (real/rationalp (/ y z))
      (<= z 0))
    (equal (mod (+ x y) z)
      (if (< z (+ (mod x z) (mod y z)))
        (+ (mod x z) (mod y z))
        (+ (mod x z) (mod y z) (- z)))))
  :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (syntaxp (not-too-many-addends y))
          (real/rationalp (/ x z))
          (real/rationalp (/ y z))
          (<= z 0)
          (< z (+ (mod x z) (mod y z))))
        (equal (mod (+ x y) z) (+ (mod x z) (mod y z)))))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (syntaxp (not-too-many-addends y))
          (real/rationalp (/ x z))
          (real/rationalp (/ y z))
          (<= z 0)
          (<= (+ (mod x z) (mod y z)) z))
        (equal (mod (+ x y) z) (+ (mod x z) (mod y z) (- z)))))))

|(mod (+ x y) z) where (<= 0 z)|theorem

(defthm |(mod (+ x y) z) where (<= 0 z)|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (not-too-many-addends y))
      (real/rationalp (/ x z))
      (real/rationalp (/ y z))
      (<= 0 z))
    (equal (mod (+ x y) z)
      (if (< (+ (mod x z) (mod y z)) z)
        (+ (mod x z) (mod y z))
        (+ (mod x z) (mod y z) (- z)))))
  :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (syntaxp (not-too-many-addends y))
          (real/rationalp (/ x z))
          (real/rationalp (/ y z))
          (<= 0 z)
          (< (+ (mod x z) (mod y z)) z))
        (equal (mod (+ x y) z) (+ (mod x z) (mod y z)))))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (syntaxp (not-too-many-addends y))
          (real/rationalp (/ x z))
          (real/rationalp (/ y z))
          (<= 0 z)
          (<= z (+ (mod x z) (mod y z))))
        (equal (mod (+ x y) z) (+ (mod x z) (mod y z) (- z)))))))

in-theory

(in-theory (disable |(mod (+ x y) z)|
    |(mod (+ x y) z) rewriting goal literal|))

|(mod (+ 1 x) y)|theorem

(defthm |(mod (+ 1 x) y)|
  (implies (and (real/rationalp x) (real/rationalp y) (< 1 y))
    (equal (mod (+ 1 x) y)
      (if (< (+ 1 (mod x y)) y)
        (+ 1 (mod x y))
        (+ 1 (mod x y) (- y)))))
  :hints (("Goal" :in-theory (enable |(mod (+ x y) z)|))))

find-divisive-factorfunction

(defun find-divisive-factor
  (x simplep mfc state)
  (declare (xargs :guard t))
  (cond ((variablep x) nil)
    ((fquotep x) (if (consp (cdr x))
        (let ((c (unquote x)))
          (if (and (real/rationalp c) (not (equal 0 c)) (< (abs c) 1))
            (list (cons 'factor (invert-match x)))
            nil))
        nil))
    ((eq (ffn-symb x) 'expt) (cond ((eq (fn-symb (arg1 x)) 'unary-/) (let ((inv (invert-match x)))
            (if (and (if simplep
                  t
                  (proveably-non-zero 'x `((x . ,INV)) mfc state))
                (stable-under-rewriting-products inv mfc state))
              (list (cons 'factor inv))
              nil)))
        ((quotep (arg1 x)) (if (consp (cdr (arg1 x)))
            (let ((c (unquote (arg1 x))))
              (if (and (real/rationalp c)
                  (not (equal 0 c))
                  (or (< (abs c) 1)
                    (eq (fn-symb (arg2 x)) 'unary--)
                    (and (eq (fn-symb (arg2 x)) 'binary-*)
                      (rational-constant-p (arg1 (arg2 x)))
                      (< (unquote (arg1 (arg2 x))) 0)))
                  (stable-under-rewriting-products (invert-match x) mfc state))
                (list (cons 'factor (invert-match x)))
                nil))
            nil))
        ((eq (fn-symb (arg2 x)) 'unary--) (let ((inv (invert-match x)))
            (if (and (if simplep
                  t
                  (proveably-non-zero 'x `((x . ,INV)) mfc state))
                (stable-under-rewriting-products inv mfc state))
              (list (cons 'factor inv))
              nil)))
        ((and (eq (fn-symb (arg2 x)) 'binary-*)
           (rational-constant-p (arg1 (arg2 x)))
           (< (unquote (arg1 (arg2 x))) 0)) (let ((inv (invert-match x)))
            (if (and (if simplep
                  t
                  (proveably-non-zero 'x `((x . ,INV)) mfc state))
                (stable-under-rewriting-products inv mfc state))
              (list (cons 'factor inv))
              nil)))
        (t nil)))
    ((eq (ffn-symb x) 'unary-/) (let ((inv (invert-match x)))
        (if (and (if simplep
              t
              (proveably-non-zero 'x `((x . ,INV)) mfc state))
            (stable-under-rewriting-products inv mfc state))
          (list (cons 'factor inv))
          nil)))
    ((eq (ffn-symb x) 'binary-*) (let ((temp (find-divisive-factor (arg1 x) simplep mfc state)))
        (if temp
          temp
          (find-divisive-factor (arg2 x) simplep mfc state))))
    (t nil)))

|(floor (* x (/ y)) z) not rewriting-goal-literal|theorem

(defthm |(floor (* x (/ y)) z) not rewriting-goal-literal|
  (implies (and (syntaxp (not (quotep x)))
      (syntaxp (not (rewriting-goal-literal x mfc state)))
      (syntaxp (in-term-order-* x mfc state))
      (syntaxp (in-term-order-* y mfc state))
      (real/rationalp (/ x y))
      (bind-free (find-divisive-factor x nil mfc state) (factor))
      (acl2-numberp factor)
      (not (equal 0 factor)))
    (equal (floor x y) (floor (* factor x) (* factor y)))))

|(floor (* x (/ y)) z) rewriting-goal-literal|theorem

(defthm |(floor (* x (/ y)) z) rewriting-goal-literal|
  (implies (and (syntaxp (not (quotep x)))
      (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (in-term-order-* x mfc state))
      (syntaxp (in-term-order-* y mfc state))
      (real/rationalp (/ x y))
      (bind-free (find-divisive-factor x t mfc state) (factor))
      (acl2-numberp factor)
      (case-split (not (equal 0 factor))))
    (equal (floor x y) (floor (* factor x) (* factor y)))))

|(floor x (* y (/ z))) not rewriting-goal-literal|theorem

(defthm |(floor x (* y (/ z))) not rewriting-goal-literal|
  (implies (and (syntaxp (not (quotep y)))
      (syntaxp (not (rewriting-goal-literal x mfc state)))
      (syntaxp (in-term-order-* x mfc state))
      (syntaxp (in-term-order-* y mfc state))
      (real/rationalp (/ x y))
      (bind-free (find-divisive-factor y nil mfc state) (factor))
      (acl2-numberp factor)
      (not (equal 0 factor)))
    (equal (floor x y) (floor (* factor x) (* factor y)))))

|(floor x (* y (/ z))) rewriting-goal-literal|theorem

(defthm |(floor x (* y (/ z))) rewriting-goal-literal|
  (implies (and (syntaxp (not (quotep y)))
      (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (in-term-order-* x mfc state))
      (syntaxp (in-term-order-* y mfc state))
      (real/rationalp (/ x y))
      (bind-free (find-divisive-factor y t mfc state) (factor))
      (acl2-numberp factor)
      (case-split (not (equal 0 factor))))
    (equal (floor x y) (floor (* factor x) (* factor y)))))

|(mod (* x (/ y)) z) not rewriting-goal-literal|theorem

(defthm |(mod (* x (/ y)) z) not rewriting-goal-literal|
  (implies (and (syntaxp (not (quotep x)))
      (syntaxp (not (rewriting-goal-literal x mfc state)))
      (syntaxp (in-term-order-* x mfc state))
      (syntaxp (in-term-order-* y mfc state))
      (real/rationalp (/ x y))
      (bind-free (find-divisive-factor x nil mfc state) (factor))
      (acl2-numberp factor)
      (not (equal 0 factor)))
    (equal (mod x y)
      (* (/ factor) (mod (* factor x) (* factor y)))))
  :hints (("Goal" :in-theory (enable mod))))

|(mod (* x (/ y)) z) rewriting-goal-literal|theorem

(defthm |(mod (* x (/ y)) z) rewriting-goal-literal|
  (implies (and (syntaxp (not (quotep x)))
      (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (in-term-order-* x mfc state))
      (syntaxp (in-term-order-* y mfc state))
      (real/rationalp (/ x y))
      (bind-free (find-divisive-factor x t mfc state) (factor))
      (acl2-numberp factor)
      (case-split (not (equal 0 factor))))
    (equal (mod x y)
      (* (/ factor) (mod (* factor x) (* factor y)))))
  :hints (("Goal" :in-theory (enable mod))))

|(mod x (* y (/ z))) not rewriting-goal-literal|theorem

(defthm |(mod x (* y (/ z))) not rewriting-goal-literal|
  (implies (and (syntaxp (not (quotep y)))
      (syntaxp (not (rewriting-goal-literal x mfc state)))
      (syntaxp (in-term-order-* x mfc state))
      (syntaxp (in-term-order-* y mfc state))
      (real/rationalp (/ x y))
      (bind-free (find-divisive-factor y nil mfc state) (factor))
      (acl2-numberp factor)
      (not (equal 0 factor)))
    (equal (mod x y)
      (* (/ factor) (mod (* factor x) (* factor y)))))
  :hints (("Goal" :in-theory (enable mod))))

|(mod x (* y (/ z))) rewriting-goal-literal|theorem

(defthm |(mod x (* y (/ z))) rewriting-goal-literal|
  (implies (and (syntaxp (not (quotep y)))
      (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (in-term-order-* x mfc state))
      (syntaxp (in-term-order-* y mfc state))
      (real/rationalp (/ x y))
      (bind-free (find-divisive-factor y t mfc state) (factor))
      (acl2-numberp factor)
      (case-split (not (equal 0 factor))))
    (equal (mod x y)
      (* (/ factor) (mod (* factor x) (* factor y)))))
  :hints (("Goal" :in-theory (enable mod))))

|(floor (- x) y)|theorem

(defthm |(floor (- x) y)|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (mostly-negative-addends-p x mfc state))
      (real/rationalp (/ x y)))
    (equal (floor x y)
      (if (integerp (* x (/ y)))
        (* x (/ y))
        (+ -1 (- (floor (- x) y))))))
  :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (syntaxp (mostly-negative-addends-p x mfc state))
          (real/rationalp (/ x y))
          (not (integerp (* x (/ y)))))
        (equal (floor x y) (+ -1 (- (floor (- x) y))))))))

|(floor x (- y))|theorem

(defthm |(floor x (- y))|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (mostly-negative-addends-p y mfc state))
      (real/rationalp (/ x y)))
    (equal (floor x y)
      (if (integerp (* x (/ y)))
        (* x (/ y))
        (+ -1 (- (floor x (- y)))))))
  :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (syntaxp (mostly-negative-addends-p x mfc state))
          (real/rationalp (/ x y))
          (not (integerp (* x (/ y)))))
        (equal (floor x y) (+ -1 (- (floor x (- y)))))))))

|(mod (- x) y)|theorem

(defthm |(mod (- x) y)|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (mostly-negative-addends-p x mfc state))
      (real/rationalp (/ x y)))
    (equal (mod x y)
      (if (integerp (/ x y))
        (- (mod (- x) y))
        (+ y (- (mod (- x) y))))))
  :hints (("Goal" :in-theory (enable mod)))
  :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (syntaxp (mostly-negative-addends-p x mfc state))
          (integerp (* x (/ y))))
        (equal (mod x y) (- (mod (- x) y)))))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (syntaxp (mostly-negative-addends-p x mfc state))
          (real/rationalp (/ x y))
          (not (integerp (* x (/ y)))))
        (equal (mod x y) (+ y (- (mod (- x) y))))))))

|(mod x (- y))|theorem

(defthm |(mod x (- y))|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (mostly-negative-addends-p y mfc state))
      (real/rationalp (/ x y)))
    (equal (mod x y)
      (if (integerp (/ x y))
        (mod x (- y))
        (+ y (mod x (- y))))))
  :hints (("Goal" :in-theory (enable mod)))
  :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (syntaxp (mostly-negative-addends-p y mfc state))
          (integerp (* x (/ y))))
        (equal (mod x y) (mod x (- y)))))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (syntaxp (mostly-negative-addends-p y mfc state))
          (real/rationalp (/ x y))
          (not (integerp (* x (/ y)))))
        (equal (mod x y) (+ y (mod x (- y))))))))

|(floor (mod x y) z)|theorem

(defthm |(floor (mod x y) z)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (real/rationalp z)
      (equal i (/ y z))
      (integerp (* i (floor x y))))
    (equal (floor (mod x y) z)
      (- (floor x z) (* i (floor x y))))))

|(mod (mod x y) z)|encapsulate

(encapsulate nil
  (local (in-theory (enable floor-=-x/y)))
  (defthm |(mod (mod x y) z)|
    (implies (and (syntaxp (rewriting-goal-literal x mfc state))
        (real/rationalp y)
        (real/rationalp z)
        (equal i (/ y z))
        (integerp (* i (floor x y))))
      (equal (mod (mod x y) z)
        (if (equal z 0)
          (mod x y)
          (mod x z))))
    :hints (("Goal" :cases ((real/rationalp x)) :in-theory (enable mod)))
    :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
            (real/rationalp y)
            (equal z 0))
          (equal (mod (mod x y) z) (mod x y))))
      (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
            (real/rationalp y)
            (real/rationalp z)
            (not (equal z 0))
            (equal i (/ y z))
            (integerp (* i (floor x y))))
          (equal (mod (mod x y) z) (mod x z)))))))

|(mod (floor x y) z)|encapsulate

(encapsulate nil
  (local (in-theory (enable floor-zero floor-=-x/y mod-x-y-=-x+y)))
  (local (in-theory (disable mod-zero
        default-plus-1
        default-plus-2
        default-times-1
        default-times-2
        linear-floor-bounds-1
        linear-floor-bounds-2
        (:rewrite mod-x-y-=-x+y . 1)
        (:type-prescription floor-nonnegative . 1)
        (:type-prescription floor-nonpositive . 1)
        (:type-prescription floor-nonpositive . 2)
        (:type-prescription mod-nonnegative)
        (:type-prescription rationalp-mod)
        (:type-prescription floor-zero . 4)
        (:type-prescription floor-zero . 3)
        (:type-prescription floor-zero . 1)
        (:rewrite default-mod-ratio)
        (:type-prescription not-integerp-2a)
        (:rewrite floor-=-x/y . 2)
        (:rewrite normalize-factors-gather-exponents)
        (:rewrite default-less-than-1)
        (:rewrite default-less-than-2)
        (:meta meta-integerp-correct)
        (:rewrite |(< (/ x) 0)|)
        (:rewrite mod-x-y-=-x . 2)
        (:rewrite normalize-terms-such-as-1/ax+bx)
        (:rewrite reduce-rational-multiplicative-constant-<)
        (:rewrite reduce-multiplicative-constant-<)
        (:rewrite reduce-additive-constant-<)
        (:rewrite |(< c (/ x)) positive c --- present in goal|)
        (:rewrite |(< c (/ x)) positive c --- obj t or nil|)
        (:rewrite |(< c (/ x)) negative c --- present in goal|)
        (:rewrite |(< c (/ x)) negative c --- obj t or nil|)
        (:rewrite |(< (/ x) c) positive c --- present in goal|)
        (:rewrite |(< (/ x) c) positive c --- obj t or nil|)
        (:rewrite |(< (/ x) c) negative c --- present in goal|)
        (:rewrite |(< (/ x) c) negative c --- obj t or nil|)
        (:rewrite |(< (/ x) (/ y))|)
        (:rewrite |(< (- x) (- y))|)
        (:rewrite integerp-<-constant)
        (:rewrite constant-<-integerp)
        (:rewrite |(< c (- x))|)
        (:rewrite |(< (- x) c)|)
        (:rewrite floor-x-y-=-1 . 3)
        (:rewrite floor-x-y-=-1 . 2)
        (:rewrite default-floor-ratio)
        (:type-prescription not-integerp-1a)
        (:linear linear-floor-bounds-3)
        (:rewrite |(mod x (* y (/ z))) rewriting-goal-literal|)
        (:rewrite normalize-terms-such-as-a/a+b-+-b/a+b)
        (:rewrite arith-normalize-factors-scatter-exponents)
        (:rewrite |(< (* x y) 0)|)
        (:rewrite simplify-terms-such-as-ax+bx-<-0-rational-remainder)
        (:rewrite simplify-terms-such-as-ax+bx-<-0-rational-common)
        (:rewrite |(< 0 (/ x))|)
        (:rewrite |(< 0 (* x y))|)
        (:rewrite simplify-terms-such-as-0-<-ax+bx-rational-remainder)
        (:rewrite simplify-terms-such-as-0-<-ax+bx-rational-common)
        (:rewrite floor-zero . 2)
        (:rewrite |arith (* c (* d x))|)
        (:rewrite integerp-minus-x)
        (:rewrite |(equal (- x) (- y))|)
        (:rewrite reduce-multiplicative-constant-equal)
        (:rewrite |(equal c (/ x))|)
        (:rewrite |(equal (/ x) (/ y))|)
        (:rewrite equal-of-predicates-rewrite)
        (:rewrite |(equal c (- x))|)
        (:rewrite |(equal (- x) c)|)
        (:rewrite |(* c (* d x))|)
        (:rewrite default-mod-1)
        (:rewrite |(< (* x y) 0) rationalp (* x y)|)
        (:rewrite |(< 0 (* x y)) rationalp (* x y)|)
        (:rewrite |(floor x (* y (/ z))) rewriting-goal-literal|)
        (:rewrite |(floor (* x (/ y)) z) rewriting-goal-literal|)
        (:rewrite |(mod x (- y))| . 3)
        (:rewrite |(mod x (- y))| . 2)
        (:rewrite |(mod x (- y))| . 1)
        (:rewrite |(mod x (* y (/ z))) not rewriting-goal-literal|)
        (:rewrite |(mod (- x) y)| . 2)
        (:rewrite |(mod (- x) y)| . 1)
        (:rewrite |(mod (* x (/ y)) z) not rewriting-goal-literal|)
        (:type-prescription floor-zero . 2))))
  (defthm |(mod (floor x y) z)|
    (implies (and (syntaxp (rewriting-goal-literal x mfc state))
        (real/rationalp x)
        (integerp y)
        (integerp z))
      (equal (mod (floor x y) z)
        (cond ((integerp (* x (/ y))) (* (/ y) (mod x (* y z))))
          ((and (< z 0) (integerp (* (/ z) (floor x y)))) (+ (- z) (floor x y) (- (* z (floor x (* y z))))))
          (t (+ (floor x y) (- (* z (floor x (* y z)))))))))
    :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
            (real/rationalp x)
            (integerp y)
            (integerp z)
            (< z 0)
            (not (integerp (* x (/ y))))
            (integerp (* (/ z) (floor x y))))
          (equal (mod (floor x y) z)
            (+ (- z) (floor x y) (- (* z (floor x (* y z))))))))
      (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
            (real/rationalp x)
            (integerp y)
            (integerp z)
            (<= 0 z))
          (equal (mod (floor x y) z)
            (+ (floor x y) (- (* z (floor x (* y z))))))))
      (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
            (real/rationalp x)
            (integerp y)
            (integerp z)
            (integerp (* x (/ y))))
          (equal (mod (floor x y) z) (* (/ y) (mod x (* y z))))))
      (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
            (real/rationalp x)
            (integerp y)
            (integerp z)
            (not (integerp (* (/ z) (floor x y)))))
          (equal (mod (floor x y) z)
            (+ (floor x y) (- (* z (floor x (* y z)))))))))))

|(floor (floor x y) z)|encapsulate

(encapsulate nil
  (local (in-theory (enable floor-zero floor-=-x/y mod-x-y-=-x+y)))
  (local (in-theory (disable (:rewrite floor-=-x/y . 2)
        (:rewrite floor-zero . 5)
        (:rewrite floor-zero . 4)
        (:type-prescription floor-zero . 4)
        (:rewrite normalize-factors-gather-exponents)
        (:rewrite default-mod-ratio)
        (:type-prescription floor-zero . 3)
        (:rewrite floor-x-y-=-1 . 2)
        (:type-prescription floor-zero . 1)
        (:type-prescription floor-nonnegative . 1)
        (:rewrite floor-x-y-=-1 . 3)
        (:rewrite default-floor-ratio)
        (:rewrite default-less-than-1)
        (:meta meta-integerp-correct)
        (:rewrite default-less-than-2)
        (:type-prescription floor-nonpositive . 1)
        (:rewrite |(< (/ x) 0)|)
        (:rewrite normalize-terms-such-as-1/ax+bx)
        (:rewrite reduce-rational-multiplicative-constant-<)
        (:rewrite reduce-multiplicative-constant-<)
        (:rewrite |(< c (/ x)) positive c --- present in goal|)
        (:rewrite |(< c (/ x)) positive c --- obj t or nil|)
        (:rewrite |(< c (/ x)) negative c --- present in goal|)
        (:rewrite |(< c (/ x)) negative c --- obj t or nil|)
        (:rewrite |(< (/ x) c) positive c --- present in goal|)
        (:rewrite |(< (/ x) c) positive c --- obj t or nil|)
        (:rewrite |(< (/ x) c) negative c --- present in goal|)
        (:rewrite |(< (/ x) c) negative c --- obj t or nil|)
        (:rewrite |(< (/ x) (/ y))|)
        (:rewrite |(< (- x) (- y))|)
        (:rewrite integerp-<-constant)
        (:rewrite constant-<-integerp)
        (:rewrite |(< c (- x))|)
        (:rewrite |(< (- x) c)|)
        (:linear linear-floor-bounds-2)
        (:rewrite normalize-terms-such-as-a/a+b-+-b/a+b)
        (:rewrite floor-zero . 2)
        (:rewrite simplify-products-gather-exponents-equal)
        (:rewrite prefer-positive-addends-equal)
        (:rewrite integerp-minus-x)
        (:rewrite |arith (* c (* d x))|)
        (:rewrite |(< (* x y) 0)|)
        (:rewrite simplify-terms-such-as-ax+bx-<-0-rational-remainder)
        (:rewrite simplify-terms-such-as-ax+bx-<-0-rational-common)
        (:rewrite |(* c (* d x))|)
        (:rewrite mod-x-y-=-x . 2)
        (:rewrite |(< 0 (/ x))|)
        (:rewrite |(< 0 (* x y))|)
        (:rewrite |arith (* c (* d x))|)
        (:rewrite simplify-terms-such-as-0-<-ax+bx-rational-remainder)
        (:rewrite simplify-terms-such-as-0-<-ax+bx-rational-common)
        (:rewrite |(equal (/ x) c)|)
        (:rewrite default-floor-1)
        (:rewrite reduce-multiplicative-constant-equal)
        (:rewrite |(equal c (/ x))|)
        (:rewrite |(equal (/ x) (/ y))|)
        (:rewrite |(equal (- x) (- y))|)
        (:rewrite |(equal c (- x))|)
        (:rewrite |(< (* x y) 0) rationalp (* x y)|)
        (:rewrite |(floor x (* y (/ z))) rewriting-goal-literal|)
        (:rewrite |arith (* (- x) y)|)
        (:rewrite |(< 0 (* x y)) rationalp (* x y)|)
        (:rewrite |(floor x (* y (/ z))) not rewriting-goal-literal|)
        (:rewrite |(floor (* x (/ y)) z) not rewriting-goal-literal|)
        (:rewrite |arith (- (* c x))|))))
  (defthm |(floor (floor x y) z)|
    (implies (and (syntaxp (rewriting-goal-literal x mfc state))
        (real/rationalp x)
        (integerp y)
        (integerp z))
      (equal (floor (floor x y) z)
        (cond ((and (< z 0)
             (not (integerp (/ x y)))
             (integerp (/ (floor x y) z))) (+ 1 (floor x (* y z))))
          (t (floor x (* y z))))))
    :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
            (real/rationalp x)
            (integerp y)
            (integerp z)
            (< z 0)
            (not (integerp (/ x y)))
            (integerp (/ (floor x y) z)))
          (equal (floor (floor x y) z) (+ 1 (floor x (* y z))))))
      (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
            (real/rationalp x)
            (integerp y)
            (integerp z)
            (<= 0 z))
          (equal (floor (floor x y) z) (floor x (* y z)))))
      (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
            (real/rationalp x)
            (integerp y)
            (integerp z)
            (integerp (/ x y)))
          (equal (floor (floor x y) z) (floor x (* y z)))))
      (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
            (real/rationalp x)
            (integerp y)
            (integerp z)
            (not (integerp (/ (floor x y) z))))
          (equal (floor (floor x y) z) (floor x (* y z))))))))

mod-+-cancel-0-fn-1function

(defun mod-+-cancel-0-fn-1
  (x z)
  (declare (xargs :guard (and (pseudo-termp x) (eq (fn-symb x) 'binary-+))))
  (cond ((equal (fargn x 1) z) t)
    ((eq (fn-symb (fargn x 2)) 'binary-+) (mod-+-cancel-0-fn-1 (fargn x 2) z))
    ((equal (fargn x 2) z) t)
    (t nil)))

mod-+-cancel-0-fnfunction

(defun mod-+-cancel-0-fn
  (x z)
  (declare (xargs :guard (pseudo-termp x)))
  (if (and (eq (fn-symb x) 'binary-+)
      (not (eq (fn-symb z) 'binary-+)))
    (mod-+-cancel-0-fn-1 x z)
    nil))

|(equal (mod (+ x y) z) x)|encapsulate

(encapsulate nil
  (local (in-theory (enable not-integerp-1b
        not-integerp-2b
        not-integerp-2a
        not-integerp-1a)))
  (defthm |(equal (mod (+ x y) z) x)|
    (implies (and (real/rationalp x)
        (real/rationalp y)
        (syntaxp (mod-+-cancel-0-fn x z)))
      (equal (equal (mod x y) z)
        (and (equal (mod (- x z) y) 0) (equal (mod z y) z))))
    :hints (("Goal" :cases ((real/rationalp z))))))

floor-+-cancel-0-fn-2function

(defun floor-+-cancel-0-fn-2
  (x y z mfc state)
  (declare (xargs :guard t))
  (let ((neg-x (negate-match x)))
    (and (equal (mfc-rw+ '(equal (unary-- (binary-* neg-x (unary-/ y))) z)
          `((neg-x . ,NEG-X) (y . ,Y) (z . ,Z))
          t
          t
          mfc
          state)
        *t*)
      (stable-under-rewriting-sums neg-x mfc state))))

floor-+-cancel-0-fn-1function

(defun floor-+-cancel-0-fn-1
  (x y z mfc state)
  (declare (xargs :guard (and (pseudo-termp x) (eq (fn-symb x) 'binary-+))))
  (cond ((floor-+-cancel-0-fn-2 (fargn x 1) y z mfc state) (list (cons 'addend (negate-match (fargn x 1)))))
    ((eq (fn-symb (fargn x 2)) 'binary-+) (floor-+-cancel-0-fn-1 (fargn x 2) y z mfc state))
    ((floor-+-cancel-0-fn-2 (fargn x 2) y z mfc state) (list (cons 'addend (negate-match (fargn x 2)))))
    (t nil)))

floor-+-cancel-0-fnfunction

(defun floor-+-cancel-0-fn
  (x y z mfc state)
  (declare (xargs :guard (pseudo-termp x)))
  (if (and (eq (fn-symb x) 'binary-+)
      (not (eq (fn-symb z) 'binary-+)))
    (floor-+-cancel-0-fn-1 x y z mfc state)
    nil))

local

(local (defthm crock-529
    (implies (and (real/rationalp (/ x z)) (real/rationalp (/ y z)))
      (equal (equal (floor (+ x y) z) (/ x z))
        (and (integerp (/ x z)) (equal (floor y z) 0))))
    :hints (("Goal" :cases ((< 0 z) (< z 0))))
    :rule-classes nil))

|(equal (floor (+ x y) z) x)|theorem

(defthm |(equal (floor (+ x y) z) x)|
  (implies (and (real/rationalp (/ x y))
      (syntaxp (in-term-order-+ x mfc state))
      (bind-free (floor-+-cancel-0-fn x y z mfc state) (addend))
      (equal (- (/ addend y)) z))
    (equal (equal (floor x y) z)
      (and (integerp (/ addend y))
        (equal (floor (+ addend x) y) 0))))
  :hints (("Goal" :in-theory (disable floor-zero)
     :use (:instance crock-529 (x addend) (y (+ addend x)) (z y)))))

get-the-ens-dangerouslyfunction

(defun get-the-ens-dangerously
  (mfc)
  (let ((rcnst (access metafunction-context mfc :rcnst)))
    (access rewrite-constant rcnst :current-enabled-structure)))

gather-or-scatter-dangerouslyfunction

(defun gather-or-scatter-dangerously
  (mfc state)
  (declare (xargs :mode :program))
  (let ((ens (get-the-ens-dangerously mfc)) (nume (caar (getprop 'simplify-products-gather-exponents-equal
            'runic-mapping-pairs
            nil
            'current-acl2-world
            (w state)))))
    (enabled-numep nume ens)))

ugly-hack-onefunction

(defun ugly-hack-one
  (lhs rhs mfc state)
  (declare (xargs :mode :program))
  (if (gather-or-scatter-dangerously mfc state)
    (find-rational-matching-factors-gather-exponents lhs
      rhs
      mfc
      state)
    (find-rational-matching-factors-scatter-exponents lhs
      rhs
      mfc
      state)))

ugly-hack-twofunction

(defun ugly-hack-two
  (lhs rhs mfc state)
  (declare (xargs :mode :program))
  (if (gather-or-scatter-dangerously mfc state)
    (find-non-zero-rational-matching-factors-gather-exponents lhs
      rhs
      mfc
      state)
    (find-non-zero-rational-matching-factors-scatter-exponents lhs
      rhs
      mfc
      state)))

floor-cancel-*-not-rewriting-goal-literaltheorem

(defthm floor-cancel-*-not-rewriting-goal-literal
  (implies (and (syntaxp (not (rewriting-goal-literal lhs mfc state)))
      (real/rationalp (/ lhs rhs))
      (syntaxp (in-term-order-* lhs mfc state))
      (syntaxp (in-term-order-* rhs mfc state))
      (bind-free (ugly-hack-two lhs rhs mfc state) (x))
      (real/rationalp x)
      (not (equal x 0)))
    (equal (floor lhs rhs) (floor (* x lhs) (* x rhs)))))

floor-cancel-*-rewriting-goal-literaltheorem

(defthm floor-cancel-*-rewriting-goal-literal
  (implies (and (syntaxp (rewriting-goal-literal lhs mfc state))
      (real/rationalp (/ lhs rhs))
      (syntaxp (in-term-order-* lhs mfc state))
      (syntaxp (in-term-order-* rhs mfc state))
      (bind-free (ugly-hack-one lhs rhs mfc state) (x))
      (real/rationalp x)
      (case-split (not (equal x 0))))
    (equal (floor lhs rhs) (floor (* x lhs) (* x rhs)))))

mod-cancel-*-not-rewriting-goal-literaltheorem

(defthm mod-cancel-*-not-rewriting-goal-literal
  (implies (and (syntaxp (not (rewriting-goal-literal lhs mfc state)))
      (real/rationalp (/ lhs rhs))
      (syntaxp (in-term-order-* lhs mfc state))
      (syntaxp (in-term-order-* rhs mfc state))
      (bind-free (ugly-hack-two lhs rhs mfc state) (x))
      (real/rationalp x)
      (not (equal x 0)))
    (equal (mod lhs rhs) (* (/ x) (mod (* x lhs) (* x rhs)))))
  :hints (("Goal" :in-theory (enable mod))))

mod-cancel-*-rewriting-goal-literaltheorem

(defthm mod-cancel-*-rewriting-goal-literal
  (implies (and (syntaxp (rewriting-goal-literal lhs mfc state))
      (real/rationalp (/ lhs rhs))
      (syntaxp (in-term-order-* lhs mfc state))
      (syntaxp (in-term-order-* rhs mfc state))
      (bind-free (ugly-hack-one lhs rhs mfc state) (x))
      (real/rationalp x)
      (case-split (not (equal x 0))))
    (equal (mod lhs rhs) (* (/ x) (mod (* x lhs) (* x rhs)))))
  :hints (("Goal" :in-theory (enable mod))))

find-constant-factor-floor-modfunction

(defun find-constant-factor-floor-mod
  (lhs rhs)
  (cond ((and (eq (fn-symb lhs) 'binary-*)
       (eq (fn-symb rhs) 'binary-*)
       (numeric-constant-p (arg1 lhs))
       (numeric-constant-p (arg1 rhs))) (let ((c (unquote (arg1 lhs))) (d (unquote (arg1 rhs))))
        (cond ((or (eql c 0) (eql (abs c) 1)) `((c . ,(KWOTE (/ D)))))
          ((or (eql d 0) (eql (abs d) 1)) `((c . ,(KWOTE (/ C)))))
          ((< c d) `((c . ,(KWOTE (/ C)))))
          (t `((c . ,(KWOTE (/ D))))))))
    ((and (eq (fn-symb rhs) 'binary-*)
       (numeric-constant-p lhs)
       (numeric-constant-p (arg1 rhs))) (let ((c (unquote lhs)) (d (unquote (arg1 rhs))))
        (cond ((or (eql c 0) (eql (abs c) 1)) `((c . ,(KWOTE (/ D)))))
          ((or (eql d 0) (eql (abs d) 1)) `((c . ,(KWOTE (/ C)))))
          ((< c d) `((c . ,(KWOTE (/ C)))))
          (t `((c . ,(KWOTE (/ D))))))))
    ((and (eq (fn-symb lhs) 'binary-*)
       (numeric-constant-p (arg1 lhs))
       (numeric-constant-p rhs)) (let ((c (unquote (arg1 lhs))) (d (unquote rhs)))
        (cond ((or (eql c 0) (eql (abs c) 1)) `((c . ,(KWOTE (/ D)))))
          ((or (eql d 0) (eql (abs d) 1)) `((c . ,(KWOTE (/ C)))))
          ((< c d) `((c . ,(KWOTE (/ C)))))
          (t `((c . ,(KWOTE (/ D))))))))
    ((and (eq (fn-symb rhs) 'binary-*)
       (numeric-constant-p (arg1 rhs))
       (not (eq (fn-symb (arg2 rhs)) 'binary-*))
       (eq (fn-symb lhs) 'binary-+)) nil)
    ((and (eq (fn-symb lhs) 'binary-*)
       (numeric-constant-p (arg1 lhs))
       (not (eq (fn-symb (arg2 lhs)) 'binary-*))
       (eq (fn-symb rhs) 'binary-+)) nil)
    ((and (eq (fn-symb rhs) 'binary-+)
       (eq (fn-symb lhs) 'binary-+)) nil)
    (t nil)))

floor-cancel-*-consttheorem

(defthm floor-cancel-*-const
  (implies (and (real/rationalp (/ lhs rhs))
      (syntaxp (in-term-order-* lhs mfc state))
      (syntaxp (in-term-order-* rhs mfc state))
      (bind-free (find-constant-factor-floor-mod lhs rhs) (c))
      (real/rationalp c)
      (not (equal c 0)))
    (equal (floor lhs rhs) (floor (* c lhs) (* c rhs)))))

mod-cancel-*-consttheorem

(defthm mod-cancel-*-const
  (implies (and (real/rationalp (/ lhs rhs))
      (syntaxp (in-term-order-* lhs mfc state))
      (syntaxp (in-term-order-* rhs mfc state))
      (bind-free (find-constant-factor-floor-mod lhs rhs) (c))
      (real/rationalp c)
      (not (equal c 0)))
    (equal (mod lhs rhs) (* (/ c) (mod (* c lhs) (* c rhs)))))
  :hints (("Goal" :in-theory (e/d (mod) (floor-cancel-*-const)))))

find-cancelling-addendsfunction

(defun find-cancelling-addends
  (x y mfc state)
  (declare (xargs :guard (pseudo-termp x)))
  (cond ((eq (fn-symb x) 'binary-+) (cond ((and (proveably-integer '(binary-* x (unary-/ y))
             `((x . ,(NEGATE-MATCH (FARGN X 1))) (y . ,Y))
             mfc
             state)
           (stable-under-rewriting-sums (negate-match (fargn x 1))
             mfc
             state)) (list (cons 'addend (negate-match (fargn x 1)))))
        ((eq (fn-symb (fargn x 2)) 'binary-+) (find-cancelling-addends (fargn x 2) y mfc state))
        ((and (proveably-integer '(binary-* x (unary-/ y))
             `((x . ,(NEGATE-MATCH (FARGN X 2))) (y . ,Y))
             mfc
             state)
           (stable-under-rewriting-sums (negate-match (fargn x 2))
             mfc
             state)) (list (cons 'addend (negate-match (fargn x 2)))))
        (t nil)))
    ((and (proveably-integer '(binary-* x (unary-/ y))
         `((x . ,(NEGATE-MATCH X)) (y . ,Y))
         mfc
         state)
       (stable-under-rewriting-sums (negate-match x) mfc state)) (list (cons 'addend (negate-match x))))
    (t nil)))

cancel-floor-+theorem

(defthm cancel-floor-+
  (implies (and (real/rationalp (/ x y))
      (syntaxp (in-term-order-+ x mfc state))
      (bind-free (find-cancelling-addends x y mfc state) (addend))
      (equal i (/ addend y))
      (integerp i))
    (equal (floor x y) (+ (- i) (floor (+ addend x) y)))))

cancel-mod-+theorem

(defthm cancel-mod-+
  (implies (and (acl2-numberp x)
      (acl2-numberp y)
      (not (equal y 0))
      (syntaxp (not (equal x ''0)))
      (real/rationalp (/ x y))
      (syntaxp (in-term-order-+ x mfc state))
      (bind-free (find-cancelling-addends x y mfc state) (addend))
      (equal i (/ addend y))
      (integerp i))
    (equal (mod x y) (mod (+ addend x) y)))
  :hints (("Goal" :in-theory (enable mod)))
  :otf-flg t)

simplify-mod-+-mod-fnfunction

(defun simplify-mod-+-mod-fn
  (x y mfc state)
  (declare (xargs :guard (pseudo-termp x)))
  (cond ((eq (fn-symb x) 'binary-+) (let ((arg1 (fargn x 1)) (arg2 (fargn x 2)))
        (cond ((and (eq (fn-symb arg1) 'mod)
             (proveably-integer '(binary-* x (unary-/ y))
               `((x . ,(FARGN ARG1 2)) (y . ,Y))
               mfc
               state)
             (stable-under-rewriting-sums (negate-match arg1) mfc state)) (list (cons 'w (fargn arg1 1))
              (cons 'z (fargn arg1 2))
              (cons 'term (negate-match arg1))))
          ((eq (fn-symb arg2) 'binary-+) (simplify-mod-+-mod-fn arg2 y mfc state))
          ((and (eq (fn-symb arg2) 'mod)
             (proveably-integer '(binary-* x (unary-/ y))
               `((x . ,(FARGN ARG2 2)) (y . ,Y))
               mfc
               state)
             (stable-under-rewriting-sums (negate-match arg2) mfc state)) (list (cons 'w (fargn arg2 1))
              (cons 'z (fargn arg2 2))
              (cons 'term (negate-match arg2))))
          (t nil))))
    ((and (eq (fn-symb x) 'mod)
       (proveably-integer '(binary-* x (unary-/ y))
         `((x . ,(FARGN X 2)) (y . ,Y))
         mfc
         state)
       (stable-under-rewriting-sums (negate-match x) mfc state)) (list (cons 'w (fargn x 1))
        (cons 'z (fargn x 2))
        (cons 'term (negate-match x))))
    (t nil)))

|(mod (+ x (mod a b)) y)|encapsulate

(encapsulate nil
  (local (in-theory (disable (:type-prescription mod-nonnegative)
        (:type-prescription rationalp-mod)
        (:rewrite normalize-terms-such-as-1/ax+bx)
        (:rewrite mod-x-y-=-x . 4)
        (:rewrite prefer-positive-addends-<)
        (:rewrite reduce-rationalp-*)
        (:rewrite normalize-terms-such-as-a/a+b-+-b/a+b)
        (:rewrite rationalp-minus-x)
        (:rewrite |(< c (- x))|)
        (:rewrite |(< (- x) c)|)
        (:rewrite |(< (- x) (- y))|)
        (:rewrite |(rationalp (- x))|)
        (:rewrite mod-x-y-=-x . 2)
        (:rewrite reduce-rational-multiplicative-constant-<)
        (:rewrite reduce-multiplicative-constant-<)
        (:rewrite integerp-<-constant)
        (:rewrite constant-<-integerp)
        (:rewrite |(< c (/ x)) positive c --- present in goal|)
        (:rewrite |(< c (/ x)) positive c --- obj t or nil|)
        (:rewrite |(< c (/ x)) negative c --- present in goal|)
        (:rewrite |(< c (/ x)) negative c --- obj t or nil|)
        (:rewrite |(< (/ x) c) positive c --- present in goal|)
        (:rewrite |(< (/ x) c) positive c --- obj t or nil|)
        (:rewrite |(< (/ x) c) negative c --- present in goal|)
        (:rewrite |(< (/ x) c) negative c --- obj t or nil|)
        (:rewrite |(< (/ x) (/ y))|)
        (:linear mod-bounds-3)
        (:rewrite rationalp-/)
        (:rewrite mod-cancel-*-rewriting-goal-literal)
        (:rewrite mod-cancel-*-const)
        (:rewrite |(mod x (* y (/ z))) rewriting-goal-literal|)
        (:rewrite |(mod (* x (/ y)) z) rewriting-goal-literal|)
        (:meta meta-integerp-correct)
        (:rewrite simplify-products-gather-exponents-equal)
        (:rewrite |(- (* c x))|)
        (:rewrite integerp-minus-x)
        (:rewrite |(< (* x y) 0)|)
        (:rewrite |(< (/ x) 0)|)
        (:rewrite simplify-terms-such-as-ax+bx-<-0-rational-remainder)
        (:rewrite simplify-terms-such-as-ax+bx-<-0-rational-common)
        (:rewrite |(equal (- x) (- y))|)
        (:rewrite reduce-multiplicative-constant-equal)
        (:rewrite equal-of-predicates-rewrite)
        (:rewrite |(equal c (/ x))|)
        (:rewrite |(equal c (- x))|)
        (:rewrite |(equal (/ x) c)|)
        (:rewrite |(equal (/ x) (/ y))|)
        (:rewrite |(equal (- x) c)|)
        (:rewrite |(<= 1 (* x (/ y))) with (< y 0)|)
        (:rewrite |(<= 1 (* x (/ y))) with (< 0 y)|)
        (:rewrite |(< (* x (/ y)) 1) with (< y 0)|)
        (:rewrite |(< (* x (/ y)) 1) with (< 0 y)|)
        (:rewrite |(equal (mod (+ x y) z) x)|)
        (:rewrite |(< 0 (/ x))|)
        (:rewrite |(< 0 (* x y))|)
        (:rewrite simplify-terms-such-as-0-<-ax+bx-rational-remainder)
        (:rewrite simplify-terms-such-as-0-<-ax+bx-rational-common)
        (:rewrite |(< (+ c/d x) y)|)
        (:rewrite |(< (+ (- c) x) y)|)
        (:rewrite |(mod (- x) y)| . 1))))
  (defthm |(mod (+ x (mod a b)) y)|
    (implies (and (acl2-numberp x)
        (acl2-numberp y)
        (real/rationalp (/ x y))
        (not (equal y 0))
        (syntaxp (in-term-order-+ x mfc state))
        (bind-free (simplify-mod-+-mod-fn x y mfc state) (w z term))
        (syntaxp (stable-under-rewriting-sums term mfc state))
        (equal term (- (mod w z)))
        (integerp (/ z y)))
      (equal (mod x y) (mod (+ term w x) y)))))

simplify-mod-+-minus-mod-fnfunction

(defun simplify-mod-+-minus-mod-fn
  (x y mfc state)
  (declare (xargs :guard (pseudo-termp x)))
  (cond ((eq (fn-symb x) 'binary-+) (let ((arg1 (fargn x 1)) (arg2 (fargn x 2)))
        (cond ((and (eq (fn-symb arg1) 'unary--)
             (eq (fn-symb (fargn arg1 1)) 'mod)
             (proveably-integer '(binary-* x (unary-/ y))
               `((x . ,(FARGN (FARGN ARG1 1) 2)) (y . ,Y))
               mfc
               state)
             (stable-under-rewriting-sums (negate-match (fargn arg1 1))
               mfc
               state)) (list (cons 'w (fargn (fargn arg1 1) 1))
              (cons 'z (fargn (fargn arg1 1) 2))
              (cons 'term (negate-match arg1))))
          ((eq (fn-symb arg2) 'binary-+) (simplify-mod-+-minus-mod-fn arg2 y mfc state))
          ((and (eq (fn-symb arg2) 'unary--)
             (eq (fn-symb (fargn arg2 1)) 'mod)
             (proveably-integer '(binary-* x (unary-/ y))
               `((x . ,(FARGN (FARGN ARG2 1) 2)) (y . ,Y))
               mfc
               state)
             (stable-under-rewriting-sums (negate-match (fargn arg2 1))
               mfc
               state)) (list (cons 'w (fargn (fargn arg2 1) 1))
              (cons 'z (fargn (fargn arg2 1) 2))
              (cons 'term (negate-match arg2))))
          (t nil))))
    ((and (eq (fn-symb x) 'unary--)
       (eq (fn-symb (fargn x 1)) 'mod)
       (proveably-integer '(binary-* x (unary-/ y))
         `((x . ,(FARGN (FARGN X 1) 2)) (y . ,Y))
         mfc
         state)
       (stable-under-rewriting-sums (negate-match (fargn x 1))
         mfc
         state)) (list (cons 'w (fargn (fargn x 1) 1))
        (cons 'z (fargn (fargn x 1) 2))
        (cons 'term (negate-match (fargn x 1)))))
    (t nil)))

|(mod (+ x (- (mod a b))) y)|theorem

(defthm |(mod (+ x (- (mod a b))) y)|
  (implies (and (acl2-numberp x)
      (acl2-numberp y)
      (real/rationalp (/ x y))
      (not (equal y 0))
      (syntaxp (in-term-order-+ x mfc state))
      (bind-free (simplify-mod-+-minus-mod-fn x y mfc state)
        (w z term))
      (syntaxp (stable-under-rewriting-sums term mfc state))
      (equal term (mod w z))
      (integerp (/ z y)))
    (equal (mod x y) (mod (+ x (- w) term) y))))