Filtering...

if-normalization

books/arithmetic-5/lib/basic-ops/if-normalization

Included Books

building-blocks
other
(in-package "ACL2")
include-book
(include-book "building-blocks")
|(+ (if a b c) x)|theorem
(defthm |(+ (if a b c) x)|
  (implies (syntaxp (ok-to-lift-p a))
    (equal (+ (if a
          b
          c)
        x)
      (if a
        (+ b x)
        (+ c x)))))
|(+ x (if a b c))|theorem
(defthm |(+ x (if a b c))|
  (implies (syntaxp (ok-to-lift-p a))
    (equal (+ x
        (if a
          b
          c))
      (if a
        (+ x b)
        (+ x c)))))
|(- (if a b c))|theorem
(defthm |(- (if a b c))|
  (implies (syntaxp (ok-to-lift-p a))
    (equal (- (if a
          b
          c))
      (if a
        (- b)
        (- c)))))
|(* (if a b c) x)|theorem
(defthm |(* (if a b c) x)|
  (implies (syntaxp (ok-to-lift-p a))
    (equal (* (if a
          b
          c)
        x)
      (if a
        (* b x)
        (* c x)))))
|(* x (if a b c))|theorem
(defthm |(* x (if a b c))|
  (implies (syntaxp (ok-to-lift-p a))
    (equal (* x
        (if a
          b
          c))
      (if a
        (* x b)
        (* x c)))))
|(/ (if a b c))|theorem
(defthm |(/ (if a b c))|
  (implies (syntaxp (ok-to-lift-p a))
    (equal (/ (if a
          b
          c))
      (if a
        (/ b)
        (/ c)))))
|(expt (if a b c) x)|theorem
(defthm |(expt (if a b c) x)|
  (implies (syntaxp (ok-to-lift-p a))
    (equal (expt (if a
          b
          c)
        x)
      (if a
        (expt b x)
        (expt c x)))))
|(expt x (if a b c))|theorem
(defthm |(expt x (if a b c))|
  (implies (syntaxp (ok-to-lift-p a))
    (equal (expt x
        (if a
          b
          c))
      (if a
        (expt x b)
        (expt x c)))))
|(equal x (if a b c))|theorem
(defthm |(equal x (if a b c))|
  (implies (syntaxp (ok-to-lift-p a))
    (equal (equal x
        (if a
          b
          c))
      (if a
        (equal x b)
        (equal x c)))))
|(equal (if a b c) x)|theorem
(defthm |(equal (if a b c) x)|
  (implies (syntaxp (ok-to-lift-p a))
    (equal (equal (if a
          b
          c)
        x)
      (if a
        (equal b x)
        (equal c x)))))
|(< x (if a b c))|theorem
(defthm |(< x (if a b c))|
  (implies (syntaxp (ok-to-lift-p a))
    (equal (< x
        (if a
          b
          c))
      (if a
        (< x b)
        (< x c)))))
|(< (if a b c) x)|theorem
(defthm |(< (if a b c) x)|
  (implies (syntaxp (ok-to-lift-p a))
    (equal (< (if a
          b
          c)
        x)
      (if a
        (< b x)
        (< c x)))))