Filtering...

top

books/arithmetic-5/lib/basic-ops/top

Included Books

we-are-here distributivity default-hint building-blocks common normalize simplify mini-theories numerator-and-denominator natp-posp integerp-meta integerp basic expt collect remove-weak-inequalities arithmetic-theory types simple-equalities-and-inequalities if-normalization forcing-types banner
other
(in-package "ACL2")
other
(deftheory base (current-theory :here))
include-book
(include-book "we-are-here")
include-book
(include-book "distributivity")
include-book
(include-book "default-hint")
include-book
(include-book "building-blocks")
include-book
(include-book "common")
include-book
(include-book "normalize")
include-book
(include-book "simplify")
other
(deftheory minimal-start-a (current-theory :here))
other
(deftheory-static arithmetic-5-minimal-start-a
  (current-theory :here))
include-book
(include-book "mini-theories")
include-book
(include-book "numerator-and-denominator")
other
(deftheory natp-posp-start (current-theory :here))
include-book
(include-book "natp-posp")
other
(deftheory natp-posp-end (current-theory :here))
include-book
(include-book "integerp-meta")
include-book
(include-book "integerp")
include-book
(include-book "basic")
include-book
(include-book "expt")
other
(deftheory minimal-end-a (current-theory :here))
other
(deftheory-static arithmetic-5-minimal-end-a
  (current-theory :here))
include-book
(include-book "collect")
include-book
(include-book "remove-weak-inequalities")
include-book
(include-book "arithmetic-theory")
include-book
(include-book "types")
other
(deftheory minimal-start-b (current-theory :here))
other
(deftheory-static arithmetic-5-minimal-start-b
  (current-theory :here))
include-book
(include-book "simple-equalities-and-inequalities")
include-book
(include-book "if-normalization")
include-book
(include-book "forcing-types")
other
(deftheory minimal-end-b (current-theory :here))
other
(deftheory-static arithmetic-5-minimal-end-b
  (current-theory :here))
other
(deftheory full (current-theory :here))
other
(deftheory minimal-arithmetic-theory
  (union-theories (theory 'base)
    (union-theories (set-difference-theories (theory 'minimal-end-a)
        (theory 'minimal-start-a))
      (set-difference-theories (theory 'minimal-end-b)
        (theory 'minimal-start-b)))))
other
(deftheory natp-posp-theory
  (set-difference-theories (theory 'natp-posp-end)
    (theory 'natp-posp-start)))
enable-natp-pposp-theorymacro
(defmacro enable-natp-pposp-theory
  nil
  '(progn (in-theory (enable natp-posp-theory))
    (in-theory (disable natp posp))))
disable-natp-posp-theorymacro
(defmacro disable-natp-posp-theory
  nil
  '(progn (in-theory (disable natp-posp-theory))
    (in-theory (enable natp posp))))
other
(disable-natp-posp-theory)
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 (+ m n)|
    |(expt x (+ m n)) non-zero x|
    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-<
    |(equal (+ (- c) x) y)|
    |(< (+ (- c) x) y)|
    |(< y (+ (- c) x))|))
other
(deftheory prefer-positive-exponents-scatter-exponents-theory
  '(prefer-positive-exponents-scatter-exponents-equal prefer-positive-exponents-scatter-exponents-<
    prefer-positive-exponents-scatter-exponents-<-2))
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 (if (active-runep '(:definition arith-5-active-flag))
    (not (and (active-runep '(:rewrite |(expt x (+ m n))|))
        (active-runep '(:rewrite normalize-factors-gather-exponents))))
    t)
  :error nil)
in-theory
(in-theory (disable expt))
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 (* 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 (* (/ 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 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-scatter-exponents
    arith-normalize-factors-scatter-exponents
    arith-normalize-addends
    arith-find-matching-addend))
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 (* 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 (* (/ 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 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-+-problem-finder
    arith-collect-*-problem-finder
    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-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-*
    inverse-of-*
    rationalp-*
    rationalp-unary-/
    distributivity
    nonnegative-product
    rationalp-implies-acl2-numberp
    expt-type-prescription-non-zero-base
    default-+-1
    default-+-2
    default-*-1
    default-*-2
    default-unary-minus
    default-unary-/
    default-<-1
    default-<-2
    default-denominator
    default-numerator))
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)