equal
deleted
inserted
replaced
6 Miscellaneous examples for Zermelo-Fraenkel Set Theory |
6 Miscellaneous examples for Zermelo-Fraenkel Set Theory |
7 Composition of homomorphisms, Pastre's examples, ... |
7 Composition of homomorphisms, Pastre's examples, ... |
8 *) |
8 *) |
9 |
9 |
10 writeln"ZF/ex/misc"; |
10 writeln"ZF/ex/misc"; |
|
11 |
|
12 (*These two are cited in Benzmueller and Kohlhash's system description of LEO, |
|
13 CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*) |
|
14 |
|
15 Goal "(X = Y Un Z) <-> (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))"; |
|
16 by (blast_tac (claset() addSIs [equalityI]) 1); |
|
17 result(); |
|
18 |
|
19 (*the dual of the previous one*) |
|
20 Goal "(X = Y Int Z) <-> (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))"; |
|
21 by (blast_tac (claset() addSIs [equalityI]) 1); |
|
22 result(); |
11 |
23 |
12 (*trivial example of term synthesis: apparently hard for some provers!*) |
24 (*trivial example of term synthesis: apparently hard for some provers!*) |
13 Goal "a ~= b ==> a:?X & b ~: ?X"; |
25 Goal "a ~= b ==> a:?X & b ~: ?X"; |
14 by (Blast_tac 1); |
26 by (Blast_tac 1); |
15 result(); |
27 result(); |