arith - ACL2 Book

Included Books

arith2 meta-plus-equal meta-plus-lessp meta-times-equal

other

(in-package "ACL2")

local

(local (include-book "arith2"))

include-book

(include-book "../../../meta/meta-plus-equal")

include-book

(include-book "../../../meta/meta-plus-lessp")

include-book

(include-book "../../../meta/meta-times-equal")

collect-constants-in-equal-of-sumstheorem

(defthm collect-constants-in-equal-of-sums
  (implies (and (syntaxp (and (quotep c1) (quotep c2)))
      (case-split (acl2-numberp c1)))
    (and (equal (equal (+ c2 x) c1) (equal (fix x) (- c1 c2)))
      (equal (equal c1 (+ c2 x)) (equal (fix x) (- c1 c2))))))

collect-constants-in-equal-of-sums-2theorem

(defthm collect-constants-in-equal-of-sums-2
  (implies (syntaxp (and (quotep c1) (quotep c2)))
    (and (equal (equal (+ c2 x) (+ c1 y))
        (equal (fix x) (+ (- c1 c2) y))))))

collect-constants-in-<-of-sumstheorem

(defthm collect-constants-in-<-of-sums
  (implies (syntaxp (and (quotep c1) (quotep c2)))
    (and (equal (< (+ c2 x) c1) (< x (- c1 c2)))
      (equal (< c1 (+ c2 x)) (< (- c1 c2) x)))))

collect-constants-in-<-of-sums-2theorem

(defthm collect-constants-in-<-of-sums-2
  (implies (syntaxp (and (quotep c1) (quotep c2)))
    (equal (< (+ c2 x) (+ c1 y)) (< x (+ (- c1 c2) y)))))

dumbtheorem

(defthm dumb (equal (< x x) nil))