Filtering...

top

books/arithmetic-3/bind-free/top

Included Books

default-hint building-blocks mini-theories common normalize simplify numerator-and-denominator integerp integerp-meta basic collect remove-weak-inequalities arithmetic-theory banner
other
(in-package "ACL2")
other
(deftheory arithmetic-3-bind-free-base
  (current-theory :here))
include-book
(include-book "default-hint")
include-book
(include-book "building-blocks")
include-book
(include-book "mini-theories")
include-book
(include-book "common")
include-book
(include-book "normalize")
include-book
(include-book "simplify")
include-book
(include-book "numerator-and-denominator")
include-book
(include-book "integerp")
include-book
(include-book "integerp-meta")
other
(deftheory pre-basic (current-theory :here))
include-book
(include-book "basic")
other
(deftheory post-basic (current-theory :here))
include-book
(include-book "collect")
include-book
(include-book "remove-weak-inequalities")
include-book
(include-book "arithmetic-theory")
other
(deftheory full (current-theory :here))
other
(deftheory minimal-arithmetic-theory
  (union-theories (theory 'arithmetic-3-bind-free-base)
    (set-difference-theories (theory 'post-basic)
      (theory 'pre-basic))))
other
(deftheory gather-exponents-theory
  '(normalize-factors-gather-exponents simplify-products-gather-exponents-equal
    simplify-products-gather-exponents-<))
other
(deftheory scatter-exponents-theory
  '(|(expt x (+ m n))| |(expt x (+ m n)) non-zero x|
    |(expt x c)|
    normalize-factors-scatter-exponents
    simplify-products-scatter-exponents-equal
    simplify-products-scatter-exponents-<))
other
(deftheory prefer-positive-addends-theory
  '(prefer-positive-addends-equal prefer-positive-addends-<))
other
(deftheory prefer-positive-exponents-scatter-exponents-theory
  '(prefer-positive-exponents-scatter-exponents-equal prefer-positive-exponents-scatter-exponents-<))
gather-exponentsmacro
(defmacro gather-exponents
  nil
  '(progn (in-theory (disable scatter-exponents-theory))
    (in-theory (disable prefer-positive-exponents-scatter-exponents-theory))
    (in-theory (enable gather-exponents-theory))))
scatter-exponentsmacro
(defmacro scatter-exponents
  nil
  '(progn (in-theory (disable gather-exponents-theory))
    (in-theory (enable scatter-exponents-theory))))
prefer-positive-exponentsmacro
(defmacro prefer-positive-exponents
  nil
  '(progn (in-theory (disable gather-exponents-theory))
    (in-theory (enable prefer-positive-exponents-scatter-exponents-theory))
    (in-theory (enable scatter-exponents-theory))))
do-not-prefer-positive-exponentsmacro
(defmacro do-not-prefer-positive-exponents
  nil
  '(in-theory (disable prefer-positive-exponents-scatter-exponents-theory)))
prefer-positive-addendsmacro
(defmacro prefer-positive-addends
  nil
  '(in-theory (enable prefer-positive-addends-theory)))
do-not-prefer-positive-addendsmacro
(defmacro do-not-prefer-positive-addends
  nil
  '(in-theory (disable prefer-positive-addends-theory)))
other
(gather-exponents)
other
(prefer-positive-addends)
other
(theory-invariant (not (and (active-runep '(:rewrite |(expt x (+ m n))|))
      (active-runep '(:rewrite normalize-factors-gather-exponents))))
  :error nil)
in-theory
(in-theory (disable expt))
other
(deftheory strong-expt-type-prescription-rules
  '(expt-type-prescription-negative-base-even-exponent expt-type-prescription-negative-base-odd-exponent
    expt-type-prescription-nonpositive-base-even-exponent
    expt-type-prescription-nonpositive-base-odd-exponent
    expt-negative-base-even-exponent
    expt-negative-base-odd-exponent))
in-theory
(in-theory (disable strong-expt-type-prescription-rules))
in-theory
(in-theory (disable |arith (expt x c)|
    |arith (- (- x))|
    |arith (- (+ x y))|
    |arith (* y x)|
    |arith (* y (* x z))|
    |arith (* (* x y) z)|
    |arith (* 1 x)|
    |arith (* x 1)|
    |arith (* 0 x)|
    |arith (* x 0)|
    |arith (* -1 x)|
    |arith (/ (/ x))|
    |arith (/ (* x y))|
    |arith (* x (+ y z))|
    |arith (* (+ x y) z)|
    |arith (* x (- y))|
    |arith (* (- x) y)|
    |arith (- (* c x))|
    |arith (/ (- x))|
    |arith (expt (+ x y) 2)|
    |arith (expt (+ x y) 3)|
    |arith (expt x 0)|
    |arith (expt 0 n)|
    |arith (expt x 1)|
    |arith (expt 1 n)|
    |arith (expt x -1)|
    |arith (expt (/ x) n)|
    |arith (expt x (- n))|
    |arith (expt 1/c n)|
    |arith (expt 4 n)|
    |arith (expt 8 n)|
    |arith (expt 16 n)|
    |arith (expt (* x y) n)|
    |arith (expt (expt x m) n)|
    |arith (expt x (+ m n))|
    |arith (expt x (+ m n)) non-zero x|
    |arith (fix x)|
    |arith (* (expt x n) (expt y n))|
    |arith (* x x)|
    |arith (* x (/ x))|
    |arith (* x (expt x n))|
    |arith (* x (expt (- x) n))|
    |arith (* x (/ (expt x n)))|
    |arith (* (numerator x) (/ (denominator x)))|
    |arith (* c (* d x))|
    |arith (* x (/ (expt (- x) n)))|
    |arith (* (/ x) (expt x n))|
    |arith (* (/ x) (expt (- x) n))|
    |arith (* (expt x m) (expt x n))|
    |arith (* (expt (- x) m) (expt x n))|
    |arith (* (expt x m) (expt (- x) n))|
    |arith (* (/ (expt x m)) (expt x n))|
    |arith (* (/ (expt (- x) m)) (expt x n))|
    |arith (* (/ (expt x m)) (expt (- x) n))|
    |arith (* (expt x m) (/ (expt x n)))|
    |arith (* (expt (- x) m) (/ (expt x n)))|
    |arith (* (expt x m) (/ (expt (- x) n)))|
    |arith (* (expt c n) (expt d n))|
    |arith (+ c (+ d x))|
    |arith (+ x x)|
    |arith (+ x (- x))|
    |arith (+ x (* c x))|
    |arith (+ (- x) (* c x))|
    |arith (+ (* c x) (* d x))|
    arith-collect-+
    arith-collect-+-problem-finder
    arith-collect-*
    arith-collect-*-problem-finder
    arith-bubble-down
    arith-bubble-down-+-problem-finder
    arith-bubble-down-+-bubble-down
    arith-bubble-down-+-match-1
    arith-bubble-down-+-match-2
    arith-bubble-down-+-match-3
    arith-bubble-down-*-problem-finder
    arith-bubble-down-*-bubble-down
    arith-bubble-down-*-match-1
    arith-bubble-down-*-match-2
    arith-bubble-down-*-match-3
    |(arith-collect-* y x)|
    |(arith-collect-+ y x)|
    arith-find-matching-factor-gather-exponents
    arith-normalize-factors-gather-exponents
    arith-find-matching-factor-scatter-exponents
    arith-normalize-factors-scatter-exponents
    arith-find-matching-addend
    arith-normalize-addends))
other
(in-arithmetic-theory '(|arith (expt x c)| |arith (- (- x))|
    |arith (- (+ x y))|
    |arith (* y x)|
    |arith (* y (* x z))|
    |arith (* (* x y) z)|
    |arith (* 1 x)|
    |arith (* x 1)|
    |arith (* 0 x)|
    |arith (* x 0)|
    |arith (* -1 x)|
    |arith (/ (/ x))|
    |arith (/ (* x y))|
    |arith (* x (+ y z))|
    |arith (* (+ x y) z)|
    |arith (* x (- y))|
    |arith (* (- x) y)|
    |arith (- (* c x))|
    |arith (/ (- x))|
    |arith (expt (+ x y) 2)|
    |arith (expt (+ x y) 3)|
    |arith (expt x 0)|
    |arith (expt 0 n)|
    |arith (expt x 1)|
    |arith (expt 1 n)|
    |arith (expt x -1)|
    |arith (expt (/ x) n)|
    |arith (expt x (- n))|
    |arith (expt 1/c n)|
    |arith (expt 4 n)|
    |arith (expt 8 n)|
    |arith (expt 16 n)|
    |arith (expt (* x y) n)|
    |arith (expt (expt x m) n)|
    |arith (expt x (+ m n))|
    |arith (expt x (+ m n)) non-zero x|
    |arith (fix x)|
    |arith (* (expt x n) (expt y n))|
    |arith (* x x)|
    |arith (* x (/ x))|
    |arith (* x (expt x n))|
    |arith (* x (expt (- x) n))|
    |arith (* x (/ (expt x n)))|
    |arith (* (numerator x) (/ (denominator x)))|
    |arith (* c (* d x))|
    |arith (* x (/ (expt (- x) n)))|
    |arith (* (/ x) (expt x n))|
    |arith (* (/ x) (expt (- x) n))|
    |arith (* (expt x m) (expt x n))|
    |arith (* (expt (- x) m) (expt x n))|
    |arith (* (expt x m) (expt (- x) n))|
    |arith (* (/ (expt x m)) (expt x n))|
    |arith (* (/ (expt (- x) m)) (expt x n))|
    |arith (* (/ (expt x m)) (expt (- x) n))|
    |arith (* (expt x m) (/ (expt x n)))|
    |arith (* (expt (- x) m) (/ (expt x n)))|
    |arith (* (expt x m) (/ (expt (- x) n)))|
    |arith (* (expt c n) (expt d n))|
    |arith (+ c (+ d x))|
    |arith (+ x x)|
    |arith (+ x (- x))|
    |arith (+ x (* c x))|
    |arith (+ (- x) (* c x))|
    |arith (+ (* c x) (* d x))|
    arith-bubble-down-*-bubble-down
    arith-bubble-down-*-match-1
    arith-bubble-down-*-match-2
    arith-bubble-down-*-match-3
    arith-bubble-down-+-bubble-down
    arith-bubble-down-+-match-1
    arith-bubble-down-+-match-2
    arith-bubble-down-+-match-3
    |(arith-collect-* y x)|
    |(arith-collect-+ y x)|
    arith-normalize-factors-scatter-exponents
    arith-normalize-addends))
in-theory
(in-theory (disable associativity-of-+
    commutativity-of-+
    unicity-of-0
    inverse-of-+
    rationalp-+
    rationalp-unary--
    unicity-of-1
    associativity-of-*
    commutativity-of-*
    rational-implies2
    inverse-of-*
    rationalp-*
    rationalp-unary-/
    distributivity
    nonnegative-product
    rationalp-implies-acl2-numberp
    expt-type-prescription-non-zero-base))
other
(deftheory default-arithmetic-theory (current-theory :here))
set-default-arithmetic-theorymacro
(defmacro set-default-arithmetic-theory
  nil
  `(in-theory (union-theories (set-difference-theories (current-theory :here)
        (theory 'full))
      (theory 'default-arithmetic-theory))))
set-minimal-arithmetic-theorymacro
(defmacro set-minimal-arithmetic-theory
  nil
  `(in-theory (union-theories (set-difference-theories (current-theory :here)
        (theory 'full))
      (theory 'minimal-arithmetic-theory))))
include-book
(include-book "banner" :load-compiled-file nil)