basic

other

(in-package "ACL2")

include-book

(include-book "building-blocks")

local

(local (include-book "../../support/top"))

|(+ c (+ d x))|theorem

(defthm |(+ c (+ d x))|
  (implies (and (syntaxp (quotep c)) (syntaxp (quotep d)))
    (equal (+ c (+ d x)) (+ (+ c d) x))))

|(+ y x)|theorem

(defthm |(+ y x)| (equal (+ y x) (+ x y)))

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

(defthm |(+ y (+ x z))| (equal (+ y (+ x z)) (+ x (+ y z))))

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

(defthm |(+ (+ x y) z)| (equal (+ (+ x y) z) (+ x (+ y z))))

|(+ 0 x)|theorem

(defthm |(+ 0 x)|
  (implies (acl2-numberp x) (equal (+ 0 x) x)))

|(- (- x))|theorem

(defthm |(- (- x))|
  (implies (acl2-numberp x) (equal (- (- x)) x)))

|(- (+ x y))|theorem

(defthm |(- (+ x y))| (equal (- (+ x y)) (+ (- x) (- y))))

|(* c (* d x))|theorem

(defthm |(* c (* d x))|
  (implies (and (syntaxp (quotep c)) (syntaxp (quotep d)))
    (equal (* c (* d x)) (* (* c d) x))))

|(* y x)|theorem

(defthm |(* y x)| (equal (* y x) (* x y)))

|(* y (* x z))|theorem

(defthm |(* y (* x z))| (equal (* y (* x z)) (* x (* y z))))

|(* (* x y) z)|theorem

(defthm |(* (* x y) z)| (equal (* (* x y) z) (* x (* y z))))

|(* 1 x)|theorem

(defthm |(* 1 x)|
  (implies (acl2-numberp x) (equal (* 1 x) x)))

|(* 0 x)|theorem

(defthm |(* 0 x)| (equal (* 0 x) 0))

|(* -1 x)|theorem

(defthm |(* -1 x)| (equal (* -1 x) (- x)))

|(/ (/ x))|theorem

(defthm |(/ (/ x))|
  (implies (acl2-numberp x) (equal (/ (/ x)) x)))

|(/ (* x y))|theorem

(defthm |(/ (* x y))| (equal (/ (* x y)) (* (/ x) (/ y))))

|(* a (/ a))|theorem

(defthm |(* a (/ a))|
  (implies (acl2-numberp x)
    (equal (* x (/ x))
      (if (equal x 0)
        0
        1))))

|(* a (/ a) b)|theorem

(defthm |(* a (/ a) b)|
  (implies (and (acl2-numberp x) (acl2-numberp y))
    (equal (* x (/ x) y)
      (if (equal x 0)
        0
        y))))

|(* x (- y))|theorem

(defthm |(* x (- y))|
  (implies (syntaxp (not (quotep y)))
    (equal (* x (- y)) (- (* x y)))))

|(* (- x) y)|theorem

(defthm |(* (- x) y)|
  (implies (syntaxp (not (quotep x)))
    (equal (* (- x) y) (- (* x y)))))

|(- (* c x))|theorem

(defthm |(- (* c x))|
  (implies (syntaxp (quotep c))
    (equal (- (* c x)) (* (- c) x))))

|(/ (- x))|theorem

(defthm |(/ (- x))|
  (implies (syntaxp (not (quotep x)))
    (equal (/ (- x)) (- (/ x)))))

Included Books