Filtering...

if-normalization

books/arithmetic-5/lib/floor-mod/if-normalization

Included Books

building-blocks
other
(in-package "ACL2")
include-book
(include-book "../basic-ops/building-blocks")
|(floor (if a b c) x)|theorem
(defthm |(floor (if a b c) x)|
  (implies (syntaxp (ok-to-lift-p a))
    (equal (floor (if a
          b
          c)
        x)
      (if a
        (floor b x)
        (floor c x)))))
|(floor y (if a b c))|theorem
(defthm |(floor y (if a b c))|
  (implies (syntaxp (ok-to-lift-p a))
    (equal (floor y
        (if a
          b
          c))
      (if a
        (floor y b)
        (floor y c)))))
|(mod (if a b c) x)|theorem
(defthm |(mod (if a b c) x)|
  (implies (syntaxp (ok-to-lift-p a))
    (equal (mod (if a
          b
          c)
        x)
      (if a
        (mod b x)
        (mod c x)))))
|(mod y (if a b c))|theorem
(defthm |(mod y (if a b c))|
  (implies (syntaxp (ok-to-lift-p a))
    (equal (mod y
        (if a
          b
          c))
      (if a
        (mod y b)
        (mod y c)))))
|(logand (if a b c) x)|theorem
(defthm |(logand (if a b c) x)|
  (implies (syntaxp (ok-to-lift-p a))
    (equal (logand (if a
          b
          c)
        x)
      (if a
        (logand b x)
        (logand c x)))))
|(logand y (if a b c))|theorem
(defthm |(logand y (if a b c))|
  (implies (syntaxp (ok-to-lift-p a))
    (equal (logand y
        (if a
          b
          c))
      (if a
        (logand y b)
        (logand y c)))))
|(lognot (if a b c))|theorem
(defthm |(lognot (if a b c))|
  (implies (syntaxp (ok-to-lift-p a))
    (equal (lognot (if a
          b
          c))
      (if a
        (lognot b)
        (lognot c)))))