other
(in-package "ACL2")
other
(deftheory-static arithmetic-5-current-base (current-theory :here))
other
(deftheory-static arithmetic-5-universal-base (universal-theory :here))
include-book
(include-book "lib/basic-ops/top")
include-book
(include-book "lib/floor-mod/top")
other
(deftheory-static arithmetic-5-current-full (current-theory :here))
other
(deftheory-static arithmetic-5-universal-full (universal-theory :here))
other
(deftheory minimal-arithmetic-5-base (theory 'arithmetic-5-current-base))
other
(deftheory default-arithmetic-5-base (intersection-theories (theory 'arithmetic-5-universal-base) (theory 'arithmetic-5-current-full)))
other
(deftheory-static minimal-arithmetic-5 (union-theories (set-difference-theories (theory 'arithmetic-5-minimal-end-a) (theory 'arithmetic-5-minimal-start-a)) (set-difference-theories (theory 'arithmetic-5-minimal-end-b) (theory 'arithmetic-5-minimal-start-b))))
other
(deftheory default-arithmetic-5 (set-difference-theories (theory 'arithmetic-5-current-full) (theory 'arithmetic-5-current-base)))
intersection-theories-3macro
(defmacro intersection-theories-3 (x y z) `(intersection-theories ,X (intersection-theories ,Y ,Z)))
union-theories-3macro
(defmacro union-theories-3 (x y z) `(union-theories ,X (union-theories ,Y ,Z)))
set-minimal-arithmetic-5-theorymacro
(defmacro set-minimal-arithmetic-5-theory nil `(in-theory (union-theories-3 (intersection-theories-3 (theory 'minimal-arithmetic-5-base) (theory 'arithmetic-5-current-full) (current-theory :here)) (theory 'minimal-arithmetic-5) (set-difference-theories (current-theory :here) (theory 'arithmetic-5-universal-full)))))
set-default-arithmetic-5-theorymacro
(defmacro set-default-arithmetic-5-theory nil `(in-theory (union-theories-3 (intersection-theories-3 (theory 'default-arithmetic-5-base) (theory 'arithmetic-5-current-full) (current-theory :here)) (theory 'default-arithmetic-5) (set-difference-theories (current-theory :here) (theory 'arithmetic-5-universal-full)))))