Filtering...

complex-rationalp

books/rtl/rel9/arithmetic/complex-rationalp

Included Books

predicate
other
(in-package "ACL2")
local
(local (include-book "predicate"))
complex-rationalp-+-when-second-term-is-rationaltheorem
(defthm complex-rationalp-+-when-second-term-is-rational
  (implies (rationalp y)
    (equal (complex-rationalp (+ x y)) (complex-rationalp x))))
complex-rationalp-+-when-second-term-is-not-complextheorem
(defthm complex-rationalp-+-when-second-term-is-not-complex
  (implies (not (complex-rationalp y))
    (equal (complex-rationalp (+ x y)) (complex-rationalp x))))
complex-rationalp-+-when-first-term-is-rationaltheorem
(defthm complex-rationalp-+-when-first-term-is-rational
  (implies (rationalp x)
    (equal (complex-rationalp (+ x y)) (complex-rationalp y))))
complex-rationalp-+-when-first-term-is-not-complextheorem
(defthm complex-rationalp-+-when-first-term-is-not-complex
  (implies (not (complex-rationalp x))
    (equal (complex-rationalp (+ x y)) (complex-rationalp y))))
complex-rationalp-*-drop-first-term-if-rationaltheorem
(defthm complex-rationalp-*-drop-first-term-if-rational
  (implies (and (case-split (not (equal y 0))) (rationalp y))
    (equal (complex-rationalp (* y x)) (complex-rationalp x))))