blob: 853350962fae44e4373dcf1ac95222c35c443b80 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
(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)
|
