163 ((nat : IntInf.int) = nat') andalso |
163 ((nat : IntInf.int) = nat') andalso |
164 (((inta : IntInf.int) = int') andalso eq_num num num') |
164 (((inta : IntInf.int) = int') andalso eq_num num num') |
165 | eq_num (Bound nat) (Bound nat') = ((nat : IntInf.int) = nat') |
165 | eq_num (Bound nat) (Bound nat') = ((nat : IntInf.int) = nat') |
166 | eq_num (C inta) (C int') = ((inta : IntInf.int) = int'); |
166 | eq_num (C inta) (C int') = ((inta : IntInf.int) = int'); |
167 |
167 |
168 fun eq_fm (NClosed bd) (Closed ad) = false |
168 fun eq_fm (NClosed b) (Closed a) = false |
169 | eq_fm (NClosed bd) (A af) = false |
169 | eq_fm (NClosed b) (A a) = false |
170 | eq_fm (Closed bd) (A af) = false |
170 | eq_fm (Closed b) (A a) = false |
171 | eq_fm (NClosed bd) (E af) = false |
171 | eq_fm (NClosed b) (E a) = false |
172 | eq_fm (Closed bd) (E af) = false |
172 | eq_fm (Closed b) (E a) = false |
173 | eq_fm (A bf) (E af) = false |
173 | eq_fm (A b) (E a) = false |
174 | eq_fm (NClosed cd) (Iff (af, bf)) = false |
174 | eq_fm (NClosed c) (Iff (a, b)) = false |
175 | eq_fm (Closed cd) (Iff (af, bf)) = false |
175 | eq_fm (Closed c) (Iff (a, b)) = false |
176 | eq_fm (A cf) (Iff (af, bf)) = false |
176 | eq_fm (A c) (Iff (a, b)) = false |
177 | eq_fm (E cf) (Iff (af, bf)) = false |
177 | eq_fm (E c) (Iff (a, b)) = false |
178 | eq_fm (NClosed cd) (Imp (af, bf)) = false |
178 | eq_fm (NClosed c) (Imp (a, b)) = false |
179 | eq_fm (Closed cd) (Imp (af, bf)) = false |
179 | eq_fm (Closed c) (Imp (a, b)) = false |
180 | eq_fm (A cf) (Imp (af, bf)) = false |
180 | eq_fm (A c) (Imp (a, b)) = false |
181 | eq_fm (E cf) (Imp (af, bf)) = false |
181 | eq_fm (E c) (Imp (a, b)) = false |
182 | eq_fm (Iff (cf, db)) (Imp (af, bf)) = false |
182 | eq_fm (Iff (c, d)) (Imp (a, b)) = false |
183 | eq_fm (NClosed cd) (Or (af, bf)) = false |
183 | eq_fm (NClosed c) (Or (a, b)) = false |
184 | eq_fm (Closed cd) (Or (af, bf)) = false |
184 | eq_fm (Closed c) (Or (a, b)) = false |
185 | eq_fm (A cf) (Or (af, bf)) = false |
185 | eq_fm (A c) (Or (a, b)) = false |
186 | eq_fm (E cf) (Or (af, bf)) = false |
186 | eq_fm (E c) (Or (a, b)) = false |
187 | eq_fm (Iff (cf, db)) (Or (af, bf)) = false |
187 | eq_fm (Iff (c, d)) (Or (a, b)) = false |
188 | eq_fm (Imp (cf, db)) (Or (af, bf)) = false |
188 | eq_fm (Imp (c, d)) (Or (a, b)) = false |
189 | eq_fm (NClosed cd) (And (af, bf)) = false |
189 | eq_fm (NClosed c) (And (a, b)) = false |
190 | eq_fm (Closed cd) (And (af, bf)) = false |
190 | eq_fm (Closed c) (And (a, b)) = false |
191 | eq_fm (A cf) (And (af, bf)) = false |
191 | eq_fm (A c) (And (a, b)) = false |
192 | eq_fm (E cf) (And (af, bf)) = false |
192 | eq_fm (E c) (And (a, b)) = false |
193 | eq_fm (Iff (cf, db)) (And (af, bf)) = false |
193 | eq_fm (Iff (c, d)) (And (a, b)) = false |
194 | eq_fm (Imp (cf, db)) (And (af, bf)) = false |
194 | eq_fm (Imp (c, d)) (And (a, b)) = false |
195 | eq_fm (Or (cf, db)) (And (af, bf)) = false |
195 | eq_fm (Or (c, d)) (And (a, b)) = false |
196 | eq_fm (NClosed bd) (Not af) = false |
196 | eq_fm (NClosed b) (Not a) = false |
197 | eq_fm (Closed bd) (Not af) = false |
197 | eq_fm (Closed b) (Not a) = false |
198 | eq_fm (A bf) (Not af) = false |
198 | eq_fm (A b) (Not a) = false |
199 | eq_fm (E bf) (Not af) = false |
199 | eq_fm (E b) (Not a) = false |
200 | eq_fm (Iff (bf, cf)) (Not af) = false |
200 | eq_fm (Iff (b, c)) (Not a) = false |
201 | eq_fm (Imp (bf, cf)) (Not af) = false |
201 | eq_fm (Imp (b, c)) (Not a) = false |
202 | eq_fm (Or (bf, cf)) (Not af) = false |
202 | eq_fm (Or (b, c)) (Not a) = false |
203 | eq_fm (And (bf, cf)) (Not af) = false |
203 | eq_fm (And (b, c)) (Not a) = false |
204 | eq_fm (NClosed cd) (NDvd (ae, bg)) = false |
204 | eq_fm (NClosed c) (NDvd (a, b)) = false |
205 | eq_fm (Closed cd) (NDvd (ae, bg)) = false |
205 | eq_fm (Closed c) (NDvd (a, b)) = false |
206 | eq_fm (A cf) (NDvd (ae, bg)) = false |
206 | eq_fm (A c) (NDvd (a, b)) = false |
207 | eq_fm (E cf) (NDvd (ae, bg)) = false |
207 | eq_fm (E c) (NDvd (a, b)) = false |
208 | eq_fm (Iff (cf, db)) (NDvd (ae, bg)) = false |
208 | eq_fm (Iff (c, d)) (NDvd (a, b)) = false |
209 | eq_fm (Imp (cf, db)) (NDvd (ae, bg)) = false |
209 | eq_fm (Imp (c, d)) (NDvd (a, b)) = false |
210 | eq_fm (Or (cf, db)) (NDvd (ae, bg)) = false |
210 | eq_fm (Or (c, d)) (NDvd (a, b)) = false |
211 | eq_fm (And (cf, db)) (NDvd (ae, bg)) = false |
211 | eq_fm (And (c, d)) (NDvd (a, b)) = false |
212 | eq_fm (Not cf) (NDvd (ae, bg)) = false |
212 | eq_fm (Not c) (NDvd (a, b)) = false |
213 | eq_fm (NClosed cd) (Dvd (ae, bg)) = false |
213 | eq_fm (NClosed c) (Dvd (a, b)) = false |
214 | eq_fm (Closed cd) (Dvd (ae, bg)) = false |
214 | eq_fm (Closed c) (Dvd (a, b)) = false |
215 | eq_fm (A cf) (Dvd (ae, bg)) = false |
215 | eq_fm (A c) (Dvd (a, b)) = false |
216 | eq_fm (E cf) (Dvd (ae, bg)) = false |
216 | eq_fm (E c) (Dvd (a, b)) = false |
217 | eq_fm (Iff (cf, db)) (Dvd (ae, bg)) = false |
217 | eq_fm (Iff (c, d)) (Dvd (a, b)) = false |
218 | eq_fm (Imp (cf, db)) (Dvd (ae, bg)) = false |
218 | eq_fm (Imp (c, d)) (Dvd (a, b)) = false |
219 | eq_fm (Or (cf, db)) (Dvd (ae, bg)) = false |
219 | eq_fm (Or (c, d)) (Dvd (a, b)) = false |
220 | eq_fm (And (cf, db)) (Dvd (ae, bg)) = false |
220 | eq_fm (And (c, d)) (Dvd (a, b)) = false |
221 | eq_fm (Not cf) (Dvd (ae, bg)) = false |
221 | eq_fm (Not c) (Dvd (a, b)) = false |
222 | eq_fm (NDvd (ce, dc)) (Dvd (ae, bg)) = false |
222 | eq_fm (NDvd (c, d)) (Dvd (a, b)) = false |
223 | eq_fm (NClosed bd) (NEq ag) = false |
223 | eq_fm (NClosed b) (NEq a) = false |
224 | eq_fm (Closed bd) (NEq ag) = false |
224 | eq_fm (Closed b) (NEq a) = false |
225 | eq_fm (A bf) (NEq ag) = false |
225 | eq_fm (A b) (NEq a) = false |
226 | eq_fm (E bf) (NEq ag) = false |
226 | eq_fm (E b) (NEq a) = false |
227 | eq_fm (Iff (bf, cf)) (NEq ag) = false |
227 | eq_fm (Iff (b, c)) (NEq a) = false |
228 | eq_fm (Imp (bf, cf)) (NEq ag) = false |
228 | eq_fm (Imp (b, c)) (NEq a) = false |
229 | eq_fm (Or (bf, cf)) (NEq ag) = false |
229 | eq_fm (Or (b, c)) (NEq a) = false |
230 | eq_fm (And (bf, cf)) (NEq ag) = false |
230 | eq_fm (And (b, c)) (NEq a) = false |
231 | eq_fm (Not bf) (NEq ag) = false |
231 | eq_fm (Not b) (NEq a) = false |
232 | eq_fm (NDvd (be, cg)) (NEq ag) = false |
232 | eq_fm (NDvd (b, c)) (NEq a) = false |
233 | eq_fm (Dvd (be, cg)) (NEq ag) = false |
233 | eq_fm (Dvd (b, c)) (NEq a) = false |
234 | eq_fm (NClosed bd) (Eq ag) = false |
234 | eq_fm (NClosed b) (Eq a) = false |
235 | eq_fm (Closed bd) (Eq ag) = false |
235 | eq_fm (Closed b) (Eq a) = false |
236 | eq_fm (A bf) (Eq ag) = false |
236 | eq_fm (A b) (Eq a) = false |
237 | eq_fm (E bf) (Eq ag) = false |
237 | eq_fm (E b) (Eq a) = false |
238 | eq_fm (Iff (bf, cf)) (Eq ag) = false |
238 | eq_fm (Iff (b, c)) (Eq a) = false |
239 | eq_fm (Imp (bf, cf)) (Eq ag) = false |
239 | eq_fm (Imp (b, c)) (Eq a) = false |
240 | eq_fm (Or (bf, cf)) (Eq ag) = false |
240 | eq_fm (Or (b, c)) (Eq a) = false |
241 | eq_fm (And (bf, cf)) (Eq ag) = false |
241 | eq_fm (And (b, c)) (Eq a) = false |
242 | eq_fm (Not bf) (Eq ag) = false |
242 | eq_fm (Not b) (Eq a) = false |
243 | eq_fm (NDvd (be, cg)) (Eq ag) = false |
243 | eq_fm (NDvd (b, c)) (Eq a) = false |
244 | eq_fm (Dvd (be, cg)) (Eq ag) = false |
244 | eq_fm (Dvd (b, c)) (Eq a) = false |
245 | eq_fm (NEq bg) (Eq ag) = false |
245 | eq_fm (NEq b) (Eq a) = false |
246 | eq_fm (NClosed bd) (Ge ag) = false |
246 | eq_fm (NClosed b) (Ge a) = false |
247 | eq_fm (Closed bd) (Ge ag) = false |
247 | eq_fm (Closed b) (Ge a) = false |
248 | eq_fm (A bf) (Ge ag) = false |
248 | eq_fm (A b) (Ge a) = false |
249 | eq_fm (E bf) (Ge ag) = false |
249 | eq_fm (E b) (Ge a) = false |
250 | eq_fm (Iff (bf, cf)) (Ge ag) = false |
250 | eq_fm (Iff (b, c)) (Ge a) = false |
251 | eq_fm (Imp (bf, cf)) (Ge ag) = false |
251 | eq_fm (Imp (b, c)) (Ge a) = false |
252 | eq_fm (Or (bf, cf)) (Ge ag) = false |
252 | eq_fm (Or (b, c)) (Ge a) = false |
253 | eq_fm (And (bf, cf)) (Ge ag) = false |
253 | eq_fm (And (b, c)) (Ge a) = false |
254 | eq_fm (Not bf) (Ge ag) = false |
254 | eq_fm (Not b) (Ge a) = false |
255 | eq_fm (NDvd (be, cg)) (Ge ag) = false |
255 | eq_fm (NDvd (b, c)) (Ge a) = false |
256 | eq_fm (Dvd (be, cg)) (Ge ag) = false |
256 | eq_fm (Dvd (b, c)) (Ge a) = false |
257 | eq_fm (NEq bg) (Ge ag) = false |
257 | eq_fm (NEq b) (Ge a) = false |
258 | eq_fm (Eq bg) (Ge ag) = false |
258 | eq_fm (Eq b) (Ge a) = false |
259 | eq_fm (NClosed bd) (Gt ag) = false |
259 | eq_fm (NClosed b) (Gt a) = false |
260 | eq_fm (Closed bd) (Gt ag) = false |
260 | eq_fm (Closed b) (Gt a) = false |
261 | eq_fm (A bf) (Gt ag) = false |
261 | eq_fm (A b) (Gt a) = false |
262 | eq_fm (E bf) (Gt ag) = false |
262 | eq_fm (E b) (Gt a) = false |
263 | eq_fm (Iff (bf, cf)) (Gt ag) = false |
263 | eq_fm (Iff (b, c)) (Gt a) = false |
264 | eq_fm (Imp (bf, cf)) (Gt ag) = false |
264 | eq_fm (Imp (b, c)) (Gt a) = false |
265 | eq_fm (Or (bf, cf)) (Gt ag) = false |
265 | eq_fm (Or (b, c)) (Gt a) = false |
266 | eq_fm (And (bf, cf)) (Gt ag) = false |
266 | eq_fm (And (b, c)) (Gt a) = false |
267 | eq_fm (Not bf) (Gt ag) = false |
267 | eq_fm (Not b) (Gt a) = false |
268 | eq_fm (NDvd (be, cg)) (Gt ag) = false |
268 | eq_fm (NDvd (b, c)) (Gt a) = false |
269 | eq_fm (Dvd (be, cg)) (Gt ag) = false |
269 | eq_fm (Dvd (b, c)) (Gt a) = false |
270 | eq_fm (NEq bg) (Gt ag) = false |
270 | eq_fm (NEq b) (Gt a) = false |
271 | eq_fm (Eq bg) (Gt ag) = false |
271 | eq_fm (Eq b) (Gt a) = false |
272 | eq_fm (Ge bg) (Gt ag) = false |
272 | eq_fm (Ge b) (Gt a) = false |
273 | eq_fm (NClosed bd) (Le ag) = false |
273 | eq_fm (NClosed b) (Le a) = false |
274 | eq_fm (Closed bd) (Le ag) = false |
274 | eq_fm (Closed b) (Le a) = false |
275 | eq_fm (A bf) (Le ag) = false |
275 | eq_fm (A b) (Le a) = false |
276 | eq_fm (E bf) (Le ag) = false |
276 | eq_fm (E b) (Le a) = false |
277 | eq_fm (Iff (bf, cf)) (Le ag) = false |
277 | eq_fm (Iff (b, c)) (Le a) = false |
278 | eq_fm (Imp (bf, cf)) (Le ag) = false |
278 | eq_fm (Imp (b, c)) (Le a) = false |
279 | eq_fm (Or (bf, cf)) (Le ag) = false |
279 | eq_fm (Or (b, c)) (Le a) = false |
280 | eq_fm (And (bf, cf)) (Le ag) = false |
280 | eq_fm (And (b, c)) (Le a) = false |
281 | eq_fm (Not bf) (Le ag) = false |
281 | eq_fm (Not b) (Le a) = false |
282 | eq_fm (NDvd (be, cg)) (Le ag) = false |
282 | eq_fm (NDvd (b, c)) (Le a) = false |
283 | eq_fm (Dvd (be, cg)) (Le ag) = false |
283 | eq_fm (Dvd (b, c)) (Le a) = false |
284 | eq_fm (NEq bg) (Le ag) = false |
284 | eq_fm (NEq b) (Le a) = false |
285 | eq_fm (Eq bg) (Le ag) = false |
285 | eq_fm (Eq b) (Le a) = false |
286 | eq_fm (Ge bg) (Le ag) = false |
286 | eq_fm (Ge b) (Le a) = false |
287 | eq_fm (Gt bg) (Le ag) = false |
287 | eq_fm (Gt b) (Le a) = false |
288 | eq_fm (NClosed bd) (Lt ag) = false |
288 | eq_fm (NClosed b) (Lt a) = false |
289 | eq_fm (Closed bd) (Lt ag) = false |
289 | eq_fm (Closed b) (Lt a) = false |
290 | eq_fm (A bf) (Lt ag) = false |
290 | eq_fm (A b) (Lt a) = false |
291 | eq_fm (E bf) (Lt ag) = false |
291 | eq_fm (E b) (Lt a) = false |
292 | eq_fm (Iff (bf, cf)) (Lt ag) = false |
292 | eq_fm (Iff (b, c)) (Lt a) = false |
293 | eq_fm (Imp (bf, cf)) (Lt ag) = false |
293 | eq_fm (Imp (b, c)) (Lt a) = false |
294 | eq_fm (Or (bf, cf)) (Lt ag) = false |
294 | eq_fm (Or (b, c)) (Lt a) = false |
295 | eq_fm (And (bf, cf)) (Lt ag) = false |
295 | eq_fm (And (b, c)) (Lt a) = false |
296 | eq_fm (Not bf) (Lt ag) = false |
296 | eq_fm (Not b) (Lt a) = false |
297 | eq_fm (NDvd (be, cg)) (Lt ag) = false |
297 | eq_fm (NDvd (b, c)) (Lt a) = false |
298 | eq_fm (Dvd (be, cg)) (Lt ag) = false |
298 | eq_fm (Dvd (b, c)) (Lt a) = false |
299 | eq_fm (NEq bg) (Lt ag) = false |
299 | eq_fm (NEq b) (Lt a) = false |
300 | eq_fm (Eq bg) (Lt ag) = false |
300 | eq_fm (Eq b) (Lt a) = false |
301 | eq_fm (Ge bg) (Lt ag) = false |
301 | eq_fm (Ge b) (Lt a) = false |
302 | eq_fm (Gt bg) (Lt ag) = false |
302 | eq_fm (Gt b) (Lt a) = false |
303 | eq_fm (Le bg) (Lt ag) = false |
303 | eq_fm (Le b) (Lt a) = false |
304 | eq_fm (NClosed ad) F = false |
304 | eq_fm (NClosed a) F = false |
305 | eq_fm (Closed ad) F = false |
305 | eq_fm (Closed a) F = false |
306 | eq_fm (A af) F = false |
306 | eq_fm (A a) F = false |
307 | eq_fm (E af) F = false |
307 | eq_fm (E a) F = false |
308 | eq_fm (Iff (af, bf)) F = false |
308 | eq_fm (Iff (a, b)) F = false |
309 | eq_fm (Imp (af, bf)) F = false |
309 | eq_fm (Imp (a, b)) F = false |
310 | eq_fm (Or (af, bf)) F = false |
310 | eq_fm (Or (a, b)) F = false |
311 | eq_fm (And (af, bf)) F = false |
311 | eq_fm (And (a, b)) F = false |
312 | eq_fm (Not af) F = false |
312 | eq_fm (Not a) F = false |
313 | eq_fm (NDvd (ae, bg)) F = false |
313 | eq_fm (NDvd (a, b)) F = false |
314 | eq_fm (Dvd (ae, bg)) F = false |
314 | eq_fm (Dvd (a, b)) F = false |
315 | eq_fm (NEq ag) F = false |
315 | eq_fm (NEq a) F = false |
316 | eq_fm (Eq ag) F = false |
316 | eq_fm (Eq a) F = false |
317 | eq_fm (Ge ag) F = false |
317 | eq_fm (Ge a) F = false |
318 | eq_fm (Gt ag) F = false |
318 | eq_fm (Gt a) F = false |
319 | eq_fm (Le ag) F = false |
319 | eq_fm (Le a) F = false |
320 | eq_fm (Lt ag) F = false |
320 | eq_fm (Lt a) F = false |
321 | eq_fm (NClosed ad) T = false |
321 | eq_fm (NClosed a) T = false |
322 | eq_fm (Closed ad) T = false |
322 | eq_fm (Closed a) T = false |
323 | eq_fm (A af) T = false |
323 | eq_fm (A a) T = false |
324 | eq_fm (E af) T = false |
324 | eq_fm (E a) T = false |
325 | eq_fm (Iff (af, bf)) T = false |
325 | eq_fm (Iff (a, b)) T = false |
326 | eq_fm (Imp (af, bf)) T = false |
326 | eq_fm (Imp (a, b)) T = false |
327 | eq_fm (Or (af, bf)) T = false |
327 | eq_fm (Or (a, b)) T = false |
328 | eq_fm (And (af, bf)) T = false |
328 | eq_fm (And (a, b)) T = false |
329 | eq_fm (Not af) T = false |
329 | eq_fm (Not a) T = false |
330 | eq_fm (NDvd (ae, bg)) T = false |
330 | eq_fm (NDvd (a, b)) T = false |
331 | eq_fm (Dvd (ae, bg)) T = false |
331 | eq_fm (Dvd (a, b)) T = false |
332 | eq_fm (NEq ag) T = false |
332 | eq_fm (NEq a) T = false |
333 | eq_fm (Eq ag) T = false |
333 | eq_fm (Eq a) T = false |
334 | eq_fm (Ge ag) T = false |
334 | eq_fm (Ge a) T = false |
335 | eq_fm (Gt ag) T = false |
335 | eq_fm (Gt a) T = false |
336 | eq_fm (Le ag) T = false |
336 | eq_fm (Le a) T = false |
337 | eq_fm (Lt ag) T = false |
337 | eq_fm (Lt a) T = false |
338 | eq_fm F T = false |
338 | eq_fm F T = false |
339 | eq_fm (Closed a) (NClosed b) = false |
339 | eq_fm (Closed a) (NClosed b) = false |
340 | eq_fm (A ab) (NClosed b) = false |
340 | eq_fm (A a) (NClosed b) = false |
341 | eq_fm (A ab) (Closed b) = false |
341 | eq_fm (A a) (Closed b) = false |
342 | eq_fm (E ab) (NClosed b) = false |
342 | eq_fm (E a) (NClosed b) = false |
343 | eq_fm (E ab) (Closed b) = false |
343 | eq_fm (E a) (Closed b) = false |
344 | eq_fm (E ab) (A bb) = false |
344 | eq_fm (E a) (A b) = false |
345 | eq_fm (Iff (ab, bb)) (NClosed c) = false |
345 | eq_fm (Iff (a, b)) (NClosed c) = false |
346 | eq_fm (Iff (ab, bb)) (Closed c) = false |
346 | eq_fm (Iff (a, b)) (Closed c) = false |
347 | eq_fm (Iff (ab, bb)) (A cb) = false |
347 | eq_fm (Iff (a, b)) (A c) = false |
348 | eq_fm (Iff (ab, bb)) (E cb) = false |
348 | eq_fm (Iff (a, b)) (E c) = false |
349 | eq_fm (Imp (ab, bb)) (NClosed c) = false |
349 | eq_fm (Imp (a, b)) (NClosed c) = false |
350 | eq_fm (Imp (ab, bb)) (Closed c) = false |
350 | eq_fm (Imp (a, b)) (Closed c) = false |
351 | eq_fm (Imp (ab, bb)) (A cb) = false |
351 | eq_fm (Imp (a, b)) (A c) = false |
352 | eq_fm (Imp (ab, bb)) (E cb) = false |
352 | eq_fm (Imp (a, b)) (E c) = false |
353 | eq_fm (Imp (ab, bb)) (Iff (cb, d)) = false |
353 | eq_fm (Imp (a, b)) (Iff (c, d)) = false |
354 | eq_fm (Or (ab, bb)) (NClosed c) = false |
354 | eq_fm (Or (a, b)) (NClosed c) = false |
355 | eq_fm (Or (ab, bb)) (Closed c) = false |
355 | eq_fm (Or (a, b)) (Closed c) = false |
356 | eq_fm (Or (ab, bb)) (A cb) = false |
356 | eq_fm (Or (a, b)) (A c) = false |
357 | eq_fm (Or (ab, bb)) (E cb) = false |
357 | eq_fm (Or (a, b)) (E c) = false |
358 | eq_fm (Or (ab, bb)) (Iff (cb, d)) = false |
358 | eq_fm (Or (a, b)) (Iff (c, d)) = false |
359 | eq_fm (Or (ab, bb)) (Imp (cb, d)) = false |
359 | eq_fm (Or (a, b)) (Imp (c, d)) = false |
360 | eq_fm (And (ab, bb)) (NClosed c) = false |
360 | eq_fm (And (a, b)) (NClosed c) = false |
361 | eq_fm (And (ab, bb)) (Closed c) = false |
361 | eq_fm (And (a, b)) (Closed c) = false |
362 | eq_fm (And (ab, bb)) (A cb) = false |
362 | eq_fm (And (a, b)) (A c) = false |
363 | eq_fm (And (ab, bb)) (E cb) = false |
363 | eq_fm (And (a, b)) (E c) = false |
364 | eq_fm (And (ab, bb)) (Iff (cb, d)) = false |
364 | eq_fm (And (a, b)) (Iff (c, d)) = false |
365 | eq_fm (And (ab, bb)) (Imp (cb, d)) = false |
365 | eq_fm (And (a, b)) (Imp (c, d)) = false |
366 | eq_fm (And (ab, bb)) (Or (cb, d)) = false |
366 | eq_fm (And (a, b)) (Or (c, d)) = false |
367 | eq_fm (Not ab) (NClosed b) = false |
367 | eq_fm (Not a) (NClosed b) = false |
368 | eq_fm (Not ab) (Closed b) = false |
368 | eq_fm (Not a) (Closed b) = false |
369 | eq_fm (Not ab) (A bb) = false |
369 | eq_fm (Not a) (A b) = false |
370 | eq_fm (Not ab) (E bb) = false |
370 | eq_fm (Not a) (E b) = false |
371 | eq_fm (Not ab) (Iff (bb, cb)) = false |
371 | eq_fm (Not a) (Iff (b, c)) = false |
372 | eq_fm (Not ab) (Imp (bb, cb)) = false |
372 | eq_fm (Not a) (Imp (b, c)) = false |
373 | eq_fm (Not ab) (Or (bb, cb)) = false |
373 | eq_fm (Not a) (Or (b, c)) = false |
374 | eq_fm (Not ab) (And (bb, cb)) = false |
374 | eq_fm (Not a) (And (b, c)) = false |
375 | eq_fm (NDvd (aa, bc)) (NClosed c) = false |
375 | eq_fm (NDvd (a, b)) (NClosed c) = false |
376 | eq_fm (NDvd (aa, bc)) (Closed c) = false |
376 | eq_fm (NDvd (a, b)) (Closed c) = false |
377 | eq_fm (NDvd (aa, bc)) (A cb) = false |
377 | eq_fm (NDvd (a, b)) (A c) = false |
378 | eq_fm (NDvd (aa, bc)) (E cb) = false |
378 | eq_fm (NDvd (a, b)) (E c) = false |
379 | eq_fm (NDvd (aa, bc)) (Iff (cb, d)) = false |
379 | eq_fm (NDvd (a, b)) (Iff (c, d)) = false |
380 | eq_fm (NDvd (aa, bc)) (Imp (cb, d)) = false |
380 | eq_fm (NDvd (a, b)) (Imp (c, d)) = false |
381 | eq_fm (NDvd (aa, bc)) (Or (cb, d)) = false |
381 | eq_fm (NDvd (a, b)) (Or (c, d)) = false |
382 | eq_fm (NDvd (aa, bc)) (And (cb, d)) = false |
382 | eq_fm (NDvd (a, b)) (And (c, d)) = false |
383 | eq_fm (NDvd (aa, bc)) (Not cb) = false |
383 | eq_fm (NDvd (a, b)) (Not c) = false |
384 | eq_fm (Dvd (aa, bc)) (NClosed c) = false |
384 | eq_fm (Dvd (a, b)) (NClosed c) = false |
385 | eq_fm (Dvd (aa, bc)) (Closed c) = false |
385 | eq_fm (Dvd (a, b)) (Closed c) = false |
386 | eq_fm (Dvd (aa, bc)) (A cb) = false |
386 | eq_fm (Dvd (a, b)) (A c) = false |
387 | eq_fm (Dvd (aa, bc)) (E cb) = false |
387 | eq_fm (Dvd (a, b)) (E c) = false |
388 | eq_fm (Dvd (aa, bc)) (Iff (cb, d)) = false |
388 | eq_fm (Dvd (a, b)) (Iff (c, d)) = false |
389 | eq_fm (Dvd (aa, bc)) (Imp (cb, d)) = false |
389 | eq_fm (Dvd (a, b)) (Imp (c, d)) = false |
390 | eq_fm (Dvd (aa, bc)) (Or (cb, d)) = false |
390 | eq_fm (Dvd (a, b)) (Or (c, d)) = false |
391 | eq_fm (Dvd (aa, bc)) (And (cb, d)) = false |
391 | eq_fm (Dvd (a, b)) (And (c, d)) = false |
392 | eq_fm (Dvd (aa, bc)) (Not cb) = false |
392 | eq_fm (Dvd (a, b)) (Not c) = false |
393 | eq_fm (Dvd (aa, bc)) (NDvd (ca, da)) = false |
393 | eq_fm (Dvd (a, b)) (NDvd (c, d)) = false |
394 | eq_fm (NEq ac) (NClosed b) = false |
394 | eq_fm (NEq a) (NClosed b) = false |
395 | eq_fm (NEq ac) (Closed b) = false |
395 | eq_fm (NEq a) (Closed b) = false |
396 | eq_fm (NEq ac) (A bb) = false |
396 | eq_fm (NEq a) (A b) = false |
397 | eq_fm (NEq ac) (E bb) = false |
397 | eq_fm (NEq a) (E b) = false |
398 | eq_fm (NEq ac) (Iff (bb, cb)) = false |
398 | eq_fm (NEq a) (Iff (b, c)) = false |
399 | eq_fm (NEq ac) (Imp (bb, cb)) = false |
399 | eq_fm (NEq a) (Imp (b, c)) = false |
400 | eq_fm (NEq ac) (Or (bb, cb)) = false |
400 | eq_fm (NEq a) (Or (b, c)) = false |
401 | eq_fm (NEq ac) (And (bb, cb)) = false |
401 | eq_fm (NEq a) (And (b, c)) = false |
402 | eq_fm (NEq ac) (Not bb) = false |
402 | eq_fm (NEq a) (Not b) = false |
403 | eq_fm (NEq ac) (NDvd (ba, cc)) = false |
403 | eq_fm (NEq a) (NDvd (b, c)) = false |
404 | eq_fm (NEq ac) (Dvd (ba, cc)) = false |
404 | eq_fm (NEq a) (Dvd (b, c)) = false |
405 | eq_fm (Eq ac) (NClosed b) = false |
405 | eq_fm (Eq a) (NClosed b) = false |
406 | eq_fm (Eq ac) (Closed b) = false |
406 | eq_fm (Eq a) (Closed b) = false |
407 | eq_fm (Eq ac) (A bb) = false |
407 | eq_fm (Eq a) (A b) = false |
408 | eq_fm (Eq ac) (E bb) = false |
408 | eq_fm (Eq a) (E b) = false |
409 | eq_fm (Eq ac) (Iff (bb, cb)) = false |
409 | eq_fm (Eq a) (Iff (b, c)) = false |
410 | eq_fm (Eq ac) (Imp (bb, cb)) = false |
410 | eq_fm (Eq a) (Imp (b, c)) = false |
411 | eq_fm (Eq ac) (Or (bb, cb)) = false |
411 | eq_fm (Eq a) (Or (b, c)) = false |
412 | eq_fm (Eq ac) (And (bb, cb)) = false |
412 | eq_fm (Eq a) (And (b, c)) = false |
413 | eq_fm (Eq ac) (Not bb) = false |
413 | eq_fm (Eq a) (Not b) = false |
414 | eq_fm (Eq ac) (NDvd (ba, cc)) = false |
414 | eq_fm (Eq a) (NDvd (b, c)) = false |
415 | eq_fm (Eq ac) (Dvd (ba, cc)) = false |
415 | eq_fm (Eq a) (Dvd (b, c)) = false |
416 | eq_fm (Eq ac) (NEq bc) = false |
416 | eq_fm (Eq a) (NEq b) = false |
417 | eq_fm (Ge ac) (NClosed b) = false |
417 | eq_fm (Ge a) (NClosed b) = false |
418 | eq_fm (Ge ac) (Closed b) = false |
418 | eq_fm (Ge a) (Closed b) = false |
419 | eq_fm (Ge ac) (A bb) = false |
419 | eq_fm (Ge a) (A b) = false |
420 | eq_fm (Ge ac) (E bb) = false |
420 | eq_fm (Ge a) (E b) = false |
421 | eq_fm (Ge ac) (Iff (bb, cb)) = false |
421 | eq_fm (Ge a) (Iff (b, c)) = false |
422 | eq_fm (Ge ac) (Imp (bb, cb)) = false |
422 | eq_fm (Ge a) (Imp (b, c)) = false |
423 | eq_fm (Ge ac) (Or (bb, cb)) = false |
423 | eq_fm (Ge a) (Or (b, c)) = false |
424 | eq_fm (Ge ac) (And (bb, cb)) = false |
424 | eq_fm (Ge a) (And (b, c)) = false |
425 | eq_fm (Ge ac) (Not bb) = false |
425 | eq_fm (Ge a) (Not b) = false |
426 | eq_fm (Ge ac) (NDvd (ba, cc)) = false |
426 | eq_fm (Ge a) (NDvd (b, c)) = false |
427 | eq_fm (Ge ac) (Dvd (ba, cc)) = false |
427 | eq_fm (Ge a) (Dvd (b, c)) = false |
428 | eq_fm (Ge ac) (NEq bc) = false |
428 | eq_fm (Ge a) (NEq b) = false |
429 | eq_fm (Ge ac) (Eq bc) = false |
429 | eq_fm (Ge a) (Eq b) = false |
430 | eq_fm (Gt ac) (NClosed b) = false |
430 | eq_fm (Gt a) (NClosed b) = false |
431 | eq_fm (Gt ac) (Closed b) = false |
431 | eq_fm (Gt a) (Closed b) = false |
432 | eq_fm (Gt ac) (A bb) = false |
432 | eq_fm (Gt a) (A b) = false |
433 | eq_fm (Gt ac) (E bb) = false |
433 | eq_fm (Gt a) (E b) = false |
434 | eq_fm (Gt ac) (Iff (bb, cb)) = false |
434 | eq_fm (Gt a) (Iff (b, c)) = false |
435 | eq_fm (Gt ac) (Imp (bb, cb)) = false |
435 | eq_fm (Gt a) (Imp (b, c)) = false |
436 | eq_fm (Gt ac) (Or (bb, cb)) = false |
436 | eq_fm (Gt a) (Or (b, c)) = false |
437 | eq_fm (Gt ac) (And (bb, cb)) = false |
437 | eq_fm (Gt a) (And (b, c)) = false |
438 | eq_fm (Gt ac) (Not bb) = false |
438 | eq_fm (Gt a) (Not b) = false |
439 | eq_fm (Gt ac) (NDvd (ba, cc)) = false |
439 | eq_fm (Gt a) (NDvd (b, c)) = false |
440 | eq_fm (Gt ac) (Dvd (ba, cc)) = false |
440 | eq_fm (Gt a) (Dvd (b, c)) = false |
441 | eq_fm (Gt ac) (NEq bc) = false |
441 | eq_fm (Gt a) (NEq b) = false |
442 | eq_fm (Gt ac) (Eq bc) = false |
442 | eq_fm (Gt a) (Eq b) = false |
443 | eq_fm (Gt ac) (Ge bc) = false |
443 | eq_fm (Gt a) (Ge b) = false |
444 | eq_fm (Le ac) (NClosed b) = false |
444 | eq_fm (Le a) (NClosed b) = false |
445 | eq_fm (Le ac) (Closed b) = false |
445 | eq_fm (Le a) (Closed b) = false |
446 | eq_fm (Le ac) (A bb) = false |
446 | eq_fm (Le a) (A b) = false |
447 | eq_fm (Le ac) (E bb) = false |
447 | eq_fm (Le a) (E b) = false |
448 | eq_fm (Le ac) (Iff (bb, cb)) = false |
448 | eq_fm (Le a) (Iff (b, c)) = false |
449 | eq_fm (Le ac) (Imp (bb, cb)) = false |
449 | eq_fm (Le a) (Imp (b, c)) = false |
450 | eq_fm (Le ac) (Or (bb, cb)) = false |
450 | eq_fm (Le a) (Or (b, c)) = false |
451 | eq_fm (Le ac) (And (bb, cb)) = false |
451 | eq_fm (Le a) (And (b, c)) = false |
452 | eq_fm (Le ac) (Not bb) = false |
452 | eq_fm (Le a) (Not b) = false |
453 | eq_fm (Le ac) (NDvd (ba, cc)) = false |
453 | eq_fm (Le a) (NDvd (b, c)) = false |
454 | eq_fm (Le ac) (Dvd (ba, cc)) = false |
454 | eq_fm (Le a) (Dvd (b, c)) = false |
455 | eq_fm (Le ac) (NEq bc) = false |
455 | eq_fm (Le a) (NEq b) = false |
456 | eq_fm (Le ac) (Eq bc) = false |
456 | eq_fm (Le a) (Eq b) = false |
457 | eq_fm (Le ac) (Ge bc) = false |
457 | eq_fm (Le a) (Ge b) = false |
458 | eq_fm (Le ac) (Gt bc) = false |
458 | eq_fm (Le a) (Gt b) = false |
459 | eq_fm (Lt ac) (NClosed b) = false |
459 | eq_fm (Lt a) (NClosed b) = false |
460 | eq_fm (Lt ac) (Closed b) = false |
460 | eq_fm (Lt a) (Closed b) = false |
461 | eq_fm (Lt ac) (A bb) = false |
461 | eq_fm (Lt a) (A b) = false |
462 | eq_fm (Lt ac) (E bb) = false |
462 | eq_fm (Lt a) (E b) = false |
463 | eq_fm (Lt ac) (Iff (bb, cb)) = false |
463 | eq_fm (Lt a) (Iff (b, c)) = false |
464 | eq_fm (Lt ac) (Imp (bb, cb)) = false |
464 | eq_fm (Lt a) (Imp (b, c)) = false |
465 | eq_fm (Lt ac) (Or (bb, cb)) = false |
465 | eq_fm (Lt a) (Or (b, c)) = false |
466 | eq_fm (Lt ac) (And (bb, cb)) = false |
466 | eq_fm (Lt a) (And (b, c)) = false |
467 | eq_fm (Lt ac) (Not bb) = false |
467 | eq_fm (Lt a) (Not b) = false |
468 | eq_fm (Lt ac) (NDvd (ba, cc)) = false |
468 | eq_fm (Lt a) (NDvd (b, c)) = false |
469 | eq_fm (Lt ac) (Dvd (ba, cc)) = false |
469 | eq_fm (Lt a) (Dvd (b, c)) = false |
470 | eq_fm (Lt ac) (NEq bc) = false |
470 | eq_fm (Lt a) (NEq b) = false |
471 | eq_fm (Lt ac) (Eq bc) = false |
471 | eq_fm (Lt a) (Eq b) = false |
472 | eq_fm (Lt ac) (Ge bc) = false |
472 | eq_fm (Lt a) (Ge b) = false |
473 | eq_fm (Lt ac) (Gt bc) = false |
473 | eq_fm (Lt a) (Gt b) = false |
474 | eq_fm (Lt ac) (Le bc) = false |
474 | eq_fm (Lt a) (Le b) = false |
475 | eq_fm F (NClosed a) = false |
475 | eq_fm F (NClosed a) = false |
476 | eq_fm F (Closed a) = false |
476 | eq_fm F (Closed a) = false |
477 | eq_fm F (A ab) = false |
477 | eq_fm F (A a) = false |
478 | eq_fm F (E ab) = false |
478 | eq_fm F (E a) = false |
479 | eq_fm F (Iff (ab, bb)) = false |
479 | eq_fm F (Iff (a, b)) = false |
480 | eq_fm F (Imp (ab, bb)) = false |
480 | eq_fm F (Imp (a, b)) = false |
481 | eq_fm F (Or (ab, bb)) = false |
481 | eq_fm F (Or (a, b)) = false |
482 | eq_fm F (And (ab, bb)) = false |
482 | eq_fm F (And (a, b)) = false |
483 | eq_fm F (Not ab) = false |
483 | eq_fm F (Not a) = false |
484 | eq_fm F (NDvd (aa, bc)) = false |
484 | eq_fm F (NDvd (a, b)) = false |
485 | eq_fm F (Dvd (aa, bc)) = false |
485 | eq_fm F (Dvd (a, b)) = false |
486 | eq_fm F (NEq ac) = false |
486 | eq_fm F (NEq a) = false |
487 | eq_fm F (Eq ac) = false |
487 | eq_fm F (Eq a) = false |
488 | eq_fm F (Ge ac) = false |
488 | eq_fm F (Ge a) = false |
489 | eq_fm F (Gt ac) = false |
489 | eq_fm F (Gt a) = false |
490 | eq_fm F (Le ac) = false |
490 | eq_fm F (Le a) = false |
491 | eq_fm F (Lt ac) = false |
491 | eq_fm F (Lt a) = false |
492 | eq_fm T (NClosed a) = false |
492 | eq_fm T (NClosed a) = false |
493 | eq_fm T (Closed a) = false |
493 | eq_fm T (Closed a) = false |
494 | eq_fm T (A ab) = false |
494 | eq_fm T (A a) = false |
495 | eq_fm T (E ab) = false |
495 | eq_fm T (E a) = false |
496 | eq_fm T (Iff (ab, bb)) = false |
496 | eq_fm T (Iff (a, b)) = false |
497 | eq_fm T (Imp (ab, bb)) = false |
497 | eq_fm T (Imp (a, b)) = false |
498 | eq_fm T (Or (ab, bb)) = false |
498 | eq_fm T (Or (a, b)) = false |
499 | eq_fm T (And (ab, bb)) = false |
499 | eq_fm T (And (a, b)) = false |
500 | eq_fm T (Not ab) = false |
500 | eq_fm T (Not a) = false |
501 | eq_fm T (NDvd (aa, bc)) = false |
501 | eq_fm T (NDvd (a, b)) = false |
502 | eq_fm T (Dvd (aa, bc)) = false |
502 | eq_fm T (Dvd (a, b)) = false |
503 | eq_fm T (NEq ac) = false |
503 | eq_fm T (NEq a) = false |
504 | eq_fm T (Eq ac) = false |
504 | eq_fm T (Eq a) = false |
505 | eq_fm T (Ge ac) = false |
505 | eq_fm T (Ge a) = false |
506 | eq_fm T (Gt ac) = false |
506 | eq_fm T (Gt a) = false |
507 | eq_fm T (Le ac) = false |
507 | eq_fm T (Le a) = false |
508 | eq_fm T (Lt ac) = false |
508 | eq_fm T (Lt a) = false |
509 | eq_fm T F = false |
509 | eq_fm T F = false |
510 | eq_fm (NClosed nat) (NClosed nat') = ((nat : IntInf.int) = nat') |
510 | eq_fm (NClosed nat) (NClosed nat') = ((nat : IntInf.int) = nat') |
511 | eq_fm (Closed nat) (Closed nat') = ((nat : IntInf.int) = nat') |
511 | eq_fm (Closed nat) (Closed nat') = ((nat : IntInf.int) = nat') |
512 | eq_fm (A fm) (A fm') = eq_fm fm fm' |
512 | eq_fm (A fm) (A fm') = eq_fm fm fm' |
513 | eq_fm (E fm) (E fm') = eq_fm fm fm' |
513 | eq_fm (E fm) (E fm') = eq_fm fm fm' |