1 structure GeneratedCooper = |
|
2 struct |
|
3 nonfix oo; |
|
4 fun nat i = if i < 0 then 0 else i; |
|
5 |
|
6 val one_def0 : int = (0 + 1); |
|
7 |
|
8 datatype num = C of int | Bound of int | CX of int * num | Neg of num |
|
9 | Add of num * num | Sub of num * num | Mul of int * num; |
|
10 |
|
11 fun snd (a, b) = b; |
|
12 |
|
13 fun negateSnd x = (fn (q, r) => (q, ~ r)) x; |
|
14 |
|
15 fun minus_def2 z w = (z + ~ w); |
|
16 |
|
17 fun adjust b = |
|
18 (fn (q, r) => |
|
19 (if (0 <= minus_def2 r b) then (((2 * q) + 1), minus_def2 r b) |
|
20 else ((2 * q), r))); |
|
21 |
|
22 fun negDivAlg a b = |
|
23 (if ((0 <= (a + b)) orelse (b <= 0)) then (~1, (a + b)) |
|
24 else adjust b (negDivAlg a (2 * b))); |
|
25 |
|
26 fun posDivAlg a b = |
|
27 (if ((a < b) orelse (b <= 0)) then (0, a) |
|
28 else adjust b (posDivAlg a (2 * b))); |
|
29 |
|
30 fun divAlg x = |
|
31 (fn (a, b) => |
|
32 (if (0 <= a) |
|
33 then (if (0 <= b) then posDivAlg a b |
|
34 else (if (a = 0) then (0, 0) |
|
35 else negateSnd (negDivAlg (~ a) (~ b)))) |
|
36 else (if (0 < b) then negDivAlg a b |
|
37 else negateSnd (posDivAlg (~ a) (~ b))))) |
|
38 x; |
|
39 |
|
40 fun mod_def1 a b = snd (divAlg (a, b)); |
|
41 |
|
42 fun dvd m n = (mod_def1 n m = 0); |
|
43 |
|
44 fun abs i = (if (i < 0) then ~ i else i); |
|
45 |
|
46 fun less_def3 m n = ((m) < (n)); |
|
47 |
|
48 fun less_eq_def3 m n = Bool.not (less_def3 n m); |
|
49 |
|
50 fun numadd (Add (Mul (c1, Bound n1), r1), Add (Mul (c2, Bound n2), r2)) = |
|
51 (if (n1 = n2) |
|
52 then let val c = (c1 + c2) |
|
53 in (if (c = 0) then numadd (r1, r2) |
|
54 else Add (Mul (c, Bound n1), numadd (r1, r2))) |
|
55 end |
|
56 else (if less_eq_def3 n1 n2 |
|
57 then Add (Mul (c1, Bound n1), |
|
58 numadd (r1, Add (Mul (c2, Bound n2), r2))) |
|
59 else Add (Mul (c2, Bound n2), |
|
60 numadd (Add (Mul (c1, Bound n1), r1), r2)))) |
|
61 | numadd (Add (Mul (c1, Bound n1), r1), C afq) = |
|
62 Add (Mul (c1, Bound n1), numadd (r1, C afq)) |
|
63 | numadd (Add (Mul (c1, Bound n1), r1), Bound afr) = |
|
64 Add (Mul (c1, Bound n1), numadd (r1, Bound afr)) |
|
65 | numadd (Add (Mul (c1, Bound n1), r1), CX (afs, aft)) = |
|
66 Add (Mul (c1, Bound n1), numadd (r1, CX (afs, aft))) |
|
67 | numadd (Add (Mul (c1, Bound n1), r1), Neg afu) = |
|
68 Add (Mul (c1, Bound n1), numadd (r1, Neg afu)) |
|
69 | numadd (Add (Mul (c1, Bound n1), r1), Add (C agx, afw)) = |
|
70 Add (Mul (c1, Bound n1), numadd (r1, Add (C agx, afw))) |
|
71 | numadd (Add (Mul (c1, Bound n1), r1), Add (Bound agy, afw)) = |
|
72 Add (Mul (c1, Bound n1), numadd (r1, Add (Bound agy, afw))) |
|
73 | numadd (Add (Mul (c1, Bound n1), r1), Add (CX (agz, aha), afw)) = |
|
74 Add (Mul (c1, Bound n1), numadd (r1, Add (CX (agz, aha), afw))) |
|
75 | numadd (Add (Mul (c1, Bound n1), r1), Add (Neg ahb, afw)) = |
|
76 Add (Mul (c1, Bound n1), numadd (r1, Add (Neg ahb, afw))) |
|
77 | numadd (Add (Mul (c1, Bound n1), r1), Add (Add (ahc, ahd), afw)) = |
|
78 Add (Mul (c1, Bound n1), numadd (r1, Add (Add (ahc, ahd), afw))) |
|
79 | numadd (Add (Mul (c1, Bound n1), r1), Add (Sub (ahe, ahf), afw)) = |
|
80 Add (Mul (c1, Bound n1), numadd (r1, Add (Sub (ahe, ahf), afw))) |
|
81 | numadd (Add (Mul (c1, Bound n1), r1), Add (Mul (ahg, C aie), afw)) = |
|
82 Add (Mul (c1, Bound n1), numadd (r1, Add (Mul (ahg, C aie), afw))) |
|
83 | numadd (Add (Mul (c1, Bound n1), r1), Add (Mul (ahg, CX (aig, aih)), afw)) = |
|
84 Add (Mul (c1, Bound n1), numadd (r1, Add (Mul (ahg, CX (aig, aih)), afw))) |
|
85 | numadd (Add (Mul (c1, Bound n1), r1), Add (Mul (ahg, Neg aii), afw)) = |
|
86 Add (Mul (c1, Bound n1), numadd (r1, Add (Mul (ahg, Neg aii), afw))) |
|
87 | numadd |
|
88 (Add (Mul (c1, Bound n1), r1), Add (Mul (ahg, Add (aij, aik)), afw)) = |
|
89 Add (Mul (c1, Bound n1), numadd (r1, Add (Mul (ahg, Add (aij, aik)), afw))) |
|
90 | numadd |
|
91 (Add (Mul (c1, Bound n1), r1), Add (Mul (ahg, Sub (ail, aim)), afw)) = |
|
92 Add (Mul (c1, Bound n1), numadd (r1, Add (Mul (ahg, Sub (ail, aim)), afw))) |
|
93 | numadd |
|
94 (Add (Mul (c1, Bound n1), r1), Add (Mul (ahg, Mul (ain, aio)), afw)) = |
|
95 Add (Mul (c1, Bound n1), numadd (r1, Add (Mul (ahg, Mul (ain, aio)), afw))) |
|
96 | numadd (Add (Mul (c1, Bound n1), r1), Sub (afx, afy)) = |
|
97 Add (Mul (c1, Bound n1), numadd (r1, Sub (afx, afy))) |
|
98 | numadd (Add (Mul (c1, Bound n1), r1), Mul (afz, aga)) = |
|
99 Add (Mul (c1, Bound n1), numadd (r1, Mul (afz, aga))) |
|
100 | numadd (C w, Add (Mul (c2, Bound n2), r2)) = |
|
101 Add (Mul (c2, Bound n2), numadd (C w, r2)) |
|
102 | numadd (Bound x, Add (Mul (c2, Bound n2), r2)) = |
|
103 Add (Mul (c2, Bound n2), numadd (Bound x, r2)) |
|
104 | numadd (CX (y, z), Add (Mul (c2, Bound n2), r2)) = |
|
105 Add (Mul (c2, Bound n2), numadd (CX (y, z), r2)) |
|
106 | numadd (Neg ab, Add (Mul (c2, Bound n2), r2)) = |
|
107 Add (Mul (c2, Bound n2), numadd (Neg ab, r2)) |
|
108 | numadd (Add (C li, ad), Add (Mul (c2, Bound n2), r2)) = |
|
109 Add (Mul (c2, Bound n2), numadd (Add (C li, ad), r2)) |
|
110 | numadd (Add (Bound lj, ad), Add (Mul (c2, Bound n2), r2)) = |
|
111 Add (Mul (c2, Bound n2), numadd (Add (Bound lj, ad), r2)) |
|
112 | numadd (Add (CX (lk, ll), ad), Add (Mul (c2, Bound n2), r2)) = |
|
113 Add (Mul (c2, Bound n2), numadd (Add (CX (lk, ll), ad), r2)) |
|
114 | numadd (Add (Neg lm, ad), Add (Mul (c2, Bound n2), r2)) = |
|
115 Add (Mul (c2, Bound n2), numadd (Add (Neg lm, ad), r2)) |
|
116 | numadd (Add (Add (ln, lo), ad), Add (Mul (c2, Bound n2), r2)) = |
|
117 Add (Mul (c2, Bound n2), numadd (Add (Add (ln, lo), ad), r2)) |
|
118 | numadd (Add (Sub (lp, lq), ad), Add (Mul (c2, Bound n2), r2)) = |
|
119 Add (Mul (c2, Bound n2), numadd (Add (Sub (lp, lq), ad), r2)) |
|
120 | numadd (Add (Mul (lr, C abv), ad), Add (Mul (c2, Bound n2), r2)) = |
|
121 Add (Mul (c2, Bound n2), numadd (Add (Mul (lr, C abv), ad), r2)) |
|
122 | numadd (Add (Mul (lr, CX (abx, aby)), ad), Add (Mul (c2, Bound n2), r2)) = |
|
123 Add (Mul (c2, Bound n2), numadd (Add (Mul (lr, CX (abx, aby)), ad), r2)) |
|
124 | numadd (Add (Mul (lr, Neg abz), ad), Add (Mul (c2, Bound n2), r2)) = |
|
125 Add (Mul (c2, Bound n2), numadd (Add (Mul (lr, Neg abz), ad), r2)) |
|
126 | numadd (Add (Mul (lr, Add (aca, acb)), ad), Add (Mul (c2, Bound n2), r2)) = |
|
127 Add (Mul (c2, Bound n2), numadd (Add (Mul (lr, Add (aca, acb)), ad), r2)) |
|
128 | numadd (Add (Mul (lr, Sub (acc, acd)), ad), Add (Mul (c2, Bound n2), r2)) = |
|
129 Add (Mul (c2, Bound n2), numadd (Add (Mul (lr, Sub (acc, acd)), ad), r2)) |
|
130 | numadd (Add (Mul (lr, Mul (ace, acf)), ad), Add (Mul (c2, Bound n2), r2)) = |
|
131 Add (Mul (c2, Bound n2), numadd (Add (Mul (lr, Mul (ace, acf)), ad), r2)) |
|
132 | numadd (Sub (ae, af), Add (Mul (c2, Bound n2), r2)) = |
|
133 Add (Mul (c2, Bound n2), numadd (Sub (ae, af), r2)) |
|
134 | numadd (Mul (ag, ah), Add (Mul (c2, Bound n2), r2)) = |
|
135 Add (Mul (c2, Bound n2), numadd (Mul (ag, ah), r2)) |
|
136 | numadd (C b1, C b2) = C (b1 + b2) |
|
137 | numadd (C ai, Bound bf) = Add (C ai, Bound bf) |
|
138 | numadd (C ai, CX (bg, bh)) = Add (C ai, CX (bg, bh)) |
|
139 | numadd (C ai, Neg bi) = Add (C ai, Neg bi) |
|
140 | numadd (C ai, Add (C ca, bk)) = Add (C ai, Add (C ca, bk)) |
|
141 | numadd (C ai, Add (Bound cb, bk)) = Add (C ai, Add (Bound cb, bk)) |
|
142 | numadd (C ai, Add (CX (cc, cd), bk)) = Add (C ai, Add (CX (cc, cd), bk)) |
|
143 | numadd (C ai, Add (Neg ce, bk)) = Add (C ai, Add (Neg ce, bk)) |
|
144 | numadd (C ai, Add (Add (cf, cg), bk)) = Add (C ai, Add (Add (cf, cg), bk)) |
|
145 | numadd (C ai, Add (Sub (ch, ci), bk)) = Add (C ai, Add (Sub (ch, ci), bk)) |
|
146 | numadd (C ai, Add (Mul (cj, C cw), bk)) = |
|
147 Add (C ai, Add (Mul (cj, C cw), bk)) |
|
148 | numadd (C ai, Add (Mul (cj, CX (cy, cz)), bk)) = |
|
149 Add (C ai, Add (Mul (cj, CX (cy, cz)), bk)) |
|
150 | numadd (C ai, Add (Mul (cj, Neg da), bk)) = |
|
151 Add (C ai, Add (Mul (cj, Neg da), bk)) |
|
152 | numadd (C ai, Add (Mul (cj, Add (db, dc)), bk)) = |
|
153 Add (C ai, Add (Mul (cj, Add (db, dc)), bk)) |
|
154 | numadd (C ai, Add (Mul (cj, Sub (dd, de)), bk)) = |
|
155 Add (C ai, Add (Mul (cj, Sub (dd, de)), bk)) |
|
156 | numadd (C ai, Add (Mul (cj, Mul (df, dg)), bk)) = |
|
157 Add (C ai, Add (Mul (cj, Mul (df, dg)), bk)) |
|
158 | numadd (C ai, Sub (bl, bm)) = Add (C ai, Sub (bl, bm)) |
|
159 | numadd (C ai, Mul (bn, bo)) = Add (C ai, Mul (bn, bo)) |
|
160 | numadd (Bound aj, C ds) = Add (Bound aj, C ds) |
|
161 | numadd (Bound aj, Bound dt) = Add (Bound aj, Bound dt) |
|
162 | numadd (Bound aj, CX (du, dv)) = Add (Bound aj, CX (du, dv)) |
|
163 | numadd (Bound aj, Neg dw) = Add (Bound aj, Neg dw) |
|
164 | numadd (Bound aj, Add (C eo, dy)) = Add (Bound aj, Add (C eo, dy)) |
|
165 | numadd (Bound aj, Add (Bound ep, dy)) = Add (Bound aj, Add (Bound ep, dy)) |
|
166 | numadd (Bound aj, Add (CX (eq, er), dy)) = |
|
167 Add (Bound aj, Add (CX (eq, er), dy)) |
|
168 | numadd (Bound aj, Add (Neg es, dy)) = Add (Bound aj, Add (Neg es, dy)) |
|
169 | numadd (Bound aj, Add (Add (et, eu), dy)) = |
|
170 Add (Bound aj, Add (Add (et, eu), dy)) |
|
171 | numadd (Bound aj, Add (Sub (ev, ew), dy)) = |
|
172 Add (Bound aj, Add (Sub (ev, ew), dy)) |
|
173 | numadd (Bound aj, Add (Mul (ex, C fk), dy)) = |
|
174 Add (Bound aj, Add (Mul (ex, C fk), dy)) |
|
175 | numadd (Bound aj, Add (Mul (ex, CX (fm, fn')), dy)) = |
|
176 Add (Bound aj, Add (Mul (ex, CX (fm, fn')), dy)) |
|
177 | numadd (Bound aj, Add (Mul (ex, Neg fo), dy)) = |
|
178 Add (Bound aj, Add (Mul (ex, Neg fo), dy)) |
|
179 | numadd (Bound aj, Add (Mul (ex, Add (fp, fq)), dy)) = |
|
180 Add (Bound aj, Add (Mul (ex, Add (fp, fq)), dy)) |
|
181 | numadd (Bound aj, Add (Mul (ex, Sub (fr, fs)), dy)) = |
|
182 Add (Bound aj, Add (Mul (ex, Sub (fr, fs)), dy)) |
|
183 | numadd (Bound aj, Add (Mul (ex, Mul (ft, fu)), dy)) = |
|
184 Add (Bound aj, Add (Mul (ex, Mul (ft, fu)), dy)) |
|
185 | numadd (Bound aj, Sub (dz, ea)) = Add (Bound aj, Sub (dz, ea)) |
|
186 | numadd (Bound aj, Mul (eb, ec)) = Add (Bound aj, Mul (eb, ec)) |
|
187 | numadd (CX (ak, al), C gg) = Add (CX (ak, al), C gg) |
|
188 | numadd (CX (ak, al), Bound gh) = Add (CX (ak, al), Bound gh) |
|
189 | numadd (CX (ak, al), CX (gi, gj)) = Add (CX (ak, al), CX (gi, gj)) |
|
190 | numadd (CX (ak, al), Neg gk) = Add (CX (ak, al), Neg gk) |
|
191 | numadd (CX (ak, al), Add (C hc, gm)) = Add (CX (ak, al), Add (C hc, gm)) |
|
192 | numadd (CX (ak, al), Add (Bound hd, gm)) = |
|
193 Add (CX (ak, al), Add (Bound hd, gm)) |
|
194 | numadd (CX (ak, al), Add (CX (he, hf), gm)) = |
|
195 Add (CX (ak, al), Add (CX (he, hf), gm)) |
|
196 | numadd (CX (ak, al), Add (Neg hg, gm)) = Add (CX (ak, al), Add (Neg hg, gm)) |
|
197 | numadd (CX (ak, al), Add (Add (hh, hi), gm)) = |
|
198 Add (CX (ak, al), Add (Add (hh, hi), gm)) |
|
199 | numadd (CX (ak, al), Add (Sub (hj, hk), gm)) = |
|
200 Add (CX (ak, al), Add (Sub (hj, hk), gm)) |
|
201 | numadd (CX (ak, al), Add (Mul (hl, C hy), gm)) = |
|
202 Add (CX (ak, al), Add (Mul (hl, C hy), gm)) |
|
203 | numadd (CX (ak, al), Add (Mul (hl, CX (ia, ib)), gm)) = |
|
204 Add (CX (ak, al), Add (Mul (hl, CX (ia, ib)), gm)) |
|
205 | numadd (CX (ak, al), Add (Mul (hl, Neg ic), gm)) = |
|
206 Add (CX (ak, al), Add (Mul (hl, Neg ic), gm)) |
|
207 | numadd (CX (ak, al), Add (Mul (hl, Add (id, ie)), gm)) = |
|
208 Add (CX (ak, al), Add (Mul (hl, Add (id, ie)), gm)) |
|
209 | numadd (CX (ak, al), Add (Mul (hl, Sub (if', ig)), gm)) = |
|
210 Add (CX (ak, al), Add (Mul (hl, Sub (if', ig)), gm)) |
|
211 | numadd (CX (ak, al), Add (Mul (hl, Mul (ih, ii)), gm)) = |
|
212 Add (CX (ak, al), Add (Mul (hl, Mul (ih, ii)), gm)) |
|
213 | numadd (CX (ak, al), Sub (gn, go)) = Add (CX (ak, al), Sub (gn, go)) |
|
214 | numadd (CX (ak, al), Mul (gp, gq)) = Add (CX (ak, al), Mul (gp, gq)) |
|
215 | numadd (Neg am, C iu) = Add (Neg am, C iu) |
|
216 | numadd (Neg am, Bound iv) = Add (Neg am, Bound iv) |
|
217 | numadd (Neg am, CX (iw, ix)) = Add (Neg am, CX (iw, ix)) |
|
218 | numadd (Neg am, Neg iy) = Add (Neg am, Neg iy) |
|
219 | numadd (Neg am, Add (C jq, ja)) = Add (Neg am, Add (C jq, ja)) |
|
220 | numadd (Neg am, Add (Bound jr, ja)) = Add (Neg am, Add (Bound jr, ja)) |
|
221 | numadd (Neg am, Add (CX (js, jt), ja)) = Add (Neg am, Add (CX (js, jt), ja)) |
|
222 | numadd (Neg am, Add (Neg ju, ja)) = Add (Neg am, Add (Neg ju, ja)) |
|
223 | numadd (Neg am, Add (Add (jv, jw), ja)) = |
|
224 Add (Neg am, Add (Add (jv, jw), ja)) |
|
225 | numadd (Neg am, Add (Sub (jx, jy), ja)) = |
|
226 Add (Neg am, Add (Sub (jx, jy), ja)) |
|
227 | numadd (Neg am, Add (Mul (jz, C km), ja)) = |
|
228 Add (Neg am, Add (Mul (jz, C km), ja)) |
|
229 | numadd (Neg am, Add (Mul (jz, CX (ko, kp)), ja)) = |
|
230 Add (Neg am, Add (Mul (jz, CX (ko, kp)), ja)) |
|
231 | numadd (Neg am, Add (Mul (jz, Neg kq), ja)) = |
|
232 Add (Neg am, Add (Mul (jz, Neg kq), ja)) |
|
233 | numadd (Neg am, Add (Mul (jz, Add (kr, ks)), ja)) = |
|
234 Add (Neg am, Add (Mul (jz, Add (kr, ks)), ja)) |
|
235 | numadd (Neg am, Add (Mul (jz, Sub (kt, ku)), ja)) = |
|
236 Add (Neg am, Add (Mul (jz, Sub (kt, ku)), ja)) |
|
237 | numadd (Neg am, Add (Mul (jz, Mul (kv, kw)), ja)) = |
|
238 Add (Neg am, Add (Mul (jz, Mul (kv, kw)), ja)) |
|
239 | numadd (Neg am, Sub (jb, jc)) = Add (Neg am, Sub (jb, jc)) |
|
240 | numadd (Neg am, Mul (jd, je)) = Add (Neg am, Mul (jd, je)) |
|
241 | numadd (Add (C lt, ao), C mp) = Add (Add (C lt, ao), C mp) |
|
242 | numadd (Add (C lt, ao), Bound mq) = Add (Add (C lt, ao), Bound mq) |
|
243 | numadd (Add (C lt, ao), CX (mr, ms)) = Add (Add (C lt, ao), CX (mr, ms)) |
|
244 | numadd (Add (C lt, ao), Neg mt) = Add (Add (C lt, ao), Neg mt) |
|
245 | numadd (Add (C lt, ao), Add (C nl, mv)) = |
|
246 Add (Add (C lt, ao), Add (C nl, mv)) |
|
247 | numadd (Add (C lt, ao), Add (Bound nm, mv)) = |
|
248 Add (Add (C lt, ao), Add (Bound nm, mv)) |
|
249 | numadd (Add (C lt, ao), Add (CX (nn, no), mv)) = |
|
250 Add (Add (C lt, ao), Add (CX (nn, no), mv)) |
|
251 | numadd (Add (C lt, ao), Add (Neg np, mv)) = |
|
252 Add (Add (C lt, ao), Add (Neg np, mv)) |
|
253 | numadd (Add (C lt, ao), Add (Add (nq, nr), mv)) = |
|
254 Add (Add (C lt, ao), Add (Add (nq, nr), mv)) |
|
255 | numadd (Add (C lt, ao), Add (Sub (ns, nt), mv)) = |
|
256 Add (Add (C lt, ao), Add (Sub (ns, nt), mv)) |
|
257 | numadd (Add (C lt, ao), Add (Mul (nu, C oh), mv)) = |
|
258 Add (Add (C lt, ao), Add (Mul (nu, C oh), mv)) |
|
259 | numadd (Add (C lt, ao), Add (Mul (nu, CX (oj, ok)), mv)) = |
|
260 Add (Add (C lt, ao), Add (Mul (nu, CX (oj, ok)), mv)) |
|
261 | numadd (Add (C lt, ao), Add (Mul (nu, Neg ol), mv)) = |
|
262 Add (Add (C lt, ao), Add (Mul (nu, Neg ol), mv)) |
|
263 | numadd (Add (C lt, ao), Add (Mul (nu, Add (om, on)), mv)) = |
|
264 Add (Add (C lt, ao), Add (Mul (nu, Add (om, on)), mv)) |
|
265 | numadd (Add (C lt, ao), Add (Mul (nu, Sub (oo, op')), mv)) = |
|
266 Add (Add (C lt, ao), Add (Mul (nu, Sub (oo, op')), mv)) |
|
267 | numadd (Add (C lt, ao), Add (Mul (nu, Mul (oq, or)), mv)) = |
|
268 Add (Add (C lt, ao), Add (Mul (nu, Mul (oq, or)), mv)) |
|
269 | numadd (Add (C lt, ao), Sub (mw, mx)) = Add (Add (C lt, ao), Sub (mw, mx)) |
|
270 | numadd (Add (C lt, ao), Mul (my, mz)) = Add (Add (C lt, ao), Mul (my, mz)) |
|
271 | numadd (Add (Bound lu, ao), C pd) = Add (Add (Bound lu, ao), C pd) |
|
272 | numadd (Add (Bound lu, ao), Bound pe) = Add (Add (Bound lu, ao), Bound pe) |
|
273 | numadd (Add (Bound lu, ao), CX (pf, pg)) = |
|
274 Add (Add (Bound lu, ao), CX (pf, pg)) |
|
275 | numadd (Add (Bound lu, ao), Neg ph) = Add (Add (Bound lu, ao), Neg ph) |
|
276 | numadd (Add (Bound lu, ao), Add (C pz, pj)) = |
|
277 Add (Add (Bound lu, ao), Add (C pz, pj)) |
|
278 | numadd (Add (Bound lu, ao), Add (Bound qa, pj)) = |
|
279 Add (Add (Bound lu, ao), Add (Bound qa, pj)) |
|
280 | numadd (Add (Bound lu, ao), Add (CX (qb, qc), pj)) = |
|
281 Add (Add (Bound lu, ao), Add (CX (qb, qc), pj)) |
|
282 | numadd (Add (Bound lu, ao), Add (Neg qd, pj)) = |
|
283 Add (Add (Bound lu, ao), Add (Neg qd, pj)) |
|
284 | numadd (Add (Bound lu, ao), Add (Add (qe, qf), pj)) = |
|
285 Add (Add (Bound lu, ao), Add (Add (qe, qf), pj)) |
|
286 | numadd (Add (Bound lu, ao), Add (Sub (qg, qh), pj)) = |
|
287 Add (Add (Bound lu, ao), Add (Sub (qg, qh), pj)) |
|
288 | numadd (Add (Bound lu, ao), Add (Mul (qi, C qv), pj)) = |
|
289 Add (Add (Bound lu, ao), Add (Mul (qi, C qv), pj)) |
|
290 | numadd (Add (Bound lu, ao), Add (Mul (qi, CX (qx, qy)), pj)) = |
|
291 Add (Add (Bound lu, ao), Add (Mul (qi, CX (qx, qy)), pj)) |
|
292 | numadd (Add (Bound lu, ao), Add (Mul (qi, Neg qz), pj)) = |
|
293 Add (Add (Bound lu, ao), Add (Mul (qi, Neg qz), pj)) |
|
294 | numadd (Add (Bound lu, ao), Add (Mul (qi, Add (ra, rb)), pj)) = |
|
295 Add (Add (Bound lu, ao), Add (Mul (qi, Add (ra, rb)), pj)) |
|
296 | numadd (Add (Bound lu, ao), Add (Mul (qi, Sub (rc, rd)), pj)) = |
|
297 Add (Add (Bound lu, ao), Add (Mul (qi, Sub (rc, rd)), pj)) |
|
298 | numadd (Add (Bound lu, ao), Add (Mul (qi, Mul (re, rf)), pj)) = |
|
299 Add (Add (Bound lu, ao), Add (Mul (qi, Mul (re, rf)), pj)) |
|
300 | numadd (Add (Bound lu, ao), Sub (pk, pl)) = |
|
301 Add (Add (Bound lu, ao), Sub (pk, pl)) |
|
302 | numadd (Add (Bound lu, ao), Mul (pm, pn)) = |
|
303 Add (Add (Bound lu, ao), Mul (pm, pn)) |
|
304 | numadd (Add (CX (lv, lw), ao), C rr) = Add (Add (CX (lv, lw), ao), C rr) |
|
305 | numadd (Add (CX (lv, lw), ao), Bound rs) = |
|
306 Add (Add (CX (lv, lw), ao), Bound rs) |
|
307 | numadd (Add (CX (lv, lw), ao), CX (rt, ru)) = |
|
308 Add (Add (CX (lv, lw), ao), CX (rt, ru)) |
|
309 | numadd (Add (CX (lv, lw), ao), Neg rv) = Add (Add (CX (lv, lw), ao), Neg rv) |
|
310 | numadd (Add (CX (lv, lw), ao), Add (C sn, rx)) = |
|
311 Add (Add (CX (lv, lw), ao), Add (C sn, rx)) |
|
312 | numadd (Add (CX (lv, lw), ao), Add (Bound so, rx)) = |
|
313 Add (Add (CX (lv, lw), ao), Add (Bound so, rx)) |
|
314 | numadd (Add (CX (lv, lw), ao), Add (CX (sp, sq), rx)) = |
|
315 Add (Add (CX (lv, lw), ao), Add (CX (sp, sq), rx)) |
|
316 | numadd (Add (CX (lv, lw), ao), Add (Neg sr, rx)) = |
|
317 Add (Add (CX (lv, lw), ao), Add (Neg sr, rx)) |
|
318 | numadd (Add (CX (lv, lw), ao), Add (Add (ss, st), rx)) = |
|
319 Add (Add (CX (lv, lw), ao), Add (Add (ss, st), rx)) |
|
320 | numadd (Add (CX (lv, lw), ao), Add (Sub (su, sv), rx)) = |
|
321 Add (Add (CX (lv, lw), ao), Add (Sub (su, sv), rx)) |
|
322 | numadd (Add (CX (lv, lw), ao), Add (Mul (sw, C tj), rx)) = |
|
323 Add (Add (CX (lv, lw), ao), Add (Mul (sw, C tj), rx)) |
|
324 | numadd (Add (CX (lv, lw), ao), Add (Mul (sw, CX (tl, tm)), rx)) = |
|
325 Add (Add (CX (lv, lw), ao), Add (Mul (sw, CX (tl, tm)), rx)) |
|
326 | numadd (Add (CX (lv, lw), ao), Add (Mul (sw, Neg tn), rx)) = |
|
327 Add (Add (CX (lv, lw), ao), Add (Mul (sw, Neg tn), rx)) |
|
328 | numadd (Add (CX (lv, lw), ao), Add (Mul (sw, Add (to, tp)), rx)) = |
|
329 Add (Add (CX (lv, lw), ao), Add (Mul (sw, Add (to, tp)), rx)) |
|
330 | numadd (Add (CX (lv, lw), ao), Add (Mul (sw, Sub (tq, tr)), rx)) = |
|
331 Add (Add (CX (lv, lw), ao), Add (Mul (sw, Sub (tq, tr)), rx)) |
|
332 | numadd (Add (CX (lv, lw), ao), Add (Mul (sw, Mul (ts, tt)), rx)) = |
|
333 Add (Add (CX (lv, lw), ao), Add (Mul (sw, Mul (ts, tt)), rx)) |
|
334 | numadd (Add (CX (lv, lw), ao), Sub (ry, rz)) = |
|
335 Add (Add (CX (lv, lw), ao), Sub (ry, rz)) |
|
336 | numadd (Add (CX (lv, lw), ao), Mul (sa, sb)) = |
|
337 Add (Add (CX (lv, lw), ao), Mul (sa, sb)) |
|
338 | numadd (Add (Neg lx, ao), C uf) = Add (Add (Neg lx, ao), C uf) |
|
339 | numadd (Add (Neg lx, ao), Bound ug) = Add (Add (Neg lx, ao), Bound ug) |
|
340 | numadd (Add (Neg lx, ao), CX (uh, ui)) = Add (Add (Neg lx, ao), CX (uh, ui)) |
|
341 | numadd (Add (Neg lx, ao), Neg uj) = Add (Add (Neg lx, ao), Neg uj) |
|
342 | numadd (Add (Neg lx, ao), Add (C vb, ul)) = |
|
343 Add (Add (Neg lx, ao), Add (C vb, ul)) |
|
344 | numadd (Add (Neg lx, ao), Add (Bound vc, ul)) = |
|
345 Add (Add (Neg lx, ao), Add (Bound vc, ul)) |
|
346 | numadd (Add (Neg lx, ao), Add (CX (vd, ve), ul)) = |
|
347 Add (Add (Neg lx, ao), Add (CX (vd, ve), ul)) |
|
348 | numadd (Add (Neg lx, ao), Add (Neg vf, ul)) = |
|
349 Add (Add (Neg lx, ao), Add (Neg vf, ul)) |
|
350 | numadd (Add (Neg lx, ao), Add (Add (vg, vh), ul)) = |
|
351 Add (Add (Neg lx, ao), Add (Add (vg, vh), ul)) |
|
352 | numadd (Add (Neg lx, ao), Add (Sub (vi, vj), ul)) = |
|
353 Add (Add (Neg lx, ao), Add (Sub (vi, vj), ul)) |
|
354 | numadd (Add (Neg lx, ao), Add (Mul (vk, C vx), ul)) = |
|
355 Add (Add (Neg lx, ao), Add (Mul (vk, C vx), ul)) |
|
356 | numadd (Add (Neg lx, ao), Add (Mul (vk, CX (vz, wa)), ul)) = |
|
357 Add (Add (Neg lx, ao), Add (Mul (vk, CX (vz, wa)), ul)) |
|
358 | numadd (Add (Neg lx, ao), Add (Mul (vk, Neg wb), ul)) = |
|
359 Add (Add (Neg lx, ao), Add (Mul (vk, Neg wb), ul)) |
|
360 | numadd (Add (Neg lx, ao), Add (Mul (vk, Add (wc, wd)), ul)) = |
|
361 Add (Add (Neg lx, ao), Add (Mul (vk, Add (wc, wd)), ul)) |
|
362 | numadd (Add (Neg lx, ao), Add (Mul (vk, Sub (we, wf)), ul)) = |
|
363 Add (Add (Neg lx, ao), Add (Mul (vk, Sub (we, wf)), ul)) |
|
364 | numadd (Add (Neg lx, ao), Add (Mul (vk, Mul (wg, wh)), ul)) = |
|
365 Add (Add (Neg lx, ao), Add (Mul (vk, Mul (wg, wh)), ul)) |
|
366 | numadd (Add (Neg lx, ao), Sub (um, un)) = |
|
367 Add (Add (Neg lx, ao), Sub (um, un)) |
|
368 | numadd (Add (Neg lx, ao), Mul (uo, up)) = |
|
369 Add (Add (Neg lx, ao), Mul (uo, up)) |
|
370 | numadd (Add (Add (ly, lz), ao), C wt) = Add (Add (Add (ly, lz), ao), C wt) |
|
371 | numadd (Add (Add (ly, lz), ao), Bound wu) = |
|
372 Add (Add (Add (ly, lz), ao), Bound wu) |
|
373 | numadd (Add (Add (ly, lz), ao), CX (wv, ww)) = |
|
374 Add (Add (Add (ly, lz), ao), CX (wv, ww)) |
|
375 | numadd (Add (Add (ly, lz), ao), Neg wx) = |
|
376 Add (Add (Add (ly, lz), ao), Neg wx) |
|
377 | numadd (Add (Add (ly, lz), ao), Add (C xp, wz)) = |
|
378 Add (Add (Add (ly, lz), ao), Add (C xp, wz)) |
|
379 | numadd (Add (Add (ly, lz), ao), Add (Bound xq, wz)) = |
|
380 Add (Add (Add (ly, lz), ao), Add (Bound xq, wz)) |
|
381 | numadd (Add (Add (ly, lz), ao), Add (CX (xr, xs), wz)) = |
|
382 Add (Add (Add (ly, lz), ao), Add (CX (xr, xs), wz)) |
|
383 | numadd (Add (Add (ly, lz), ao), Add (Neg xt, wz)) = |
|
384 Add (Add (Add (ly, lz), ao), Add (Neg xt, wz)) |
|
385 | numadd (Add (Add (ly, lz), ao), Add (Add (xu, xv), wz)) = |
|
386 Add (Add (Add (ly, lz), ao), Add (Add (xu, xv), wz)) |
|
387 | numadd (Add (Add (ly, lz), ao), Add (Sub (xw, xx), wz)) = |
|
388 Add (Add (Add (ly, lz), ao), Add (Sub (xw, xx), wz)) |
|
389 | numadd (Add (Add (ly, lz), ao), Add (Mul (xy, C yl), wz)) = |
|
390 Add (Add (Add (ly, lz), ao), Add (Mul (xy, C yl), wz)) |
|
391 | numadd (Add (Add (ly, lz), ao), Add (Mul (xy, CX (yn, yo)), wz)) = |
|
392 Add (Add (Add (ly, lz), ao), Add (Mul (xy, CX (yn, yo)), wz)) |
|
393 | numadd (Add (Add (ly, lz), ao), Add (Mul (xy, Neg yp), wz)) = |
|
394 Add (Add (Add (ly, lz), ao), Add (Mul (xy, Neg yp), wz)) |
|
395 | numadd (Add (Add (ly, lz), ao), Add (Mul (xy, Add (yq, yr)), wz)) = |
|
396 Add (Add (Add (ly, lz), ao), Add (Mul (xy, Add (yq, yr)), wz)) |
|
397 | numadd (Add (Add (ly, lz), ao), Add (Mul (xy, Sub (ys, yt)), wz)) = |
|
398 Add (Add (Add (ly, lz), ao), Add (Mul (xy, Sub (ys, yt)), wz)) |
|
399 | numadd (Add (Add (ly, lz), ao), Add (Mul (xy, Mul (yu, yv)), wz)) = |
|
400 Add (Add (Add (ly, lz), ao), Add (Mul (xy, Mul (yu, yv)), wz)) |
|
401 | numadd (Add (Add (ly, lz), ao), Sub (xa, xb)) = |
|
402 Add (Add (Add (ly, lz), ao), Sub (xa, xb)) |
|
403 | numadd (Add (Add (ly, lz), ao), Mul (xc, xd)) = |
|
404 Add (Add (Add (ly, lz), ao), Mul (xc, xd)) |
|
405 | numadd (Add (Sub (ma, mb), ao), C zh) = Add (Add (Sub (ma, mb), ao), C zh) |
|
406 | numadd (Add (Sub (ma, mb), ao), Bound zi) = |
|
407 Add (Add (Sub (ma, mb), ao), Bound zi) |
|
408 | numadd (Add (Sub (ma, mb), ao), CX (zj, zk)) = |
|
409 Add (Add (Sub (ma, mb), ao), CX (zj, zk)) |
|
410 | numadd (Add (Sub (ma, mb), ao), Neg zl) = |
|
411 Add (Add (Sub (ma, mb), ao), Neg zl) |
|
412 | numadd (Add (Sub (ma, mb), ao), Add (C aad, zn)) = |
|
413 Add (Add (Sub (ma, mb), ao), Add (C aad, zn)) |
|
414 | numadd (Add (Sub (ma, mb), ao), Add (Bound aae, zn)) = |
|
415 Add (Add (Sub (ma, mb), ao), Add (Bound aae, zn)) |
|
416 | numadd (Add (Sub (ma, mb), ao), Add (CX (aaf, aag), zn)) = |
|
417 Add (Add (Sub (ma, mb), ao), Add (CX (aaf, aag), zn)) |
|
418 | numadd (Add (Sub (ma, mb), ao), Add (Neg aah, zn)) = |
|
419 Add (Add (Sub (ma, mb), ao), Add (Neg aah, zn)) |
|
420 | numadd (Add (Sub (ma, mb), ao), Add (Add (aai, aaj), zn)) = |
|
421 Add (Add (Sub (ma, mb), ao), Add (Add (aai, aaj), zn)) |
|
422 | numadd (Add (Sub (ma, mb), ao), Add (Sub (aak, aal), zn)) = |
|
423 Add (Add (Sub (ma, mb), ao), Add (Sub (aak, aal), zn)) |
|
424 | numadd (Add (Sub (ma, mb), ao), Add (Mul (aam, C aaz), zn)) = |
|
425 Add (Add (Sub (ma, mb), ao), Add (Mul (aam, C aaz), zn)) |
|
426 | numadd (Add (Sub (ma, mb), ao), Add (Mul (aam, CX (abb, abc)), zn)) = |
|
427 Add (Add (Sub (ma, mb), ao), Add (Mul (aam, CX (abb, abc)), zn)) |
|
428 | numadd (Add (Sub (ma, mb), ao), Add (Mul (aam, Neg abd), zn)) = |
|
429 Add (Add (Sub (ma, mb), ao), Add (Mul (aam, Neg abd), zn)) |
|
430 | numadd (Add (Sub (ma, mb), ao), Add (Mul (aam, Add (abe, abf)), zn)) = |
|
431 Add (Add (Sub (ma, mb), ao), Add (Mul (aam, Add (abe, abf)), zn)) |
|
432 | numadd (Add (Sub (ma, mb), ao), Add (Mul (aam, Sub (abg, abh)), zn)) = |
|
433 Add (Add (Sub (ma, mb), ao), Add (Mul (aam, Sub (abg, abh)), zn)) |
|
434 | numadd (Add (Sub (ma, mb), ao), Add (Mul (aam, Mul (abi, abj)), zn)) = |
|
435 Add (Add (Sub (ma, mb), ao), Add (Mul (aam, Mul (abi, abj)), zn)) |
|
436 | numadd (Add (Sub (ma, mb), ao), Sub (zo, zp)) = |
|
437 Add (Add (Sub (ma, mb), ao), Sub (zo, zp)) |
|
438 | numadd (Add (Sub (ma, mb), ao), Mul (zq, zr)) = |
|
439 Add (Add (Sub (ma, mb), ao), Mul (zq, zr)) |
|
440 | numadd (Add (Mul (mc, C acg), ao), C adc) = |
|
441 Add (Add (Mul (mc, C acg), ao), C adc) |
|
442 | numadd (Add (Mul (mc, C acg), ao), Bound add) = |
|
443 Add (Add (Mul (mc, C acg), ao), Bound add) |
|
444 | numadd (Add (Mul (mc, C acg), ao), CX (ade, adf)) = |
|
445 Add (Add (Mul (mc, C acg), ao), CX (ade, adf)) |
|
446 | numadd (Add (Mul (mc, C acg), ao), Neg adg) = |
|
447 Add (Add (Mul (mc, C acg), ao), Neg adg) |
|
448 | numadd (Add (Mul (mc, C acg), ao), Add (C ady, adi)) = |
|
449 Add (Add (Mul (mc, C acg), ao), Add (C ady, adi)) |
|
450 | numadd (Add (Mul (mc, C acg), ao), Add (Bound adz, adi)) = |
|
451 Add (Add (Mul (mc, C acg), ao), Add (Bound adz, adi)) |
|
452 | numadd (Add (Mul (mc, C acg), ao), Add (CX (aea, aeb), adi)) = |
|
453 Add (Add (Mul (mc, C acg), ao), Add (CX (aea, aeb), adi)) |
|
454 | numadd (Add (Mul (mc, C acg), ao), Add (Neg aec, adi)) = |
|
455 Add (Add (Mul (mc, C acg), ao), Add (Neg aec, adi)) |
|
456 | numadd (Add (Mul (mc, C acg), ao), Add (Add (aed, aee), adi)) = |
|
457 Add (Add (Mul (mc, C acg), ao), Add (Add (aed, aee), adi)) |
|
458 | numadd (Add (Mul (mc, C acg), ao), Add (Sub (aef, aeg), adi)) = |
|
459 Add (Add (Mul (mc, C acg), ao), Add (Sub (aef, aeg), adi)) |
|
460 | numadd (Add (Mul (mc, C acg), ao), Add (Mul (aeh, C aeu), adi)) = |
|
461 Add (Add (Mul (mc, C acg), ao), Add (Mul (aeh, C aeu), adi)) |
|
462 | numadd (Add (Mul (mc, C acg), ao), Add (Mul (aeh, CX (aew, aex)), adi)) = |
|
463 Add (Add (Mul (mc, C acg), ao), Add (Mul (aeh, CX (aew, aex)), adi)) |
|
464 | numadd (Add (Mul (mc, C acg), ao), Add (Mul (aeh, Neg aey), adi)) = |
|
465 Add (Add (Mul (mc, C acg), ao), Add (Mul (aeh, Neg aey), adi)) |
|
466 | numadd (Add (Mul (mc, C acg), ao), Add (Mul (aeh, Add (aez, afa)), adi)) = |
|
467 Add (Add (Mul (mc, C acg), ao), Add (Mul (aeh, Add (aez, afa)), adi)) |
|
468 | numadd (Add (Mul (mc, C acg), ao), Add (Mul (aeh, Sub (afb, afc)), adi)) = |
|
469 Add (Add (Mul (mc, C acg), ao), Add (Mul (aeh, Sub (afb, afc)), adi)) |
|
470 | numadd (Add (Mul (mc, C acg), ao), Add (Mul (aeh, Mul (afd, afe)), adi)) = |
|
471 Add (Add (Mul (mc, C acg), ao), Add (Mul (aeh, Mul (afd, afe)), adi)) |
|
472 | numadd (Add (Mul (mc, C acg), ao), Sub (adj, adk)) = |
|
473 Add (Add (Mul (mc, C acg), ao), Sub (adj, adk)) |
|
474 | numadd (Add (Mul (mc, C acg), ao), Mul (adl, adm)) = |
|
475 Add (Add (Mul (mc, C acg), ao), Mul (adl, adm)) |
|
476 | numadd (Add (Mul (mc, CX (aci, acj)), ao), C ajl) = |
|
477 Add (Add (Mul (mc, CX (aci, acj)), ao), C ajl) |
|
478 | numadd (Add (Mul (mc, CX (aci, acj)), ao), Bound ajm) = |
|
479 Add (Add (Mul (mc, CX (aci, acj)), ao), Bound ajm) |
|
480 | numadd (Add (Mul (mc, CX (aci, acj)), ao), CX (ajn, ajo)) = |
|
481 Add (Add (Mul (mc, CX (aci, acj)), ao), CX (ajn, ajo)) |
|
482 | numadd (Add (Mul (mc, CX (aci, acj)), ao), Neg ajp) = |
|
483 Add (Add (Mul (mc, CX (aci, acj)), ao), Neg ajp) |
|
484 | numadd (Add (Mul (mc, CX (aci, acj)), ao), Add (C akh, ajr)) = |
|
485 Add (Add (Mul (mc, CX (aci, acj)), ao), Add (C akh, ajr)) |
|
486 | numadd (Add (Mul (mc, CX (aci, acj)), ao), Add (Bound aki, ajr)) = |
|
487 Add (Add (Mul (mc, CX (aci, acj)), ao), Add (Bound aki, ajr)) |
|
488 | numadd (Add (Mul (mc, CX (aci, acj)), ao), Add (CX (akj, akk), ajr)) = |
|
489 Add (Add (Mul (mc, CX (aci, acj)), ao), Add (CX (akj, akk), ajr)) |
|
490 | numadd (Add (Mul (mc, CX (aci, acj)), ao), Add (Neg akl, ajr)) = |
|
491 Add (Add (Mul (mc, CX (aci, acj)), ao), Add (Neg akl, ajr)) |
|
492 | numadd (Add (Mul (mc, CX (aci, acj)), ao), Add (Add (akm, akn), ajr)) = |
|
493 Add (Add (Mul (mc, CX (aci, acj)), ao), Add (Add (akm, akn), ajr)) |
|
494 | numadd (Add (Mul (mc, CX (aci, acj)), ao), Add (Sub (ako, akp), ajr)) = |
|
495 Add (Add (Mul (mc, CX (aci, acj)), ao), Add (Sub (ako, akp), ajr)) |
|
496 | numadd (Add (Mul (mc, CX (aci, acj)), ao), Add (Mul (akq, C ald), ajr)) = |
|
497 Add (Add (Mul (mc, CX (aci, acj)), ao), Add (Mul (akq, C ald), ajr)) |
|
498 | numadd |
|
499 (Add (Mul (mc, CX (aci, acj)), ao), Add (Mul (akq, CX (alf, alg)), ajr)) = |
|
500 Add (Add (Mul (mc, CX (aci, acj)), ao), Add (Mul (akq, CX (alf, alg)), ajr)) |
|
501 | numadd (Add (Mul (mc, CX (aci, acj)), ao), Add (Mul (akq, Neg alh), ajr)) = |
|
502 Add (Add (Mul (mc, CX (aci, acj)), ao), Add (Mul (akq, Neg alh), ajr)) |
|
503 | numadd |
|
504 (Add (Mul (mc, CX (aci, acj)), ao), |
|
505 Add (Mul (akq, Add (ali, alj)), ajr)) = |
|
506 Add (Add (Mul (mc, CX (aci, acj)), ao), |
|
507 Add (Mul (akq, Add (ali, alj)), ajr)) |
|
508 | numadd |
|
509 (Add (Mul (mc, CX (aci, acj)), ao), |
|
510 Add (Mul (akq, Sub (alk, all)), ajr)) = |
|
511 Add (Add (Mul (mc, CX (aci, acj)), ao), |
|
512 Add (Mul (akq, Sub (alk, all)), ajr)) |
|
513 | numadd |
|
514 (Add (Mul (mc, CX (aci, acj)), ao), |
|
515 Add (Mul (akq, Mul (alm, aln)), ajr)) = |
|
516 Add (Add (Mul (mc, CX (aci, acj)), ao), |
|
517 Add (Mul (akq, Mul (alm, aln)), ajr)) |
|
518 | numadd (Add (Mul (mc, CX (aci, acj)), ao), Sub (ajs, ajt)) = |
|
519 Add (Add (Mul (mc, CX (aci, acj)), ao), Sub (ajs, ajt)) |
|
520 | numadd (Add (Mul (mc, CX (aci, acj)), ao), Mul (aju, ajv)) = |
|
521 Add (Add (Mul (mc, CX (aci, acj)), ao), Mul (aju, ajv)) |
|
522 | numadd (Add (Mul (mc, Neg ack), ao), C alz) = |
|
523 Add (Add (Mul (mc, Neg ack), ao), C alz) |
|
524 | numadd (Add (Mul (mc, Neg ack), ao), Bound ama) = |
|
525 Add (Add (Mul (mc, Neg ack), ao), Bound ama) |
|
526 | numadd (Add (Mul (mc, Neg ack), ao), CX (amb, amc)) = |
|
527 Add (Add (Mul (mc, Neg ack), ao), CX (amb, amc)) |
|
528 | numadd (Add (Mul (mc, Neg ack), ao), Neg amd) = |
|
529 Add (Add (Mul (mc, Neg ack), ao), Neg amd) |
|
530 | numadd (Add (Mul (mc, Neg ack), ao), Add (C amv, amf)) = |
|
531 Add (Add (Mul (mc, Neg ack), ao), Add (C amv, amf)) |
|
532 | numadd (Add (Mul (mc, Neg ack), ao), Add (Bound amw, amf)) = |
|
533 Add (Add (Mul (mc, Neg ack), ao), Add (Bound amw, amf)) |
|
534 | numadd (Add (Mul (mc, Neg ack), ao), Add (CX (amx, amy), amf)) = |
|
535 Add (Add (Mul (mc, Neg ack), ao), Add (CX (amx, amy), amf)) |
|
536 | numadd (Add (Mul (mc, Neg ack), ao), Add (Neg amz, amf)) = |
|
537 Add (Add (Mul (mc, Neg ack), ao), Add (Neg amz, amf)) |
|
538 | numadd (Add (Mul (mc, Neg ack), ao), Add (Add (ana, anb), amf)) = |
|
539 Add (Add (Mul (mc, Neg ack), ao), Add (Add (ana, anb), amf)) |
|
540 | numadd (Add (Mul (mc, Neg ack), ao), Add (Sub (anc, and'), amf)) = |
|
541 Add (Add (Mul (mc, Neg ack), ao), Add (Sub (anc, and'), amf)) |
|
542 | numadd (Add (Mul (mc, Neg ack), ao), Add (Mul (ane, C anr), amf)) = |
|
543 Add (Add (Mul (mc, Neg ack), ao), Add (Mul (ane, C anr), amf)) |
|
544 | numadd (Add (Mul (mc, Neg ack), ao), Add (Mul (ane, CX (ant, anu)), amf)) = |
|
545 Add (Add (Mul (mc, Neg ack), ao), Add (Mul (ane, CX (ant, anu)), amf)) |
|
546 | numadd (Add (Mul (mc, Neg ack), ao), Add (Mul (ane, Neg anv), amf)) = |
|
547 Add (Add (Mul (mc, Neg ack), ao), Add (Mul (ane, Neg anv), amf)) |
|
548 | numadd (Add (Mul (mc, Neg ack), ao), Add (Mul (ane, Add (anw, anx)), amf)) = |
|
549 Add (Add (Mul (mc, Neg ack), ao), Add (Mul (ane, Add (anw, anx)), amf)) |
|
550 | numadd (Add (Mul (mc, Neg ack), ao), Add (Mul (ane, Sub (any, anz)), amf)) = |
|
551 Add (Add (Mul (mc, Neg ack), ao), Add (Mul (ane, Sub (any, anz)), amf)) |
|
552 | numadd (Add (Mul (mc, Neg ack), ao), Add (Mul (ane, Mul (aoa, aob)), amf)) = |
|
553 Add (Add (Mul (mc, Neg ack), ao), Add (Mul (ane, Mul (aoa, aob)), amf)) |
|
554 | numadd (Add (Mul (mc, Neg ack), ao), Sub (amg, amh)) = |
|
555 Add (Add (Mul (mc, Neg ack), ao), Sub (amg, amh)) |
|
556 | numadd (Add (Mul (mc, Neg ack), ao), Mul (ami, amj)) = |
|
557 Add (Add (Mul (mc, Neg ack), ao), Mul (ami, amj)) |
|
558 | numadd (Add (Mul (mc, Add (acl, acm)), ao), C aon) = |
|
559 Add (Add (Mul (mc, Add (acl, acm)), ao), C aon) |
|
560 | numadd (Add (Mul (mc, Add (acl, acm)), ao), Bound aoo) = |
|
561 Add (Add (Mul (mc, Add (acl, acm)), ao), Bound aoo) |
|
562 | numadd (Add (Mul (mc, Add (acl, acm)), ao), CX (aop, aoq)) = |
|
563 Add (Add (Mul (mc, Add (acl, acm)), ao), CX (aop, aoq)) |
|
564 | numadd (Add (Mul (mc, Add (acl, acm)), ao), Neg aor) = |
|
565 Add (Add (Mul (mc, Add (acl, acm)), ao), Neg aor) |
|
566 | numadd (Add (Mul (mc, Add (acl, acm)), ao), Add (C apj, aot)) = |
|
567 Add (Add (Mul (mc, Add (acl, acm)), ao), Add (C apj, aot)) |
|
568 | numadd (Add (Mul (mc, Add (acl, acm)), ao), Add (Bound apk, aot)) = |
|
569 Add (Add (Mul (mc, Add (acl, acm)), ao), Add (Bound apk, aot)) |
|
570 | numadd (Add (Mul (mc, Add (acl, acm)), ao), Add (CX (apl, apm), aot)) = |
|
571 Add (Add (Mul (mc, Add (acl, acm)), ao), Add (CX (apl, apm), aot)) |
|
572 | numadd (Add (Mul (mc, Add (acl, acm)), ao), Add (Neg apn, aot)) = |
|
573 Add (Add (Mul (mc, Add (acl, acm)), ao), Add (Neg apn, aot)) |
|
574 | numadd (Add (Mul (mc, Add (acl, acm)), ao), Add (Add (apo, app), aot)) = |
|
575 Add (Add (Mul (mc, Add (acl, acm)), ao), Add (Add (apo, app), aot)) |
|
576 | numadd (Add (Mul (mc, Add (acl, acm)), ao), Add (Sub (apq, apr), aot)) = |
|
577 Add (Add (Mul (mc, Add (acl, acm)), ao), Add (Sub (apq, apr), aot)) |
|
578 | numadd (Add (Mul (mc, Add (acl, acm)), ao), Add (Mul (aps, C aqf), aot)) = |
|
579 Add (Add (Mul (mc, Add (acl, acm)), ao), Add (Mul (aps, C aqf), aot)) |
|
580 | numadd |
|
581 (Add (Mul (mc, Add (acl, acm)), ao), |
|
582 Add (Mul (aps, CX (aqh, aqi)), aot)) = |
|
583 Add (Add (Mul (mc, Add (acl, acm)), ao), |
|
584 Add (Mul (aps, CX (aqh, aqi)), aot)) |
|
585 | numadd (Add (Mul (mc, Add (acl, acm)), ao), Add (Mul (aps, Neg aqj), aot)) = |
|
586 Add (Add (Mul (mc, Add (acl, acm)), ao), Add (Mul (aps, Neg aqj), aot)) |
|
587 | numadd |
|
588 (Add (Mul (mc, Add (acl, acm)), ao), |
|
589 Add (Mul (aps, Add (aqk, aql)), aot)) = |
|
590 Add (Add (Mul (mc, Add (acl, acm)), ao), |
|
591 Add (Mul (aps, Add (aqk, aql)), aot)) |
|
592 | numadd |
|
593 (Add (Mul (mc, Add (acl, acm)), ao), |
|
594 Add (Mul (aps, Sub (aqm, aqn)), aot)) = |
|
595 Add (Add (Mul (mc, Add (acl, acm)), ao), |
|
596 Add (Mul (aps, Sub (aqm, aqn)), aot)) |
|
597 | numadd |
|
598 (Add (Mul (mc, Add (acl, acm)), ao), |
|
599 Add (Mul (aps, Mul (aqo, aqp)), aot)) = |
|
600 Add (Add (Mul (mc, Add (acl, acm)), ao), |
|
601 Add (Mul (aps, Mul (aqo, aqp)), aot)) |
|
602 | numadd (Add (Mul (mc, Add (acl, acm)), ao), Sub (aou, aov)) = |
|
603 Add (Add (Mul (mc, Add (acl, acm)), ao), Sub (aou, aov)) |
|
604 | numadd (Add (Mul (mc, Add (acl, acm)), ao), Mul (aow, aox)) = |
|
605 Add (Add (Mul (mc, Add (acl, acm)), ao), Mul (aow, aox)) |
|
606 | numadd (Add (Mul (mc, Sub (acn, aco)), ao), C arb) = |
|
607 Add (Add (Mul (mc, Sub (acn, aco)), ao), C arb) |
|
608 | numadd (Add (Mul (mc, Sub (acn, aco)), ao), Bound arc) = |
|
609 Add (Add (Mul (mc, Sub (acn, aco)), ao), Bound arc) |
|
610 | numadd (Add (Mul (mc, Sub (acn, aco)), ao), CX (ard, are)) = |
|
611 Add (Add (Mul (mc, Sub (acn, aco)), ao), CX (ard, are)) |
|
612 | numadd (Add (Mul (mc, Sub (acn, aco)), ao), Neg arf) = |
|
613 Add (Add (Mul (mc, Sub (acn, aco)), ao), Neg arf) |
|
614 | numadd (Add (Mul (mc, Sub (acn, aco)), ao), Add (C arx, arh)) = |
|
615 Add (Add (Mul (mc, Sub (acn, aco)), ao), Add (C arx, arh)) |
|
616 | numadd (Add (Mul (mc, Sub (acn, aco)), ao), Add (Bound ary, arh)) = |
|
617 Add (Add (Mul (mc, Sub (acn, aco)), ao), Add (Bound ary, arh)) |
|
618 | numadd (Add (Mul (mc, Sub (acn, aco)), ao), Add (CX (arz, asa), arh)) = |
|
619 Add (Add (Mul (mc, Sub (acn, aco)), ao), Add (CX (arz, asa), arh)) |
|
620 | numadd (Add (Mul (mc, Sub (acn, aco)), ao), Add (Neg asb, arh)) = |
|
621 Add (Add (Mul (mc, Sub (acn, aco)), ao), Add (Neg asb, arh)) |
|
622 | numadd (Add (Mul (mc, Sub (acn, aco)), ao), Add (Add (asc, asd), arh)) = |
|
623 Add (Add (Mul (mc, Sub (acn, aco)), ao), Add (Add (asc, asd), arh)) |
|
624 | numadd (Add (Mul (mc, Sub (acn, aco)), ao), Add (Sub (ase, asf), arh)) = |
|
625 Add (Add (Mul (mc, Sub (acn, aco)), ao), Add (Sub (ase, asf), arh)) |
|
626 | numadd (Add (Mul (mc, Sub (acn, aco)), ao), Add (Mul (asg, C ast), arh)) = |
|
627 Add (Add (Mul (mc, Sub (acn, aco)), ao), Add (Mul (asg, C ast), arh)) |
|
628 | numadd |
|
629 (Add (Mul (mc, Sub (acn, aco)), ao), |
|
630 Add (Mul (asg, CX (asv, asw)), arh)) = |
|
631 Add (Add (Mul (mc, Sub (acn, aco)), ao), |
|
632 Add (Mul (asg, CX (asv, asw)), arh)) |
|
633 | numadd (Add (Mul (mc, Sub (acn, aco)), ao), Add (Mul (asg, Neg asx), arh)) = |
|
634 Add (Add (Mul (mc, Sub (acn, aco)), ao), Add (Mul (asg, Neg asx), arh)) |
|
635 | numadd |
|
636 (Add (Mul (mc, Sub (acn, aco)), ao), |
|
637 Add (Mul (asg, Add (asy, asz)), arh)) = |
|
638 Add (Add (Mul (mc, Sub (acn, aco)), ao), |
|
639 Add (Mul (asg, Add (asy, asz)), arh)) |
|
640 | numadd |
|
641 (Add (Mul (mc, Sub (acn, aco)), ao), |
|
642 Add (Mul (asg, Sub (ata, atb)), arh)) = |
|
643 Add (Add (Mul (mc, Sub (acn, aco)), ao), |
|
644 Add (Mul (asg, Sub (ata, atb)), arh)) |
|
645 | numadd |
|
646 (Add (Mul (mc, Sub (acn, aco)), ao), |
|
647 Add (Mul (asg, Mul (atc, atd)), arh)) = |
|
648 Add (Add (Mul (mc, Sub (acn, aco)), ao), |
|
649 Add (Mul (asg, Mul (atc, atd)), arh)) |
|
650 | numadd (Add (Mul (mc, Sub (acn, aco)), ao), Sub (ari, arj)) = |
|
651 Add (Add (Mul (mc, Sub (acn, aco)), ao), Sub (ari, arj)) |
|
652 | numadd (Add (Mul (mc, Sub (acn, aco)), ao), Mul (ark, arl)) = |
|
653 Add (Add (Mul (mc, Sub (acn, aco)), ao), Mul (ark, arl)) |
|
654 | numadd (Add (Mul (mc, Mul (acp, acq)), ao), C atp) = |
|
655 Add (Add (Mul (mc, Mul (acp, acq)), ao), C atp) |
|
656 | numadd (Add (Mul (mc, Mul (acp, acq)), ao), Bound atq) = |
|
657 Add (Add (Mul (mc, Mul (acp, acq)), ao), Bound atq) |
|
658 | numadd (Add (Mul (mc, Mul (acp, acq)), ao), CX (atr, ats)) = |
|
659 Add (Add (Mul (mc, Mul (acp, acq)), ao), CX (atr, ats)) |
|
660 | numadd (Add (Mul (mc, Mul (acp, acq)), ao), Neg att) = |
|
661 Add (Add (Mul (mc, Mul (acp, acq)), ao), Neg att) |
|
662 | numadd (Add (Mul (mc, Mul (acp, acq)), ao), Add (C aul, atv)) = |
|
663 Add (Add (Mul (mc, Mul (acp, acq)), ao), Add (C aul, atv)) |
|
664 | numadd (Add (Mul (mc, Mul (acp, acq)), ao), Add (Bound aum, atv)) = |
|
665 Add (Add (Mul (mc, Mul (acp, acq)), ao), Add (Bound aum, atv)) |
|
666 | numadd (Add (Mul (mc, Mul (acp, acq)), ao), Add (CX (aun, auo), atv)) = |
|
667 Add (Add (Mul (mc, Mul (acp, acq)), ao), Add (CX (aun, auo), atv)) |
|
668 | numadd (Add (Mul (mc, Mul (acp, acq)), ao), Add (Neg aup, atv)) = |
|
669 Add (Add (Mul (mc, Mul (acp, acq)), ao), Add (Neg aup, atv)) |
|
670 | numadd (Add (Mul (mc, Mul (acp, acq)), ao), Add (Add (auq, aur), atv)) = |
|
671 Add (Add (Mul (mc, Mul (acp, acq)), ao), Add (Add (auq, aur), atv)) |
|
672 | numadd (Add (Mul (mc, Mul (acp, acq)), ao), Add (Sub (aus, aut), atv)) = |
|
673 Add (Add (Mul (mc, Mul (acp, acq)), ao), Add (Sub (aus, aut), atv)) |
|
674 | numadd (Add (Mul (mc, Mul (acp, acq)), ao), Add (Mul (auu, C avh), atv)) = |
|
675 Add (Add (Mul (mc, Mul (acp, acq)), ao), Add (Mul (auu, C avh), atv)) |
|
676 | numadd |
|
677 (Add (Mul (mc, Mul (acp, acq)), ao), |
|
678 Add (Mul (auu, CX (avj, avk)), atv)) = |
|
679 Add (Add (Mul (mc, Mul (acp, acq)), ao), |
|
680 Add (Mul (auu, CX (avj, avk)), atv)) |
|
681 | numadd (Add (Mul (mc, Mul (acp, acq)), ao), Add (Mul (auu, Neg avl), atv)) = |
|
682 Add (Add (Mul (mc, Mul (acp, acq)), ao), Add (Mul (auu, Neg avl), atv)) |
|
683 | numadd |
|
684 (Add (Mul (mc, Mul (acp, acq)), ao), |
|
685 Add (Mul (auu, Add (avm, avn)), atv)) = |
|
686 Add (Add (Mul (mc, Mul (acp, acq)), ao), |
|
687 Add (Mul (auu, Add (avm, avn)), atv)) |
|
688 | numadd |
|
689 (Add (Mul (mc, Mul (acp, acq)), ao), |
|
690 Add (Mul (auu, Sub (avo, avp)), atv)) = |
|
691 Add (Add (Mul (mc, Mul (acp, acq)), ao), |
|
692 Add (Mul (auu, Sub (avo, avp)), atv)) |
|
693 | numadd |
|
694 (Add (Mul (mc, Mul (acp, acq)), ao), |
|
695 Add (Mul (auu, Mul (avq, avr)), atv)) = |
|
696 Add (Add (Mul (mc, Mul (acp, acq)), ao), |
|
697 Add (Mul (auu, Mul (avq, avr)), atv)) |
|
698 | numadd (Add (Mul (mc, Mul (acp, acq)), ao), Sub (atw, atx)) = |
|
699 Add (Add (Mul (mc, Mul (acp, acq)), ao), Sub (atw, atx)) |
|
700 | numadd (Add (Mul (mc, Mul (acp, acq)), ao), Mul (aty, atz)) = |
|
701 Add (Add (Mul (mc, Mul (acp, acq)), ao), Mul (aty, atz)) |
|
702 | numadd (Sub (ap, aq), C awd) = Add (Sub (ap, aq), C awd) |
|
703 | numadd (Sub (ap, aq), Bound awe) = Add (Sub (ap, aq), Bound awe) |
|
704 | numadd (Sub (ap, aq), CX (awf, awg)) = Add (Sub (ap, aq), CX (awf, awg)) |
|
705 | numadd (Sub (ap, aq), Neg awh) = Add (Sub (ap, aq), Neg awh) |
|
706 | numadd (Sub (ap, aq), Add (C awz, awj)) = |
|
707 Add (Sub (ap, aq), Add (C awz, awj)) |
|
708 | numadd (Sub (ap, aq), Add (Bound axa, awj)) = |
|
709 Add (Sub (ap, aq), Add (Bound axa, awj)) |
|
710 | numadd (Sub (ap, aq), Add (CX (axb, axc), awj)) = |
|
711 Add (Sub (ap, aq), Add (CX (axb, axc), awj)) |
|
712 | numadd (Sub (ap, aq), Add (Neg axd, awj)) = |
|
713 Add (Sub (ap, aq), Add (Neg axd, awj)) |
|
714 | numadd (Sub (ap, aq), Add (Add (axe, axf), awj)) = |
|
715 Add (Sub (ap, aq), Add (Add (axe, axf), awj)) |
|
716 | numadd (Sub (ap, aq), Add (Sub (axg, axh), awj)) = |
|
717 Add (Sub (ap, aq), Add (Sub (axg, axh), awj)) |
|
718 | numadd (Sub (ap, aq), Add (Mul (axi, C axv), awj)) = |
|
719 Add (Sub (ap, aq), Add (Mul (axi, C axv), awj)) |
|
720 | numadd (Sub (ap, aq), Add (Mul (axi, CX (axx, axy)), awj)) = |
|
721 Add (Sub (ap, aq), Add (Mul (axi, CX (axx, axy)), awj)) |
|
722 | numadd (Sub (ap, aq), Add (Mul (axi, Neg axz), awj)) = |
|
723 Add (Sub (ap, aq), Add (Mul (axi, Neg axz), awj)) |
|
724 | numadd (Sub (ap, aq), Add (Mul (axi, Add (aya, ayb)), awj)) = |
|
725 Add (Sub (ap, aq), Add (Mul (axi, Add (aya, ayb)), awj)) |
|
726 | numadd (Sub (ap, aq), Add (Mul (axi, Sub (ayc, ayd)), awj)) = |
|
727 Add (Sub (ap, aq), Add (Mul (axi, Sub (ayc, ayd)), awj)) |
|
728 | numadd (Sub (ap, aq), Add (Mul (axi, Mul (aye, ayf)), awj)) = |
|
729 Add (Sub (ap, aq), Add (Mul (axi, Mul (aye, ayf)), awj)) |
|
730 | numadd (Sub (ap, aq), Sub (awk, awl)) = Add (Sub (ap, aq), Sub (awk, awl)) |
|
731 | numadd (Sub (ap, aq), Mul (awm, awn)) = Add (Sub (ap, aq), Mul (awm, awn)) |
|
732 | numadd (Mul (ar, as'), C ayr) = Add (Mul (ar, as'), C ayr) |
|
733 | numadd (Mul (ar, as'), Bound ays) = Add (Mul (ar, as'), Bound ays) |
|
734 | numadd (Mul (ar, as'), CX (ayt, ayu)) = Add (Mul (ar, as'), CX (ayt, ayu)) |
|
735 | numadd (Mul (ar, as'), Neg ayv) = Add (Mul (ar, as'), Neg ayv) |
|
736 | numadd (Mul (ar, as'), Add (C azn, ayx)) = |
|
737 Add (Mul (ar, as'), Add (C azn, ayx)) |
|
738 | numadd (Mul (ar, as'), Add (Bound azo, ayx)) = |
|
739 Add (Mul (ar, as'), Add (Bound azo, ayx)) |
|
740 | numadd (Mul (ar, as'), Add (CX (azp, azq), ayx)) = |
|
741 Add (Mul (ar, as'), Add (CX (azp, azq), ayx)) |
|
742 | numadd (Mul (ar, as'), Add (Neg azr, ayx)) = |
|
743 Add (Mul (ar, as'), Add (Neg azr, ayx)) |
|
744 | numadd (Mul (ar, as'), Add (Add (azs, azt), ayx)) = |
|
745 Add (Mul (ar, as'), Add (Add (azs, azt), ayx)) |
|
746 | numadd (Mul (ar, as'), Add (Sub (azu, azv), ayx)) = |
|
747 Add (Mul (ar, as'), Add (Sub (azu, azv), ayx)) |
|
748 | numadd (Mul (ar, as'), Add (Mul (azw, C baj), ayx)) = |
|
749 Add (Mul (ar, as'), Add (Mul (azw, C baj), ayx)) |
|
750 | numadd (Mul (ar, as'), Add (Mul (azw, CX (bal, bam)), ayx)) = |
|
751 Add (Mul (ar, as'), Add (Mul (azw, CX (bal, bam)), ayx)) |
|
752 | numadd (Mul (ar, as'), Add (Mul (azw, Neg ban), ayx)) = |
|
753 Add (Mul (ar, as'), Add (Mul (azw, Neg ban), ayx)) |
|
754 | numadd (Mul (ar, as'), Add (Mul (azw, Add (bao, bap)), ayx)) = |
|
755 Add (Mul (ar, as'), Add (Mul (azw, Add (bao, bap)), ayx)) |
|
756 | numadd (Mul (ar, as'), Add (Mul (azw, Sub (baq, bar)), ayx)) = |
|
757 Add (Mul (ar, as'), Add (Mul (azw, Sub (baq, bar)), ayx)) |
|
758 | numadd (Mul (ar, as'), Add (Mul (azw, Mul (bas, bat)), ayx)) = |
|
759 Add (Mul (ar, as'), Add (Mul (azw, Mul (bas, bat)), ayx)) |
|
760 | numadd (Mul (ar, as'), Sub (ayy, ayz)) = Add (Mul (ar, as'), Sub (ayy, ayz)) |
|
761 | numadd (Mul (ar, as'), Mul (aza, azb)) = |
|
762 Add (Mul (ar, as'), Mul (aza, azb)); |
|
763 |
|
764 fun nummul (C j) = (fn i => C (i * j)) |
|
765 | nummul (Add (a, b)) = (fn i => numadd (nummul a i, nummul b i)) |
|
766 | nummul (Mul (c, t)) = (fn i => nummul t (i * c)) |
|
767 | nummul (Bound v) = (fn i => Mul (i, Bound v)) |
|
768 | nummul (CX (w, x)) = (fn i => Mul (i, CX (w, x))) |
|
769 | nummul (Neg y) = (fn i => Mul (i, Neg y)) |
|
770 | nummul (Sub (ac, ad)) = (fn i => Mul (i, Sub (ac, ad))); |
|
771 |
|
772 fun numneg t = nummul t (~ 1); |
|
773 |
|
774 fun numsub s t = (if (s = t) then C 0 else numadd (s, numneg t)); |
|
775 |
|
776 fun simpnum (C j) = C j |
|
777 | simpnum (Bound n) = Add (Mul (1, Bound n), C 0) |
|
778 | simpnum (Neg t) = numneg (simpnum t) |
|
779 | simpnum (Add (t, s)) = numadd (simpnum t, simpnum s) |
|
780 | simpnum (Sub (t, s)) = numsub (simpnum t) (simpnum s) |
|
781 | simpnum (Mul (i, t)) = (if (i = 0) then C 0 else nummul (simpnum t) i) |
|
782 | simpnum (CX (w, x)) = CX (w, x); |
|
783 |
|
784 datatype fm = T | F | Lt of num | Le of num | Gt of num | Ge of num | Eq of num |
|
785 | NEq of num | Dvd of int * num | NDvd of int * num | NOT of fm |
|
786 | And of fm * fm | Or of fm * fm | Imp of fm * fm | Iff of fm * fm | E of fm |
|
787 | A of fm | Closed of int | NClosed of int; |
|
788 |
|
789 fun not (NOT p) = p |
|
790 | not T = F |
|
791 | not F = T |
|
792 | not (Lt u) = NOT (Lt u) |
|
793 | not (Le v) = NOT (Le v) |
|
794 | not (Gt w) = NOT (Gt w) |
|
795 | not (Ge x) = NOT (Ge x) |
|
796 | not (Eq y) = NOT (Eq y) |
|
797 | not (NEq z) = NOT (NEq z) |
|
798 | not (Dvd (aa, ab)) = NOT (Dvd (aa, ab)) |
|
799 | not (NDvd (ac, ad)) = NOT (NDvd (ac, ad)) |
|
800 | not (And (af, ag)) = NOT (And (af, ag)) |
|
801 | not (Or (ah, ai)) = NOT (Or (ah, ai)) |
|
802 | not (Imp (aj, ak)) = NOT (Imp (aj, ak)) |
|
803 | not (Iff (al, am)) = NOT (Iff (al, am)) |
|
804 | not (E an) = NOT (E an) |
|
805 | not (A ao) = NOT (A ao) |
|
806 | not (Closed ap) = NOT (Closed ap) |
|
807 | not (NClosed aq) = NOT (NClosed aq); |
|
808 |
|
809 fun iff p q = |
|
810 (if (p = q) then T |
|
811 else (if ((p = not q) orelse (not p = q)) then F |
|
812 else (if (p = F) then not q |
|
813 else (if (q = F) then not p |
|
814 else (if (p = T) then q |
|
815 else (if (q = T) then p else Iff (p, q))))))); |
|
816 |
|
817 fun imp p q = |
|
818 (if ((p = F) orelse (q = T)) then T |
|
819 else (if (p = T) then q else (if (q = F) then not p else Imp (p, q)))); |
|
820 |
|
821 fun disj p q = |
|
822 (if ((p = T) orelse (q = T)) then T |
|
823 else (if (p = F) then q else (if (q = F) then p else Or (p, q)))); |
|
824 |
|
825 fun conj p q = |
|
826 (if ((p = F) orelse (q = F)) then F |
|
827 else (if (p = T) then q else (if (q = T) then p else And (p, q)))); |
|
828 |
|
829 fun simpfm (And (p, q)) = conj (simpfm p) (simpfm q) |
|
830 | simpfm (Or (p, q)) = disj (simpfm p) (simpfm q) |
|
831 | simpfm (Imp (p, q)) = imp (simpfm p) (simpfm q) |
|
832 | simpfm (Iff (p, q)) = iff (simpfm p) (simpfm q) |
|
833 | simpfm (NOT p) = not (simpfm p) |
|
834 | simpfm (Lt a) = |
|
835 let val a' = simpnum a |
|
836 in (case a' of C x => (if (x < 0) then T else F) | Bound x => Lt a' |
|
837 | CX (x, xa) => Lt a' | Neg x => Lt a' | Add (x, xa) => Lt a' |
|
838 | Sub (x, xa) => Lt a' | Mul (x, xa) => Lt a') |
|
839 end |
|
840 | simpfm (Le a) = |
|
841 let val a' = simpnum a |
|
842 in (case a' of C x => (if (x <= 0) then T else F) | Bound x => Le a' |
|
843 | CX (x, xa) => Le a' | Neg x => Le a' | Add (x, xa) => Le a' |
|
844 | Sub (x, xa) => Le a' | Mul (x, xa) => Le a') |
|
845 end |
|
846 | simpfm (Gt a) = |
|
847 let val a' = simpnum a |
|
848 in (case a' of C x => (if (0 < x) then T else F) | Bound x => Gt a' |
|
849 | CX (x, xa) => Gt a' | Neg x => Gt a' | Add (x, xa) => Gt a' |
|
850 | Sub (x, xa) => Gt a' | Mul (x, xa) => Gt a') |
|
851 end |
|
852 | simpfm (Ge a) = |
|
853 let val a' = simpnum a |
|
854 in (case a' of C x => (if (0 <= x) then T else F) | Bound x => Ge a' |
|
855 | CX (x, xa) => Ge a' | Neg x => Ge a' | Add (x, xa) => Ge a' |
|
856 | Sub (x, xa) => Ge a' | Mul (x, xa) => Ge a') |
|
857 end |
|
858 | simpfm (Eq a) = |
|
859 let val a' = simpnum a |
|
860 in (case a' of C x => (if (x = 0) then T else F) | Bound x => Eq a' |
|
861 | CX (x, xa) => Eq a' | Neg x => Eq a' | Add (x, xa) => Eq a' |
|
862 | Sub (x, xa) => Eq a' | Mul (x, xa) => Eq a') |
|
863 end |
|
864 | simpfm (NEq a) = |
|
865 let val a' = simpnum a |
|
866 in (case a' of C x => (if Bool.not (x = 0) then T else F) |
|
867 | Bound x => NEq a' | CX (x, xa) => NEq a' | Neg x => NEq a' |
|
868 | Add (x, xa) => NEq a' | Sub (x, xa) => NEq a' |
|
869 | Mul (x, xa) => NEq a') |
|
870 end |
|
871 | simpfm (Dvd (i, a)) = |
|
872 (if (i = 0) then simpfm (Eq a) |
|
873 else (if (abs i = 1) then T |
|
874 else let val a' = simpnum a |
|
875 in (case a' of C x => (if dvd i x then T else F) |
|
876 | Bound x => Dvd (i, a') | CX (x, xa) => Dvd (i, a') |
|
877 | Neg x => Dvd (i, a') | Add (x, xa) => Dvd (i, a') |
|
878 | Sub (x, xa) => Dvd (i, a') |
|
879 | Mul (x, xa) => Dvd (i, a')) |
|
880 end)) |
|
881 | simpfm (NDvd (i, a)) = |
|
882 (if (i = 0) then simpfm (NEq a) |
|
883 else (if (abs i = 1) then F |
|
884 else let val a' = simpnum a |
|
885 in (case a' of C x => (if Bool.not (dvd i x) then T else F) |
|
886 | Bound x => NDvd (i, a') | CX (x, xa) => NDvd (i, a') |
|
887 | Neg x => NDvd (i, a') | Add (x, xa) => NDvd (i, a') |
|
888 | Sub (x, xa) => NDvd (i, a') |
|
889 | Mul (x, xa) => NDvd (i, a')) |
|
890 end)) |
|
891 | simpfm T = T |
|
892 | simpfm F = F |
|
893 | simpfm (E ao) = E ao |
|
894 | simpfm (A ap) = A ap |
|
895 | simpfm (Closed aq) = Closed aq |
|
896 | simpfm (NClosed ar) = NClosed ar; |
|
897 |
|
898 fun foldr f [] a = a |
|
899 | foldr f (x :: xs) a = f x (foldr f xs a); |
|
900 |
|
901 fun djf f p q = |
|
902 (if (q = T) then T |
|
903 else (if (q = F) then f p |
|
904 else let val fp = f p |
|
905 in (case fp of T => T | F => q | Lt x => Or (f p, q) |
|
906 | Le x => Or (f p, q) | Gt x => Or (f p, q) |
|
907 | Ge x => Or (f p, q) | Eq x => Or (f p, q) |
|
908 | NEq x => Or (f p, q) | Dvd (x, xa) => Or (f p, q) |
|
909 | NDvd (x, xa) => Or (f p, q) | NOT x => Or (f p, q) |
|
910 | And (x, xa) => Or (f p, q) | Or (x, xa) => Or (f p, q) |
|
911 | Imp (x, xa) => Or (f p, q) | Iff (x, xa) => Or (f p, q) |
|
912 | E x => Or (f p, q) | A x => Or (f p, q) |
|
913 | Closed x => Or (f p, q) | NClosed x => Or (f p, q)) |
|
914 end)); |
|
915 |
|
916 fun evaldjf f ps = foldr (djf f) ps F; |
|
917 |
|
918 fun append [] ys = ys |
|
919 | append (x :: xs) ys = (x :: append xs ys); |
|
920 |
|
921 fun disjuncts (Or (p, q)) = append (disjuncts p) (disjuncts q) |
|
922 | disjuncts F = [] |
|
923 | disjuncts T = [T] |
|
924 | disjuncts (Lt u) = [Lt u] |
|
925 | disjuncts (Le v) = [Le v] |
|
926 | disjuncts (Gt w) = [Gt w] |
|
927 | disjuncts (Ge x) = [Ge x] |
|
928 | disjuncts (Eq y) = [Eq y] |
|
929 | disjuncts (NEq z) = [NEq z] |
|
930 | disjuncts (Dvd (aa, ab)) = [Dvd (aa, ab)] |
|
931 | disjuncts (NDvd (ac, ad)) = [NDvd (ac, ad)] |
|
932 | disjuncts (NOT ae) = [NOT ae] |
|
933 | disjuncts (And (af, ag)) = [And (af, ag)] |
|
934 | disjuncts (Imp (aj, ak)) = [Imp (aj, ak)] |
|
935 | disjuncts (Iff (al, am)) = [Iff (al, am)] |
|
936 | disjuncts (E an) = [E an] |
|
937 | disjuncts (A ao) = [A ao] |
|
938 | disjuncts (Closed ap) = [Closed ap] |
|
939 | disjuncts (NClosed aq) = [NClosed aq]; |
|
940 |
|
941 fun DJ f p = evaldjf f (disjuncts p); |
|
942 |
|
943 fun qelim (E p) = (fn qe => DJ qe (qelim p qe)) |
|
944 | qelim (A p) = (fn qe => not (qe (qelim (NOT p) qe))) |
|
945 | qelim (NOT p) = (fn qe => not (qelim p qe)) |
|
946 | qelim (And (p, q)) = (fn qe => conj (qelim p qe) (qelim q qe)) |
|
947 | qelim (Or (p, q)) = (fn qe => disj (qelim p qe) (qelim q qe)) |
|
948 | qelim (Imp (p, q)) = (fn qe => imp (qelim p qe) (qelim q qe)) |
|
949 | qelim (Iff (p, q)) = (fn qe => iff (qelim p qe) (qelim q qe)) |
|
950 | qelim T = (fn y => simpfm T) |
|
951 | qelim F = (fn y => simpfm F) |
|
952 | qelim (Lt u) = (fn y => simpfm (Lt u)) |
|
953 | qelim (Le v) = (fn y => simpfm (Le v)) |
|
954 | qelim (Gt w) = (fn y => simpfm (Gt w)) |
|
955 | qelim (Ge x) = (fn y => simpfm (Ge x)) |
|
956 | qelim (Eq y) = (fn ya => simpfm (Eq y)) |
|
957 | qelim (NEq z) = (fn y => simpfm (NEq z)) |
|
958 | qelim (Dvd (aa, ab)) = (fn y => simpfm (Dvd (aa, ab))) |
|
959 | qelim (NDvd (ac, ad)) = (fn y => simpfm (NDvd (ac, ad))) |
|
960 | qelim (Closed ap) = (fn y => simpfm (Closed ap)) |
|
961 | qelim (NClosed aq) = (fn y => simpfm (NClosed aq)); |
|
962 |
|
963 fun minus_def1 m n = nat (minus_def2 (m) (n)); |
|
964 |
|
965 fun decrnum (Bound n) = Bound (minus_def1 n one_def0) |
|
966 | decrnum (Neg a) = Neg (decrnum a) |
|
967 | decrnum (Add (a, b)) = Add (decrnum a, decrnum b) |
|
968 | decrnum (Sub (a, b)) = Sub (decrnum a, decrnum b) |
|
969 | decrnum (Mul (c, a)) = Mul (c, decrnum a) |
|
970 | decrnum (C u) = C u |
|
971 | decrnum (CX (w, x)) = CX (w, x); |
|
972 |
|
973 fun decr (Lt a) = Lt (decrnum a) |
|
974 | decr (Le a) = Le (decrnum a) |
|
975 | decr (Gt a) = Gt (decrnum a) |
|
976 | decr (Ge a) = Ge (decrnum a) |
|
977 | decr (Eq a) = Eq (decrnum a) |
|
978 | decr (NEq a) = NEq (decrnum a) |
|
979 | decr (Dvd (i, a)) = Dvd (i, decrnum a) |
|
980 | decr (NDvd (i, a)) = NDvd (i, decrnum a) |
|
981 | decr (NOT p) = NOT (decr p) |
|
982 | decr (And (p, q)) = And (decr p, decr q) |
|
983 | decr (Or (p, q)) = Or (decr p, decr q) |
|
984 | decr (Imp (p, q)) = Imp (decr p, decr q) |
|
985 | decr (Iff (p, q)) = Iff (decr p, decr q) |
|
986 | decr T = T |
|
987 | decr F = F |
|
988 | decr (E ao) = E ao |
|
989 | decr (A ap) = A ap |
|
990 | decr (Closed aq) = Closed aq |
|
991 | decr (NClosed ar) = NClosed ar; |
|
992 |
|
993 fun map f [] = [] |
|
994 | map f (x :: xs) = (f x :: map f xs); |
|
995 |
|
996 fun allpairs f [] ys = [] |
|
997 | allpairs f (x :: xs) ys = append (map (f x) ys) (allpairs f xs ys); |
|
998 |
|
999 fun numsubst0 t (C c) = C c |
|
1000 | numsubst0 t (Bound n) = (if (n = 0) then t else Bound n) |
|
1001 | numsubst0 t (CX (i, a)) = Add (Mul (i, t), numsubst0 t a) |
|
1002 | numsubst0 t (Neg a) = Neg (numsubst0 t a) |
|
1003 | numsubst0 t (Add (a, b)) = Add (numsubst0 t a, numsubst0 t b) |
|
1004 | numsubst0 t (Sub (a, b)) = Sub (numsubst0 t a, numsubst0 t b) |
|
1005 | numsubst0 t (Mul (i, a)) = Mul (i, numsubst0 t a); |
|
1006 |
|
1007 fun subst0 t T = T |
|
1008 | subst0 t F = F |
|
1009 | subst0 t (Lt a) = Lt (numsubst0 t a) |
|
1010 | subst0 t (Le a) = Le (numsubst0 t a) |
|
1011 | subst0 t (Gt a) = Gt (numsubst0 t a) |
|
1012 | subst0 t (Ge a) = Ge (numsubst0 t a) |
|
1013 | subst0 t (Eq a) = Eq (numsubst0 t a) |
|
1014 | subst0 t (NEq a) = NEq (numsubst0 t a) |
|
1015 | subst0 t (Dvd (i, a)) = Dvd (i, numsubst0 t a) |
|
1016 | subst0 t (NDvd (i, a)) = NDvd (i, numsubst0 t a) |
|
1017 | subst0 t (NOT p) = NOT (subst0 t p) |
|
1018 | subst0 t (And (p, q)) = And (subst0 t p, subst0 t q) |
|
1019 | subst0 t (Or (p, q)) = Or (subst0 t p, subst0 t q) |
|
1020 | subst0 t (Imp (p, q)) = Imp (subst0 t p, subst0 t q) |
|
1021 | subst0 t (Iff (p, q)) = Iff (subst0 t p, subst0 t q) |
|
1022 | subst0 t (Closed P) = Closed P |
|
1023 | subst0 t (NClosed P) = NClosed P; |
|
1024 |
|
1025 fun minusinf (And (p, q)) = And (minusinf p, minusinf q) |
|
1026 | minusinf (Or (p, q)) = Or (minusinf p, minusinf q) |
|
1027 | minusinf (Eq (CX (c, e))) = F |
|
1028 | minusinf (NEq (CX (c, e))) = T |
|
1029 | minusinf (Lt (CX (c, e))) = T |
|
1030 | minusinf (Le (CX (c, e))) = T |
|
1031 | minusinf (Gt (CX (c, e))) = F |
|
1032 | minusinf (Ge (CX (c, e))) = F |
|
1033 | minusinf T = T |
|
1034 | minusinf F = F |
|
1035 | minusinf (Lt (C bo)) = Lt (C bo) |
|
1036 | minusinf (Lt (Bound bp)) = Lt (Bound bp) |
|
1037 | minusinf (Lt (Neg bs)) = Lt (Neg bs) |
|
1038 | minusinf (Lt (Add (bt, bu))) = Lt (Add (bt, bu)) |
|
1039 | minusinf (Lt (Sub (bv, bw))) = Lt (Sub (bv, bw)) |
|
1040 | minusinf (Lt (Mul (bx, by))) = Lt (Mul (bx, by)) |
|
1041 | minusinf (Le (C ck)) = Le (C ck) |
|
1042 | minusinf (Le (Bound cl)) = Le (Bound cl) |
|
1043 | minusinf (Le (Neg co)) = Le (Neg co) |
|
1044 | minusinf (Le (Add (cp, cq))) = Le (Add (cp, cq)) |
|
1045 | minusinf (Le (Sub (cr, cs))) = Le (Sub (cr, cs)) |
|
1046 | minusinf (Le (Mul (ct, cu))) = Le (Mul (ct, cu)) |
|
1047 | minusinf (Gt (C dg)) = Gt (C dg) |
|
1048 | minusinf (Gt (Bound dh)) = Gt (Bound dh) |
|
1049 | minusinf (Gt (Neg dk)) = Gt (Neg dk) |
|
1050 | minusinf (Gt (Add (dl, dm))) = Gt (Add (dl, dm)) |
|
1051 | minusinf (Gt (Sub (dn, do'))) = Gt (Sub (dn, do')) |
|
1052 | minusinf (Gt (Mul (dp, dq))) = Gt (Mul (dp, dq)) |
|
1053 | minusinf (Ge (C ec)) = Ge (C ec) |
|
1054 | minusinf (Ge (Bound ed)) = Ge (Bound ed) |
|
1055 | minusinf (Ge (Neg eg)) = Ge (Neg eg) |
|
1056 | minusinf (Ge (Add (eh, ei))) = Ge (Add (eh, ei)) |
|
1057 | minusinf (Ge (Sub (ej, ek))) = Ge (Sub (ej, ek)) |
|
1058 | minusinf (Ge (Mul (el, em))) = Ge (Mul (el, em)) |
|
1059 | minusinf (Eq (C ey)) = Eq (C ey) |
|
1060 | minusinf (Eq (Bound ez)) = Eq (Bound ez) |
|
1061 | minusinf (Eq (Neg fc)) = Eq (Neg fc) |
|
1062 | minusinf (Eq (Add (fd, fe))) = Eq (Add (fd, fe)) |
|
1063 | minusinf (Eq (Sub (ff, fg))) = Eq (Sub (ff, fg)) |
|
1064 | minusinf (Eq (Mul (fh, fi))) = Eq (Mul (fh, fi)) |
|
1065 | minusinf (NEq (C fu)) = NEq (C fu) |
|
1066 | minusinf (NEq (Bound fv)) = NEq (Bound fv) |
|
1067 | minusinf (NEq (Neg fy)) = NEq (Neg fy) |
|
1068 | minusinf (NEq (Add (fz, ga))) = NEq (Add (fz, ga)) |
|
1069 | minusinf (NEq (Sub (gb, gc))) = NEq (Sub (gb, gc)) |
|
1070 | minusinf (NEq (Mul (gd, ge))) = NEq (Mul (gd, ge)) |
|
1071 | minusinf (Dvd (aa, ab)) = Dvd (aa, ab) |
|
1072 | minusinf (NDvd (ac, ad)) = NDvd (ac, ad) |
|
1073 | minusinf (NOT ae) = NOT ae |
|
1074 | minusinf (Imp (aj, ak)) = Imp (aj, ak) |
|
1075 | minusinf (Iff (al, am)) = Iff (al, am) |
|
1076 | minusinf (E an) = E an |
|
1077 | minusinf (A ao) = A ao |
|
1078 | minusinf (Closed ap) = Closed ap |
|
1079 | minusinf (NClosed aq) = NClosed aq; |
|
1080 |
|
1081 fun iupt (i, j) = (if (j < i) then [] else (i :: iupt ((i + 1), j))); |
|
1082 |
|
1083 fun mirror (And (p, q)) = And (mirror p, mirror q) |
|
1084 | mirror (Or (p, q)) = Or (mirror p, mirror q) |
|
1085 | mirror (Eq (CX (c, e))) = Eq (CX (c, Neg e)) |
|
1086 | mirror (NEq (CX (c, e))) = NEq (CX (c, Neg e)) |
|
1087 | mirror (Lt (CX (c, e))) = Gt (CX (c, Neg e)) |
|
1088 | mirror (Le (CX (c, e))) = Ge (CX (c, Neg e)) |
|
1089 | mirror (Gt (CX (c, e))) = Lt (CX (c, Neg e)) |
|
1090 | mirror (Ge (CX (c, e))) = Le (CX (c, Neg e)) |
|
1091 | mirror (Dvd (i, CX (c, e))) = Dvd (i, CX (c, Neg e)) |
|
1092 | mirror (NDvd (i, CX (c, e))) = NDvd (i, CX (c, Neg e)) |
|
1093 | mirror T = T |
|
1094 | mirror F = F |
|
1095 | mirror (Lt (C bo)) = Lt (C bo) |
|
1096 | mirror (Lt (Bound bp)) = Lt (Bound bp) |
|
1097 | mirror (Lt (Neg bs)) = Lt (Neg bs) |
|
1098 | mirror (Lt (Add (bt, bu))) = Lt (Add (bt, bu)) |
|
1099 | mirror (Lt (Sub (bv, bw))) = Lt (Sub (bv, bw)) |
|
1100 | mirror (Lt (Mul (bx, by))) = Lt (Mul (bx, by)) |
|
1101 | mirror (Le (C ck)) = Le (C ck) |
|
1102 | mirror (Le (Bound cl)) = Le (Bound cl) |
|
1103 | mirror (Le (Neg co)) = Le (Neg co) |
|
1104 | mirror (Le (Add (cp, cq))) = Le (Add (cp, cq)) |
|
1105 | mirror (Le (Sub (cr, cs))) = Le (Sub (cr, cs)) |
|
1106 | mirror (Le (Mul (ct, cu))) = Le (Mul (ct, cu)) |
|
1107 | mirror (Gt (C dg)) = Gt (C dg) |
|
1108 | mirror (Gt (Bound dh)) = Gt (Bound dh) |
|
1109 | mirror (Gt (Neg dk)) = Gt (Neg dk) |
|
1110 | mirror (Gt (Add (dl, dm))) = Gt (Add (dl, dm)) |
|
1111 | mirror (Gt (Sub (dn, do'))) = Gt (Sub (dn, do')) |
|
1112 | mirror (Gt (Mul (dp, dq))) = Gt (Mul (dp, dq)) |
|
1113 | mirror (Ge (C ec)) = Ge (C ec) |
|
1114 | mirror (Ge (Bound ed)) = Ge (Bound ed) |
|
1115 | mirror (Ge (Neg eg)) = Ge (Neg eg) |
|
1116 | mirror (Ge (Add (eh, ei))) = Ge (Add (eh, ei)) |
|
1117 | mirror (Ge (Sub (ej, ek))) = Ge (Sub (ej, ek)) |
|
1118 | mirror (Ge (Mul (el, em))) = Ge (Mul (el, em)) |
|
1119 | mirror (Eq (C ey)) = Eq (C ey) |
|
1120 | mirror (Eq (Bound ez)) = Eq (Bound ez) |
|
1121 | mirror (Eq (Neg fc)) = Eq (Neg fc) |
|
1122 | mirror (Eq (Add (fd, fe))) = Eq (Add (fd, fe)) |
|
1123 | mirror (Eq (Sub (ff, fg))) = Eq (Sub (ff, fg)) |
|
1124 | mirror (Eq (Mul (fh, fi))) = Eq (Mul (fh, fi)) |
|
1125 | mirror (NEq (C fu)) = NEq (C fu) |
|
1126 | mirror (NEq (Bound fv)) = NEq (Bound fv) |
|
1127 | mirror (NEq (Neg fy)) = NEq (Neg fy) |
|
1128 | mirror (NEq (Add (fz, ga))) = NEq (Add (fz, ga)) |
|
1129 | mirror (NEq (Sub (gb, gc))) = NEq (Sub (gb, gc)) |
|
1130 | mirror (NEq (Mul (gd, ge))) = NEq (Mul (gd, ge)) |
|
1131 | mirror (Dvd (aa, C gq)) = Dvd (aa, C gq) |
|
1132 | mirror (Dvd (aa, Bound gr)) = Dvd (aa, Bound gr) |
|
1133 | mirror (Dvd (aa, Neg gu)) = Dvd (aa, Neg gu) |
|
1134 | mirror (Dvd (aa, Add (gv, gw))) = Dvd (aa, Add (gv, gw)) |
|
1135 | mirror (Dvd (aa, Sub (gx, gy))) = Dvd (aa, Sub (gx, gy)) |
|
1136 | mirror (Dvd (aa, Mul (gz, ha))) = Dvd (aa, Mul (gz, ha)) |
|
1137 | mirror (NDvd (ac, C hm)) = NDvd (ac, C hm) |
|
1138 | mirror (NDvd (ac, Bound hn)) = NDvd (ac, Bound hn) |
|
1139 | mirror (NDvd (ac, Neg hq)) = NDvd (ac, Neg hq) |
|
1140 | mirror (NDvd (ac, Add (hr, hs))) = NDvd (ac, Add (hr, hs)) |
|
1141 | mirror (NDvd (ac, Sub (ht, hu))) = NDvd (ac, Sub (ht, hu)) |
|
1142 | mirror (NDvd (ac, Mul (hv, hw))) = NDvd (ac, Mul (hv, hw)) |
|
1143 | mirror (NOT ae) = NOT ae |
|
1144 | mirror (Imp (aj, ak)) = Imp (aj, ak) |
|
1145 | mirror (Iff (al, am)) = Iff (al, am) |
|
1146 | mirror (E an) = E an |
|
1147 | mirror (A ao) = A ao |
|
1148 | mirror (Closed ap) = Closed ap |
|
1149 | mirror (NClosed aq) = NClosed aq; |
|
1150 |
|
1151 fun plus_def0 m n = nat ((m) + (n)); |
|
1152 |
|
1153 fun size_def9 [] = 0 |
|
1154 | size_def9 (a :: list) = plus_def0 (size_def9 list) (0 + 1); |
|
1155 |
|
1156 fun alpha (And (p, q)) = append (alpha p) (alpha q) |
|
1157 | alpha (Or (p, q)) = append (alpha p) (alpha q) |
|
1158 | alpha (Eq (CX (c, e))) = [Add (C ~1, e)] |
|
1159 | alpha (NEq (CX (c, e))) = [e] |
|
1160 | alpha (Lt (CX (c, e))) = [e] |
|
1161 | alpha (Le (CX (c, e))) = [Add (C ~1, e)] |
|
1162 | alpha (Gt (CX (c, e))) = [] |
|
1163 | alpha (Ge (CX (c, e))) = [] |
|
1164 | alpha T = [] |
|
1165 | alpha F = [] |
|
1166 | alpha (Lt (C bo)) = [] |
|
1167 | alpha (Lt (Bound bp)) = [] |
|
1168 | alpha (Lt (Neg bs)) = [] |
|
1169 | alpha (Lt (Add (bt, bu))) = [] |
|
1170 | alpha (Lt (Sub (bv, bw))) = [] |
|
1171 | alpha (Lt (Mul (bx, by))) = [] |
|
1172 | alpha (Le (C ck)) = [] |
|
1173 | alpha (Le (Bound cl)) = [] |
|
1174 | alpha (Le (Neg co)) = [] |
|
1175 | alpha (Le (Add (cp, cq))) = [] |
|
1176 | alpha (Le (Sub (cr, cs))) = [] |
|
1177 | alpha (Le (Mul (ct, cu))) = [] |
|
1178 | alpha (Gt (C dg)) = [] |
|
1179 | alpha (Gt (Bound dh)) = [] |
|
1180 | alpha (Gt (Neg dk)) = [] |
|
1181 | alpha (Gt (Add (dl, dm))) = [] |
|
1182 | alpha (Gt (Sub (dn, do'))) = [] |
|
1183 | alpha (Gt (Mul (dp, dq))) = [] |
|
1184 | alpha (Ge (C ec)) = [] |
|
1185 | alpha (Ge (Bound ed)) = [] |
|
1186 | alpha (Ge (Neg eg)) = [] |
|
1187 | alpha (Ge (Add (eh, ei))) = [] |
|
1188 | alpha (Ge (Sub (ej, ek))) = [] |
|
1189 | alpha (Ge (Mul (el, em))) = [] |
|
1190 | alpha (Eq (C ey)) = [] |
|
1191 | alpha (Eq (Bound ez)) = [] |
|
1192 | alpha (Eq (Neg fc)) = [] |
|
1193 | alpha (Eq (Add (fd, fe))) = [] |
|
1194 | alpha (Eq (Sub (ff, fg))) = [] |
|
1195 | alpha (Eq (Mul (fh, fi))) = [] |
|
1196 | alpha (NEq (C fu)) = [] |
|
1197 | alpha (NEq (Bound fv)) = [] |
|
1198 | alpha (NEq (Neg fy)) = [] |
|
1199 | alpha (NEq (Add (fz, ga))) = [] |
|
1200 | alpha (NEq (Sub (gb, gc))) = [] |
|
1201 | alpha (NEq (Mul (gd, ge))) = [] |
|
1202 | alpha (Dvd (aa, ab)) = [] |
|
1203 | alpha (NDvd (ac, ad)) = [] |
|
1204 | alpha (NOT ae) = [] |
|
1205 | alpha (Imp (aj, ak)) = [] |
|
1206 | alpha (Iff (al, am)) = [] |
|
1207 | alpha (E an) = [] |
|
1208 | alpha (A ao) = [] |
|
1209 | alpha (Closed ap) = [] |
|
1210 | alpha (NClosed aq) = []; |
|
1211 |
|
1212 fun memberl x [] = false |
|
1213 | memberl x (y :: ys) = ((x = y) orelse memberl x ys); |
|
1214 |
|
1215 fun remdups [] = [] |
|
1216 | remdups (x :: xs) = |
|
1217 (if memberl x xs then remdups xs else (x :: remdups xs)); |
|
1218 |
|
1219 fun beta (And (p, q)) = append (beta p) (beta q) |
|
1220 | beta (Or (p, q)) = append (beta p) (beta q) |
|
1221 | beta (Eq (CX (c, e))) = [Sub (C ~1, e)] |
|
1222 | beta (NEq (CX (c, e))) = [Neg e] |
|
1223 | beta (Lt (CX (c, e))) = [] |
|
1224 | beta (Le (CX (c, e))) = [] |
|
1225 | beta (Gt (CX (c, e))) = [Neg e] |
|
1226 | beta (Ge (CX (c, e))) = [Sub (C ~1, e)] |
|
1227 | beta T = [] |
|
1228 | beta F = [] |
|
1229 | beta (Lt (C bo)) = [] |
|
1230 | beta (Lt (Bound bp)) = [] |
|
1231 | beta (Lt (Neg bs)) = [] |
|
1232 | beta (Lt (Add (bt, bu))) = [] |
|
1233 | beta (Lt (Sub (bv, bw))) = [] |
|
1234 | beta (Lt (Mul (bx, by))) = [] |
|
1235 | beta (Le (C ck)) = [] |
|
1236 | beta (Le (Bound cl)) = [] |
|
1237 | beta (Le (Neg co)) = [] |
|
1238 | beta (Le (Add (cp, cq))) = [] |
|
1239 | beta (Le (Sub (cr, cs))) = [] |
|
1240 | beta (Le (Mul (ct, cu))) = [] |
|
1241 | beta (Gt (C dg)) = [] |
|
1242 | beta (Gt (Bound dh)) = [] |
|
1243 | beta (Gt (Neg dk)) = [] |
|
1244 | beta (Gt (Add (dl, dm))) = [] |
|
1245 | beta (Gt (Sub (dn, do'))) = [] |
|
1246 | beta (Gt (Mul (dp, dq))) = [] |
|
1247 | beta (Ge (C ec)) = [] |
|
1248 | beta (Ge (Bound ed)) = [] |
|
1249 | beta (Ge (Neg eg)) = [] |
|
1250 | beta (Ge (Add (eh, ei))) = [] |
|
1251 | beta (Ge (Sub (ej, ek))) = [] |
|
1252 | beta (Ge (Mul (el, em))) = [] |
|
1253 | beta (Eq (C ey)) = [] |
|
1254 | beta (Eq (Bound ez)) = [] |
|
1255 | beta (Eq (Neg fc)) = [] |
|
1256 | beta (Eq (Add (fd, fe))) = [] |
|
1257 | beta (Eq (Sub (ff, fg))) = [] |
|
1258 | beta (Eq (Mul (fh, fi))) = [] |
|
1259 | beta (NEq (C fu)) = [] |
|
1260 | beta (NEq (Bound fv)) = [] |
|
1261 | beta (NEq (Neg fy)) = [] |
|
1262 | beta (NEq (Add (fz, ga))) = [] |
|
1263 | beta (NEq (Sub (gb, gc))) = [] |
|
1264 | beta (NEq (Mul (gd, ge))) = [] |
|
1265 | beta (Dvd (aa, ab)) = [] |
|
1266 | beta (NDvd (ac, ad)) = [] |
|
1267 | beta (NOT ae) = [] |
|
1268 | beta (Imp (aj, ak)) = [] |
|
1269 | beta (Iff (al, am)) = [] |
|
1270 | beta (E an) = [] |
|
1271 | beta (A ao) = [] |
|
1272 | beta (Closed ap) = [] |
|
1273 | beta (NClosed aq) = []; |
|
1274 |
|
1275 fun fst (a, b) = a; |
|
1276 |
|
1277 fun div_def1 a b = fst (divAlg (a, b)); |
|
1278 |
|
1279 fun div_def0 m n = nat (div_def1 (m) (n)); |
|
1280 |
|
1281 fun mod_def0 m n = nat (mod_def1 (m) (n)); |
|
1282 |
|
1283 fun gcd (m, n) = (if (n = 0) then m else gcd (n, mod_def0 m n)); |
|
1284 |
|
1285 fun times_def0 m n = nat ((m) * (n)); |
|
1286 |
|
1287 fun lcm x = (fn (m, n) => div_def0 (times_def0 m n) (gcd (m, n))) x; |
|
1288 |
|
1289 fun ilcm x = (fn j => (lcm (nat (abs x), nat (abs j)))); |
|
1290 |
|
1291 fun delta (And (p, q)) = ilcm (delta p) (delta q) |
|
1292 | delta (Or (p, q)) = ilcm (delta p) (delta q) |
|
1293 | delta (Dvd (i, CX (c, e))) = i |
|
1294 | delta (NDvd (i, CX (c, e))) = i |
|
1295 | delta T = 1 |
|
1296 | delta F = 1 |
|
1297 | delta (Lt u) = 1 |
|
1298 | delta (Le v) = 1 |
|
1299 | delta (Gt w) = 1 |
|
1300 | delta (Ge x) = 1 |
|
1301 | delta (Eq y) = 1 |
|
1302 | delta (NEq z) = 1 |
|
1303 | delta (Dvd (aa, C bo)) = 1 |
|
1304 | delta (Dvd (aa, Bound bp)) = 1 |
|
1305 | delta (Dvd (aa, Neg bs)) = 1 |
|
1306 | delta (Dvd (aa, Add (bt, bu))) = 1 |
|
1307 | delta (Dvd (aa, Sub (bv, bw))) = 1 |
|
1308 | delta (Dvd (aa, Mul (bx, by))) = 1 |
|
1309 | delta (NDvd (ac, C ck)) = 1 |
|
1310 | delta (NDvd (ac, Bound cl)) = 1 |
|
1311 | delta (NDvd (ac, Neg co)) = 1 |
|
1312 | delta (NDvd (ac, Add (cp, cq))) = 1 |
|
1313 | delta (NDvd (ac, Sub (cr, cs))) = 1 |
|
1314 | delta (NDvd (ac, Mul (ct, cu))) = 1 |
|
1315 | delta (NOT ae) = 1 |
|
1316 | delta (Imp (aj, ak)) = 1 |
|
1317 | delta (Iff (al, am)) = 1 |
|
1318 | delta (E an) = 1 |
|
1319 | delta (A ao) = 1 |
|
1320 | delta (Closed ap) = 1 |
|
1321 | delta (NClosed aq) = 1; |
|
1322 |
|
1323 fun a_beta (And (p, q)) = (fn k => And (a_beta p k, a_beta q k)) |
|
1324 | a_beta (Or (p, q)) = (fn k => Or (a_beta p k, a_beta q k)) |
|
1325 | a_beta (Eq (CX (c, e))) = (fn k => Eq (CX (1, Mul (div_def1 k c, e)))) |
|
1326 | a_beta (NEq (CX (c, e))) = (fn k => NEq (CX (1, Mul (div_def1 k c, e)))) |
|
1327 | a_beta (Lt (CX (c, e))) = (fn k => Lt (CX (1, Mul (div_def1 k c, e)))) |
|
1328 | a_beta (Le (CX (c, e))) = (fn k => Le (CX (1, Mul (div_def1 k c, e)))) |
|
1329 | a_beta (Gt (CX (c, e))) = (fn k => Gt (CX (1, Mul (div_def1 k c, e)))) |
|
1330 | a_beta (Ge (CX (c, e))) = (fn k => Ge (CX (1, Mul (div_def1 k c, e)))) |
|
1331 | a_beta (Dvd (i, CX (c, e))) = |
|
1332 (fn k => Dvd ((div_def1 k c * i), CX (1, Mul (div_def1 k c, e)))) |
|
1333 | a_beta (NDvd (i, CX (c, e))) = |
|
1334 (fn k => NDvd ((div_def1 k c * i), CX (1, Mul (div_def1 k c, e)))) |
|
1335 | a_beta T = (fn k => T) |
|
1336 | a_beta F = (fn k => F) |
|
1337 | a_beta (Lt (C bo)) = (fn k => Lt (C bo)) |
|
1338 | a_beta (Lt (Bound bp)) = (fn k => Lt (Bound bp)) |
|
1339 | a_beta (Lt (Neg bs)) = (fn k => Lt (Neg bs)) |
|
1340 | a_beta (Lt (Add (bt, bu))) = (fn k => Lt (Add (bt, bu))) |
|
1341 | a_beta (Lt (Sub (bv, bw))) = (fn k => Lt (Sub (bv, bw))) |
|
1342 | a_beta (Lt (Mul (bx, by))) = (fn k => Lt (Mul (bx, by))) |
|
1343 | a_beta (Le (C ck)) = (fn k => Le (C ck)) |
|
1344 | a_beta (Le (Bound cl)) = (fn k => Le (Bound cl)) |
|
1345 | a_beta (Le (Neg co)) = (fn k => Le (Neg co)) |
|
1346 | a_beta (Le (Add (cp, cq))) = (fn k => Le (Add (cp, cq))) |
|
1347 | a_beta (Le (Sub (cr, cs))) = (fn k => Le (Sub (cr, cs))) |
|
1348 | a_beta (Le (Mul (ct, cu))) = (fn k => Le (Mul (ct, cu))) |
|
1349 | a_beta (Gt (C dg)) = (fn k => Gt (C dg)) |
|
1350 | a_beta (Gt (Bound dh)) = (fn k => Gt (Bound dh)) |
|
1351 | a_beta (Gt (Neg dk)) = (fn k => Gt (Neg dk)) |
|
1352 | a_beta (Gt (Add (dl, dm))) = (fn k => Gt (Add (dl, dm))) |
|
1353 | a_beta (Gt (Sub (dn, do'))) = (fn k => Gt (Sub (dn, do'))) |
|
1354 | a_beta (Gt (Mul (dp, dq))) = (fn k => Gt (Mul (dp, dq))) |
|
1355 | a_beta (Ge (C ec)) = (fn k => Ge (C ec)) |
|
1356 | a_beta (Ge (Bound ed)) = (fn k => Ge (Bound ed)) |
|
1357 | a_beta (Ge (Neg eg)) = (fn k => Ge (Neg eg)) |
|
1358 | a_beta (Ge (Add (eh, ei))) = (fn k => Ge (Add (eh, ei))) |
|
1359 | a_beta (Ge (Sub (ej, ek))) = (fn k => Ge (Sub (ej, ek))) |
|
1360 | a_beta (Ge (Mul (el, em))) = (fn k => Ge (Mul (el, em))) |
|
1361 | a_beta (Eq (C ey)) = (fn k => Eq (C ey)) |
|
1362 | a_beta (Eq (Bound ez)) = (fn k => Eq (Bound ez)) |
|
1363 | a_beta (Eq (Neg fc)) = (fn k => Eq (Neg fc)) |
|
1364 | a_beta (Eq (Add (fd, fe))) = (fn k => Eq (Add (fd, fe))) |
|
1365 | a_beta (Eq (Sub (ff, fg))) = (fn k => Eq (Sub (ff, fg))) |
|
1366 | a_beta (Eq (Mul (fh, fi))) = (fn k => Eq (Mul (fh, fi))) |
|
1367 | a_beta (NEq (C fu)) = (fn k => NEq (C fu)) |
|
1368 | a_beta (NEq (Bound fv)) = (fn k => NEq (Bound fv)) |
|
1369 | a_beta (NEq (Neg fy)) = (fn k => NEq (Neg fy)) |
|
1370 | a_beta (NEq (Add (fz, ga))) = (fn k => NEq (Add (fz, ga))) |
|
1371 | a_beta (NEq (Sub (gb, gc))) = (fn k => NEq (Sub (gb, gc))) |
|
1372 | a_beta (NEq (Mul (gd, ge))) = (fn k => NEq (Mul (gd, ge))) |
|
1373 | a_beta (Dvd (aa, C gq)) = (fn k => Dvd (aa, C gq)) |
|
1374 | a_beta (Dvd (aa, Bound gr)) = (fn k => Dvd (aa, Bound gr)) |
|
1375 | a_beta (Dvd (aa, Neg gu)) = (fn k => Dvd (aa, Neg gu)) |
|
1376 | a_beta (Dvd (aa, Add (gv, gw))) = (fn k => Dvd (aa, Add (gv, gw))) |
|
1377 | a_beta (Dvd (aa, Sub (gx, gy))) = (fn k => Dvd (aa, Sub (gx, gy))) |
|
1378 | a_beta (Dvd (aa, Mul (gz, ha))) = (fn k => Dvd (aa, Mul (gz, ha))) |
|
1379 | a_beta (NDvd (ac, C hm)) = (fn k => NDvd (ac, C hm)) |
|
1380 | a_beta (NDvd (ac, Bound hn)) = (fn k => NDvd (ac, Bound hn)) |
|
1381 | a_beta (NDvd (ac, Neg hq)) = (fn k => NDvd (ac, Neg hq)) |
|
1382 | a_beta (NDvd (ac, Add (hr, hs))) = (fn k => NDvd (ac, Add (hr, hs))) |
|
1383 | a_beta (NDvd (ac, Sub (ht, hu))) = (fn k => NDvd (ac, Sub (ht, hu))) |
|
1384 | a_beta (NDvd (ac, Mul (hv, hw))) = (fn k => NDvd (ac, Mul (hv, hw))) |
|
1385 | a_beta (NOT ae) = (fn k => NOT ae) |
|
1386 | a_beta (Imp (aj, ak)) = (fn k => Imp (aj, ak)) |
|
1387 | a_beta (Iff (al, am)) = (fn k => Iff (al, am)) |
|
1388 | a_beta (E an) = (fn k => E an) |
|
1389 | a_beta (A ao) = (fn k => A ao) |
|
1390 | a_beta (Closed ap) = (fn k => Closed ap) |
|
1391 | a_beta (NClosed aq) = (fn k => NClosed aq); |
|
1392 |
|
1393 fun zeta (And (p, q)) = ilcm (zeta p) (zeta q) |
|
1394 | zeta (Or (p, q)) = ilcm (zeta p) (zeta q) |
|
1395 | zeta (Eq (CX (c, e))) = c |
|
1396 | zeta (NEq (CX (c, e))) = c |
|
1397 | zeta (Lt (CX (c, e))) = c |
|
1398 | zeta (Le (CX (c, e))) = c |
|
1399 | zeta (Gt (CX (c, e))) = c |
|
1400 | zeta (Ge (CX (c, e))) = c |
|
1401 | zeta (Dvd (i, CX (c, e))) = c |
|
1402 | zeta (NDvd (i, CX (c, e))) = c |
|
1403 | zeta T = 1 |
|
1404 | zeta F = 1 |
|
1405 | zeta (Lt (C bo)) = 1 |
|
1406 | zeta (Lt (Bound bp)) = 1 |
|
1407 | zeta (Lt (Neg bs)) = 1 |
|
1408 | zeta (Lt (Add (bt, bu))) = 1 |
|
1409 | zeta (Lt (Sub (bv, bw))) = 1 |
|
1410 | zeta (Lt (Mul (bx, by))) = 1 |
|
1411 | zeta (Le (C ck)) = 1 |
|
1412 | zeta (Le (Bound cl)) = 1 |
|
1413 | zeta (Le (Neg co)) = 1 |
|
1414 | zeta (Le (Add (cp, cq))) = 1 |
|
1415 | zeta (Le (Sub (cr, cs))) = 1 |
|
1416 | zeta (Le (Mul (ct, cu))) = 1 |
|
1417 | zeta (Gt (C dg)) = 1 |
|
1418 | zeta (Gt (Bound dh)) = 1 |
|
1419 | zeta (Gt (Neg dk)) = 1 |
|
1420 | zeta (Gt (Add (dl, dm))) = 1 |
|
1421 | zeta (Gt (Sub (dn, do'))) = 1 |
|
1422 | zeta (Gt (Mul (dp, dq))) = 1 |
|
1423 | zeta (Ge (C ec)) = 1 |
|
1424 | zeta (Ge (Bound ed)) = 1 |
|
1425 | zeta (Ge (Neg eg)) = 1 |
|
1426 | zeta (Ge (Add (eh, ei))) = 1 |
|
1427 | zeta (Ge (Sub (ej, ek))) = 1 |
|
1428 | zeta (Ge (Mul (el, em))) = 1 |
|
1429 | zeta (Eq (C ey)) = 1 |
|
1430 | zeta (Eq (Bound ez)) = 1 |
|
1431 | zeta (Eq (Neg fc)) = 1 |
|
1432 | zeta (Eq (Add (fd, fe))) = 1 |
|
1433 | zeta (Eq (Sub (ff, fg))) = 1 |
|
1434 | zeta (Eq (Mul (fh, fi))) = 1 |
|
1435 | zeta (NEq (C fu)) = 1 |
|
1436 | zeta (NEq (Bound fv)) = 1 |
|
1437 | zeta (NEq (Neg fy)) = 1 |
|
1438 | zeta (NEq (Add (fz, ga))) = 1 |
|
1439 | zeta (NEq (Sub (gb, gc))) = 1 |
|
1440 | zeta (NEq (Mul (gd, ge))) = 1 |
|
1441 | zeta (Dvd (aa, C gq)) = 1 |
|
1442 | zeta (Dvd (aa, Bound gr)) = 1 |
|
1443 | zeta (Dvd (aa, Neg gu)) = 1 |
|
1444 | zeta (Dvd (aa, Add (gv, gw))) = 1 |
|
1445 | zeta (Dvd (aa, Sub (gx, gy))) = 1 |
|
1446 | zeta (Dvd (aa, Mul (gz, ha))) = 1 |
|
1447 | zeta (NDvd (ac, C hm)) = 1 |
|
1448 | zeta (NDvd (ac, Bound hn)) = 1 |
|
1449 | zeta (NDvd (ac, Neg hq)) = 1 |
|
1450 | zeta (NDvd (ac, Add (hr, hs))) = 1 |
|
1451 | zeta (NDvd (ac, Sub (ht, hu))) = 1 |
|
1452 | zeta (NDvd (ac, Mul (hv, hw))) = 1 |
|
1453 | zeta (NOT ae) = 1 |
|
1454 | zeta (Imp (aj, ak)) = 1 |
|
1455 | zeta (Iff (al, am)) = 1 |
|
1456 | zeta (E an) = 1 |
|
1457 | zeta (A ao) = 1 |
|
1458 | zeta (Closed ap) = 1 |
|
1459 | zeta (NClosed aq) = 1; |
|
1460 |
|
1461 fun split x = (fn p => x (fst p) (snd p)); |
|
1462 |
|
1463 fun zsplit0 (C c) = (0, C c) |
|
1464 | zsplit0 (Bound n) = (if (n = 0) then (1, C 0) else (0, Bound n)) |
|
1465 | zsplit0 (CX (i, a)) = split (fn i' => (fn x => ((i + i'), x))) (zsplit0 a) |
|
1466 | zsplit0 (Neg a) = (fn (i', a') => (~ i', Neg a')) (zsplit0 a) |
|
1467 | zsplit0 (Add (a, b)) = |
|
1468 (fn (ia, a') => (fn (ib, b') => ((ia + ib), Add (a', b'))) (zsplit0 b)) |
|
1469 (zsplit0 a) |
|
1470 | zsplit0 (Sub (a, b)) = |
|
1471 (fn (ia, a') => |
|
1472 (fn (ib, b') => (minus_def2 ia ib, Sub (a', b'))) (zsplit0 b)) |
|
1473 (zsplit0 a) |
|
1474 | zsplit0 (Mul (i, a)) = (fn (i', a') => ((i * i'), Mul (i, a'))) (zsplit0 a); |
|
1475 |
|
1476 fun zlfm (And (p, q)) = And (zlfm p, zlfm q) |
|
1477 | zlfm (Or (p, q)) = Or (zlfm p, zlfm q) |
|
1478 | zlfm (Imp (p, q)) = Or (zlfm (NOT p), zlfm q) |
|
1479 | zlfm (Iff (p, q)) = |
|
1480 Or (And (zlfm p, zlfm q), And (zlfm (NOT p), zlfm (NOT q))) |
|
1481 | zlfm (Lt a) = |
|
1482 let val x = zsplit0 a |
|
1483 in (fn (c, r) => |
|
1484 (if (c = 0) then Lt r |
|
1485 else (if (0 < c) then Lt (CX (c, r)) else Gt (CX (~ c, Neg r))))) |
|
1486 x |
|
1487 end |
|
1488 | zlfm (Le a) = |
|
1489 let val x = zsplit0 a |
|
1490 in (fn (c, r) => |
|
1491 (if (c = 0) then Le r |
|
1492 else (if (0 < c) then Le (CX (c, r)) else Ge (CX (~ c, Neg r))))) |
|
1493 x |
|
1494 end |
|
1495 | zlfm (Gt a) = |
|
1496 let val x = zsplit0 a |
|
1497 in (fn (c, r) => |
|
1498 (if (c = 0) then Gt r |
|
1499 else (if (0 < c) then Gt (CX (c, r)) else Lt (CX (~ c, Neg r))))) |
|
1500 x |
|
1501 end |
|
1502 | zlfm (Ge a) = |
|
1503 let val x = zsplit0 a |
|
1504 in (fn (c, r) => |
|
1505 (if (c = 0) then Ge r |
|
1506 else (if (0 < c) then Ge (CX (c, r)) else Le (CX (~ c, Neg r))))) |
|
1507 x |
|
1508 end |
|
1509 | zlfm (Eq a) = |
|
1510 let val x = zsplit0 a |
|
1511 in (fn (c, r) => |
|
1512 (if (c = 0) then Eq r |
|
1513 else (if (0 < c) then Eq (CX (c, r)) else Eq (CX (~ c, Neg r))))) |
|
1514 x |
|
1515 end |
|
1516 | zlfm (NEq a) = |
|
1517 let val x = zsplit0 a |
|
1518 in (fn (c, r) => |
|
1519 (if (c = 0) then NEq r |
|
1520 else (if (0 < c) then NEq (CX (c, r)) else NEq (CX (~ c, Neg r))))) |
|
1521 x |
|
1522 end |
|
1523 | zlfm (Dvd (i, a)) = |
|
1524 (if (i = 0) then zlfm (Eq a) |
|
1525 else let val x = zsplit0 a |
|
1526 in (fn (c, r) => |
|
1527 (if (c = 0) then Dvd (abs i, r) |
|
1528 else (if (0 < c) then Dvd (abs i, CX (c, r)) |
|
1529 else Dvd (abs i, CX (~ c, Neg r))))) |
|
1530 x |
|
1531 end) |
|
1532 | zlfm (NDvd (i, a)) = |
|
1533 (if (i = 0) then zlfm (NEq a) |
|
1534 else let val x = zsplit0 a |
|
1535 in (fn (c, r) => |
|
1536 (if (c = 0) then NDvd (abs i, r) |
|
1537 else (if (0 < c) then NDvd (abs i, CX (c, r)) |
|
1538 else NDvd (abs i, CX (~ c, Neg r))))) |
|
1539 x |
|
1540 end) |
|
1541 | zlfm (NOT (And (p, q))) = Or (zlfm (NOT p), zlfm (NOT q)) |
|
1542 | zlfm (NOT (Or (p, q))) = And (zlfm (NOT p), zlfm (NOT q)) |
|
1543 | zlfm (NOT (Imp (p, q))) = And (zlfm p, zlfm (NOT q)) |
|
1544 | zlfm (NOT (Iff (p, q))) = |
|
1545 Or (And (zlfm p, zlfm (NOT q)), And (zlfm (NOT p), zlfm q)) |
|
1546 | zlfm (NOT (NOT p)) = zlfm p |
|
1547 | zlfm (NOT T) = F |
|
1548 | zlfm (NOT F) = T |
|
1549 | zlfm (NOT (Lt a)) = zlfm (Ge a) |
|
1550 | zlfm (NOT (Le a)) = zlfm (Gt a) |
|
1551 | zlfm (NOT (Gt a)) = zlfm (Le a) |
|
1552 | zlfm (NOT (Ge a)) = zlfm (Lt a) |
|
1553 | zlfm (NOT (Eq a)) = zlfm (NEq a) |
|
1554 | zlfm (NOT (NEq a)) = zlfm (Eq a) |
|
1555 | zlfm (NOT (Dvd (i, a))) = zlfm (NDvd (i, a)) |
|
1556 | zlfm (NOT (NDvd (i, a))) = zlfm (Dvd (i, a)) |
|
1557 | zlfm (NOT (Closed P)) = NClosed P |
|
1558 | zlfm (NOT (NClosed P)) = Closed P |
|
1559 | zlfm T = T |
|
1560 | zlfm F = F |
|
1561 | zlfm (NOT (E ci)) = NOT (E ci) |
|
1562 | zlfm (NOT (A cj)) = NOT (A cj) |
|
1563 | zlfm (E ao) = E ao |
|
1564 | zlfm (A ap) = A ap |
|
1565 | zlfm (Closed aq) = Closed aq |
|
1566 | zlfm (NClosed ar) = NClosed ar; |
|
1567 |
|
1568 fun unit p = |
|
1569 let val p' = zlfm p; val l = zeta p'; |
|
1570 val q = And (Dvd (l, CX (1, C 0)), a_beta p' l); val d = delta q; |
|
1571 val B = remdups (map simpnum (beta q)); |
|
1572 val a = remdups (map simpnum (alpha q)) |
|
1573 in (if less_eq_def3 (size_def9 B) (size_def9 a) then (q, (B, d)) |
|
1574 else (mirror q, (a, d))) |
|
1575 end; |
|
1576 |
|
1577 fun cooper p = |
|
1578 let val (q, (B, d)) = unit p; val js = iupt (1, d); |
|
1579 val mq = simpfm (minusinf q); |
|
1580 val md = evaldjf (fn j => simpfm (subst0 (C j) mq)) js |
|
1581 in (if (md = T) then T |
|
1582 else let val qd = |
|
1583 evaldjf (fn (b, j) => simpfm (subst0 (Add (b, C j)) q)) |
|
1584 (allpairs (fn x => fn xa => (x, xa)) B js) |
|
1585 in decr (disj md qd) end) |
|
1586 end; |
|
1587 |
|
1588 fun prep (E T) = T |
|
1589 | prep (E F) = F |
|
1590 | prep (E (Or (p, q))) = Or (prep (E p), prep (E q)) |
|
1591 | prep (E (Imp (p, q))) = Or (prep (E (NOT p)), prep (E q)) |
|
1592 | prep (E (Iff (p, q))) = |
|
1593 Or (prep (E (And (p, q))), prep (E (And (NOT p, NOT q)))) |
|
1594 | prep (E (NOT (And (p, q)))) = Or (prep (E (NOT p)), prep (E (NOT q))) |
|
1595 | prep (E (NOT (Imp (p, q)))) = prep (E (And (p, NOT q))) |
|
1596 | prep (E (NOT (Iff (p, q)))) = |
|
1597 Or (prep (E (And (p, NOT q))), prep (E (And (NOT p, q)))) |
|
1598 | prep (E (Lt ef)) = E (prep (Lt ef)) |
|
1599 | prep (E (Le eg)) = E (prep (Le eg)) |
|
1600 | prep (E (Gt eh)) = E (prep (Gt eh)) |
|
1601 | prep (E (Ge ei)) = E (prep (Ge ei)) |
|
1602 | prep (E (Eq ej)) = E (prep (Eq ej)) |
|
1603 | prep (E (NEq ek)) = E (prep (NEq ek)) |
|
1604 | prep (E (Dvd (el, em))) = E (prep (Dvd (el, em))) |
|
1605 | prep (E (NDvd (en, eo))) = E (prep (NDvd (en, eo))) |
|
1606 | prep (E (NOT T)) = E (prep (NOT T)) |
|
1607 | prep (E (NOT F)) = E (prep (NOT F)) |
|
1608 | prep (E (NOT (Lt gw))) = E (prep (NOT (Lt gw))) |
|
1609 | prep (E (NOT (Le gx))) = E (prep (NOT (Le gx))) |
|
1610 | prep (E (NOT (Gt gy))) = E (prep (NOT (Gt gy))) |
|
1611 | prep (E (NOT (Ge gz))) = E (prep (NOT (Ge gz))) |
|
1612 | prep (E (NOT (Eq ha))) = E (prep (NOT (Eq ha))) |
|
1613 | prep (E (NOT (NEq hb))) = E (prep (NOT (NEq hb))) |
|
1614 | prep (E (NOT (Dvd (hc, hd)))) = E (prep (NOT (Dvd (hc, hd)))) |
|
1615 | prep (E (NOT (NDvd (he, hf)))) = E (prep (NOT (NDvd (he, hf)))) |
|
1616 | prep (E (NOT (NOT hg))) = E (prep (NOT (NOT hg))) |
|
1617 | prep (E (NOT (Or (hj, hk)))) = E (prep (NOT (Or (hj, hk)))) |
|
1618 | prep (E (NOT (E hp))) = E (prep (NOT (E hp))) |
|
1619 | prep (E (NOT (A hq))) = E (prep (NOT (A hq))) |
|
1620 | prep (E (NOT (Closed hr))) = E (prep (NOT (Closed hr))) |
|
1621 | prep (E (NOT (NClosed hs))) = E (prep (NOT (NClosed hs))) |
|
1622 | prep (E (And (eq, er))) = E (prep (And (eq, er))) |
|
1623 | prep (E (E ey)) = E (prep (E ey)) |
|
1624 | prep (E (A ez)) = E (prep (A ez)) |
|
1625 | prep (E (Closed fa)) = E (prep (Closed fa)) |
|
1626 | prep (E (NClosed fb)) = E (prep (NClosed fb)) |
|
1627 | prep (A (And (p, q))) = And (prep (A p), prep (A q)) |
|
1628 | prep (A T) = prep (NOT (E (NOT T))) |
|
1629 | prep (A F) = prep (NOT (E (NOT F))) |
|
1630 | prep (A (Lt jn)) = prep (NOT (E (NOT (Lt jn)))) |
|
1631 | prep (A (Le jo)) = prep (NOT (E (NOT (Le jo)))) |
|
1632 | prep (A (Gt jp)) = prep (NOT (E (NOT (Gt jp)))) |
|
1633 | prep (A (Ge jq)) = prep (NOT (E (NOT (Ge jq)))) |
|
1634 | prep (A (Eq jr)) = prep (NOT (E (NOT (Eq jr)))) |
|
1635 | prep (A (NEq js)) = prep (NOT (E (NOT (NEq js)))) |
|
1636 | prep (A (Dvd (jt, ju))) = prep (NOT (E (NOT (Dvd (jt, ju))))) |
|
1637 | prep (A (NDvd (jv, jw))) = prep (NOT (E (NOT (NDvd (jv, jw))))) |
|
1638 | prep (A (NOT jx)) = prep (NOT (E (NOT (NOT jx)))) |
|
1639 | prep (A (Or (ka, kb))) = prep (NOT (E (NOT (Or (ka, kb))))) |
|
1640 | prep (A (Imp (kc, kd))) = prep (NOT (E (NOT (Imp (kc, kd))))) |
|
1641 | prep (A (Iff (ke, kf))) = prep (NOT (E (NOT (Iff (ke, kf))))) |
|
1642 | prep (A (E kg)) = prep (NOT (E (NOT (E kg)))) |
|
1643 | prep (A (A kh)) = prep (NOT (E (NOT (A kh)))) |
|
1644 | prep (A (Closed ki)) = prep (NOT (E (NOT (Closed ki)))) |
|
1645 | prep (A (NClosed kj)) = prep (NOT (E (NOT (NClosed kj)))) |
|
1646 | prep (NOT (NOT p)) = prep p |
|
1647 | prep (NOT (And (p, q))) = Or (prep (NOT p), prep (NOT q)) |
|
1648 | prep (NOT (A p)) = prep (E (NOT p)) |
|
1649 | prep (NOT (Or (p, q))) = And (prep (NOT p), prep (NOT q)) |
|
1650 | prep (NOT (Imp (p, q))) = And (prep p, prep (NOT q)) |
|
1651 | prep (NOT (Iff (p, q))) = Or (prep (And (p, NOT q)), prep (And (NOT p, q))) |
|
1652 | prep (NOT T) = NOT (prep T) |
|
1653 | prep (NOT F) = NOT (prep F) |
|
1654 | prep (NOT (Lt bo)) = NOT (prep (Lt bo)) |
|
1655 | prep (NOT (Le bp)) = NOT (prep (Le bp)) |
|
1656 | prep (NOT (Gt bq)) = NOT (prep (Gt bq)) |
|
1657 | prep (NOT (Ge br)) = NOT (prep (Ge br)) |
|
1658 | prep (NOT (Eq bs)) = NOT (prep (Eq bs)) |
|
1659 | prep (NOT (NEq bt)) = NOT (prep (NEq bt)) |
|
1660 | prep (NOT (Dvd (bu, bv))) = NOT (prep (Dvd (bu, bv))) |
|
1661 | prep (NOT (NDvd (bw, bx))) = NOT (prep (NDvd (bw, bx))) |
|
1662 | prep (NOT (E ch)) = NOT (prep (E ch)) |
|
1663 | prep (NOT (Closed cj)) = NOT (prep (Closed cj)) |
|
1664 | prep (NOT (NClosed ck)) = NOT (prep (NClosed ck)) |
|
1665 | prep (Or (p, q)) = Or (prep p, prep q) |
|
1666 | prep (And (p, q)) = And (prep p, prep q) |
|
1667 | prep (Imp (p, q)) = prep (Or (NOT p, q)) |
|
1668 | prep (Iff (p, q)) = Or (prep (And (p, q)), prep (And (NOT p, NOT q))) |
|
1669 | prep T = T |
|
1670 | prep F = F |
|
1671 | prep (Lt u) = Lt u |
|
1672 | prep (Le v) = Le v |
|
1673 | prep (Gt w) = Gt w |
|
1674 | prep (Ge x) = Ge x |
|
1675 | prep (Eq y) = Eq y |
|
1676 | prep (NEq z) = NEq z |
|
1677 | prep (Dvd (aa, ab)) = Dvd (aa, ab) |
|
1678 | prep (NDvd (ac, ad)) = NDvd (ac, ad) |
|
1679 | prep (Closed ap) = Closed ap |
|
1680 | prep (NClosed aq) = NClosed aq; |
|
1681 |
|
1682 fun pa x = qelim (prep x) cooper; |
|
1683 |
|
1684 val pa = (fn x => pa x); |
|
1685 |
|
1686 val test = |
|
1687 (fn x => |
|
1688 pa (E (A (Imp (Ge (Sub (Bound 0, Bound one_def0)), |
|
1689 E (E (Eq (Sub (Add (Mul (3, Bound one_def0), |
|
1690 Mul (5, Bound 0)), |
|
1691 Bound (nat 2)))))))))); |
|
1692 |
|
1693 end; |
|