Included Books
other
(in-package "ACL2")
include-book
(include-book "pre")
include-book
(include-book "integerp")
include-book
(include-book "integerp-meta")
include-book
(include-book "cancel-terms-meta")
include-book
(include-book "collect-terms-meta")
include-book
(include-book "numerator-and-denominator")
include-book
(include-book "expt")
include-book
(include-book "non-linear")
include-book
(include-book "mini-theories")
include-book
(include-book "post")
other
(deftheory scatter-exponents '(collect-factors-scatter-exponents-thm cancel-factors-scatter-exponents-equal-thm cancel-factors-scatter-exponents-<-thm |(expt x (+ i j))| |(expt x (+ i j)) with non-negative exponents| |(expt x (+ i j)) with non-positive exponents| |(expt x (+ i j)) with non-zero base|))
other
(deftheory gather-exponents '(collect-factors-gather-exponents-thm cancel-factors-gather-exponents-equal-thm cancel-factors-gather-exponents-<-thm))
in-theory
(in-theory (disable scatter-exponents))
in-theory
(in-theory (enable gather-exponents))
other
(deftheory prefer-positive-exponents-scatter-exponents '(prefer-positive-factors-scatter-exponents-equal-thm prefer-positive-factors-scatter-exponents-<-thm))
in-theory
(in-theory (disable prefer-positive-exponents-scatter-exponents))
other
(deftheory prefer-positive-exponents-gather-exponents '(prefer-positive-factors-gather-exponents-equal-thm prefer-positive-factors-gather-exponents-<-thm))
in-theory
(in-theory (disable prefer-positive-exponents-gather-exponents))
other
(deftheory prefer-positive-sums '(prefer-positive-addends-equal-thm prefer-positive-addends-<-thm))
in-theory
(in-theory (disable strong-expt-rules))
in-theory
(in-theory (disable rewrite-linear-inequalities-to-iff))
in-theory
(in-theory (disable ratio-theory-of-1))
in-theory
(in-theory (disable expt))
in-theory
(in-theory (enable un-hide-times collect-times-0a collect-times-0b collect-times-1a collect-times-1b collect-times-1c collect-times-1d collect-times-2a collect-times-2b collect-times-2c collect-times-2d collect-times-2e collect-times-2f collect-times-3a collect-times-3b collect-times-3c collect-times-3d collect-times-4))
in-theory
(in-theory (enable un-hide-plus collect-plus-0a collect-plus-1a collect-plus-1b collect-plus-1c collect-plus-1d collect-plus-2a collect-plus-2b collect-plus-2c collect-plus-2d collect-plus-3))
in-theory
(in-theory (disable collect-+ collect-* un-hide-+ un-hide-*))
in-theory
(in-theory (disable default-+-1 default-+-2 default-unary-minus default-*-1 default-*-2 default-unary-/ commutativity-of-+ commutativity-of-* associativity-of-+ unicity-of-0 associativity-of-* unicity-of-1 distributivity inverse-of-+ rationalp-+ rationalp-unary-- inverse-of-* rationalp-* rationalp-unary-/ nonnegative-product rationalp-implies-acl2-numberp rational-implies2 expt-type-prescription-non-zero-base))