equal
deleted
inserted
replaced
78 by (Simp_tac 1); |
78 by (Simp_tac 1); |
79 result(); |
79 result(); |
80 |
80 |
81 Goal "#1234567 <= #1234567"; |
81 Goal "#1234567 <= #1234567"; |
82 by (Simp_tac 1); |
82 by (Simp_tac 1); |
|
83 result(); |
|
84 |
|
85 |
|
86 (** Testing the cancellation of complementary terms **) |
|
87 |
|
88 Goal "y + (x + -x) = int 0 + y"; |
|
89 by (Simp_tac 1); |
|
90 result(); |
|
91 |
|
92 Goal "y + (-x + (- y + x)) = int 0"; |
|
93 by (Simp_tac 1); |
|
94 result(); |
|
95 |
|
96 Goal "-x + (y + (- y + x)) = int 0"; |
|
97 by (Simp_tac 1); |
|
98 result(); |
|
99 |
|
100 Goal "x + (x + (- x + (- x + (- y + - z)))) = int 0 - y - z"; |
|
101 by (Simp_tac 1); |
|
102 result(); |
|
103 |
|
104 Goal "x + x - x - x - y - z = int 0 - y - z"; |
|
105 by (Simp_tac 1); |
|
106 result(); |
|
107 |
|
108 Goal "x + y + z - (x + z) = y - int 0"; |
|
109 by (Simp_tac 1); |
|
110 result(); |
|
111 |
|
112 Goal "x+(y+(y+(y+ (-x + -x)))) = int 0 + y - x + y + y"; |
|
113 by (Simp_tac 1); |
|
114 result(); |
|
115 |
|
116 Goal "x+(y+(y+(y+ (-y + -x)))) = y + int 0 + y"; |
|
117 by (Simp_tac 1); |
|
118 result(); |
|
119 |
|
120 Goal "x + y - x + z - x - y - z + x < int 1"; |
|
121 by (Simp_tac 1); |
83 result(); |
122 result(); |
84 |
123 |
85 |
124 |
86 Addsimps normal.intrs; |
125 Addsimps normal.intrs; |
87 |
126 |