(in-package "ACL2")

(defun m (x)
  x)

(defun s (x)
  x)

(defthm m+m
  (equal (+ (m x) (m y))
         (m (+ x y))))

(defthm s+s
  (equal (+ (s x) (s y))
         (s (+ x y))))

(defun m/s (x)
  x)

(defthm m/s+m/s
  (equal (+ (m/s x) (m/s y))
         (m/s (+ x y))))

(defthm m/s*s
  (equal (* (m/s x) (s y))
         (m (* x y))))

(defthm m*/s
  (equal (* (m x) (/ (s y)))
         (m/s (* x (/ y)))))

(defthm m*/m/s
  (equal (* (m x) (/ (m/s y)))
         (m (* x (/ y)))))

(in-theory (disable m s m/s))

(defthm test
  (equal (/ (m x) (/ (m y) (s z)))
         (m (/ x (/ y z))))
  :rule-classes nil)