Filtering...

post

books/arithmetic-2/meta/post

Included Books

top
other
(in-package "ACL2")
local
(local (include-book "../pass1/top"))
|(+ (+ x y) z)|theorem
(defthm |(+ (+ x y) z)| (equal (+ (+ x y) z) (+ x (+ y z))))
|(+ 0 x)|theorem
(defthm |(+ 0 x)| (equal (+ 0 x) (fix x)))
|(+ x 0)|theorem
(defthm |(+ x 0)| (equal (+ x 0) (fix x)))
|(+ c (+ d x))|theorem
(defthm |(+ c (+ d x))|
  (implies (and (syntaxp (quotep c)) (syntaxp (quotep d)))
    (equal (+ c (+ d x)) (+ (+ c d) x))))
|(- (- x))|theorem
(defthm |(- (- x))| (equal (- (- x)) (fix x)))
|(- (+ x y))|theorem
(defthm |(- (+ x y))| (equal (- (+ x y)) (+ (- x) (- y))))
|(* (* x y) z)|theorem
(defthm |(* (* x y) z)| (equal (* (* x y) z) (* x (* y z))))
|(* 1 x)|theorem
(defthm |(* 1 x)| (equal (* 1 x) (fix x)))
|(* x 1)|theorem
(defthm |(* x 1)| (equal (* x 1) (fix x)))
|(* 0 x)|theorem
(defthm |(* 0 x)| (equal (* 0 x) 0))
|(* x 0)|theorem
(defthm |(* x 0)| (equal (* x 0) 0))
|(* -1 x)|theorem
(defthm |(* -1 x)| (equal (* -1 x) (- x)))
|(* x -1)|theorem
(defthm |(* x -1)| (equal (* x -1) (- x)))
|(* c (* d x))|theorem
(defthm |(* c (* d x))|
  (implies (and (syntaxp (quotep c)) (syntaxp (quotep d)))
    (equal (* c (* d x)) (* (* c d) x))))
|(/ (/ x))|theorem
(defthm |(/ (/ x))| (equal (/ (/ x)) (fix x)))
|(/ (* x y))|theorem
(defthm |(/ (* x y))| (equal (/ (* x y)) (* (/ x) (/ y))))
|(* x (+ y z))|theorem
(defthm |(* x (+ y z))|
  (equal (* x (+ y z)) (+ (* x y) (* x z))))
local
(local (in-theory (disable distributivity)))
|(* (+ x y) z)|theorem
(defthm |(* (+ x y) z)|
  (equal (* (+ x y) z) (+ (* x z) (* y z))))
|(* x (- y))|theorem
(defthm |(* x (- y))|
  (implies (syntaxp (not (and (consp y) (fquotep y) (acl2-numberp (cadr y)))))
    (equal (* x (- y)) (- (* x y)))))
|(* (- x) y)|theorem
(defthm |(* (- x) y)|
  (implies (syntaxp (not (and (consp x) (fquotep x) (acl2-numberp (cadr x)))))
    (equal (* (- x) y) (- (* x y)))))
|(- (* c x))|theorem
(defthm |(- (* c x))|
  (implies (syntaxp (and (consp c) (fquotep c) (acl2-numberp (cadr c))))
    (equal (- (* c x)) (* (- c) x))))
|(/ (- x))|theorem
(defthm |(/ (- x))|
  (implies (syntaxp (not (and (consp x) (fquotep x) (acl2-numberp (cadr x)))))
    (equal (/ (- x)) (- (/ x)))))
|(equal (/ x) 0)|theorem
(defthm |(equal (/ x) 0)|
  (equal (equal (/ x) 0) (equal (fix x) 0)))
|(equal (- x) 0)|theorem
(defthm |(equal (- x) 0)|
  (equal (equal (- x) 0) (equal (fix x) 0)))
|(equal (/ x) (/ y))|theorem
(defthm |(equal (/ x) (/ y))|
  (equal (equal (/ x) (/ y)) (equal (fix x) (fix y))))
|(equal (- x) (- y))|theorem
(defthm |(equal (- x) (- y))|
  (equal (equal (- x) (- y)) (equal (fix x) (fix y))))
|(< (/ x) 0)|theorem
(defthm |(< (/ x) 0)|
  (implies (real/rationalp x)
    (equal (< (/ x) 0) (< (fix x) 0))))
|(< 0 (/ x))|theorem
(defthm |(< 0 (/ x))|
  (implies (real/rationalp x)
    (equal (< 0 (/ x)) (< 0 (fix x)))))
|(< (- x) 0)|theorem
(defthm |(< (- x) 0)| (equal (< (- x) 0) (< 0 (fix x))))
|(< 0 (- x))|theorem
(defthm |(< 0 (- x))| (equal (< 0 (- x)) (< (fix x) 0)))
|(< (- x) (- y))|theorem
(defthm |(< (- x) (- y))|
  (equal (< (- x) (- y)) (< (fix y) (fix x))))
|(+ (if x y z) w)|theorem
(defthm |(+ (if x y z) w)|
  (equal (+ (if x
        y
        z)
      w)
    (if x
      (+ y w)
      (+ z w))))
|(+ w (if x y z))|theorem
(defthm |(+ w (if x y z))|
  (equal (+ w
      (if x
        y
        z))
    (if x
      (+ w y)
      (+ w z))))
|(- (if x y z))|theorem
(defthm |(- (if x y z))|
  (equal (- (if x
        y
        z))
    (if x
      (- y)
      (- z))))
|(* (if x y z) w)|theorem
(defthm |(* (if x y z) w)|
  (equal (* (if x
        y
        z)
      w)
    (if x
      (* y w)
      (* z w))))
|(* w (if x y z))|theorem
(defthm |(* w (if x y z))|
  (equal (* w
      (if x
        y
        z))
    (if x
      (* w y)
      (* w z))))
|(/ (if x y z))|theorem
(defthm |(/ (if x y z))|
  (equal (/ (if x
        y
        z))
    (if x
      (/ y)
      (/ z))))
|(expt (if x y z) w)|theorem
(defthm |(expt (if x y z) w)|
  (equal (expt (if x
        y
        z)
      w)
    (if x
      (expt y w)
      (expt z w))))
|(expt w (if x y z))|theorem
(defthm |(expt w (if x y z))|
  (equal (expt w
      (if x
        y
        z))
    (if x
      (expt w y)
      (expt w z))))
|(equal w (if x y z))|theorem
(defthm |(equal w (if x y z))|
  (equal (equal w
      (if x
        y
        z))
    (if x
      (equal w y)
      (equal w z))))
|(equal (if x y z) w)|theorem
(defthm |(equal (if x y z) w)|
  (equal (equal (if x
        y
        z)
      w)
    (if x
      (equal y w)
      (equal z w))))
|(< w (if x y z))|theorem
(defthm |(< w (if x y z))|
  (equal (< w
      (if x
        y
        z))
    (if x
      (< w y)
      (< w z))))
|(< (if x y z) w)|theorem
(defthm |(< (if x y z) w)|
  (equal (< (if x
        y
        z)
      w)
    (if x
      (< y w)
      (< z w))))