pre

other

(in-package "ACL2")

local

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

|Non-numeric x in (+ x y)|theorem

(defthm |Non-numeric x in (+ x y)|
  (implies (not (acl2-numberp x)) (equal (+ x y) (fix y))))

|Non-numeric y in (+ x y)|theorem

(defthm |Non-numeric y in (+ x y)|
  (implies (not (acl2-numberp y)) (equal (+ x y) (fix x))))

|Non-numeric x in (- x)|theorem

(defthm |Non-numeric x in (- x)|
  (implies (not (acl2-numberp x)) (equal (- x) 0)))

|Non-Numeric x in (* x y)|theorem

(defthm |Non-Numeric x in (* x y)|
  (implies (not (acl2-numberp x)) (equal (* x y) 0)))

|Non-Numeric y in (* x y)|theorem

(defthm |Non-Numeric y in (* x y)|
  (implies (not (acl2-numberp y)) (equal (* x y) 0)))

|Non-Numeric x in (/ x)|theorem

(defthm |Non-Numeric x in (/ x)|
  (implies (or (not (acl2-numberp x)) (equal x 0))
    (equal (/ x) 0)))

|Non-Numeric x in (< x y)|theorem

(defthm |Non-Numeric x in (< x y)|
  (implies (not (acl2-numberp x)) (equal (< x y) (< 0 y))))

|Non-Numeric y in (< x y)|theorem

(defthm |Non-Numeric y in (< x y)|
  (implies (not (acl2-numberp y)) (equal (< x y) (< x 0))))

|Non-Numeric x in (denominator x)|theorem

(defthm |Non-Numeric x in (denominator x)|
  (implies (not (rationalp x)) (equal (denominator x) 1)))

|Non-Numeric x in (numerator x)|theorem

(defthm |Non-Numeric x in (numerator x)|
  (implies (not (rationalp x)) (equal (numerator x) 0)))

|(+ 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))))

|(* 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))))

Included Books