8557
|
1 |
(* Title: HOL/ex/mesontest2
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 2000 University of Cambridge
|
|
5 |
|
|
6 |
MORE and MUCH HARDER test data for the MESON proof procedure
|
|
7 |
|
|
8 |
Courtesy John Harrison
|
|
9 |
*)
|
|
10 |
|
|
11 |
(*All but the fastest are ignored to reduce build time*)
|
|
12 |
val even_hard_ones = false;
|
|
13 |
|
|
14 |
(*Prod.thy instead of HOL.thy regards arguments as tuples.
|
|
15 |
But Main.thy would allow clashes with many other constants*)
|
|
16 |
fun prove (s,tac) = prove_goal Prod.thy s (fn [] => [tac]);
|
|
17 |
|
|
18 |
fun prove_hard arg = if even_hard_ones then prove arg else TrueI;
|
|
19 |
|
|
20 |
val meson_tac = safe_meson_tac 1;
|
|
21 |
|
9000
|
22 |
set timing;
|
8557
|
23 |
|
|
24 |
(* ========================================================================= *)
|
|
25 |
(* 100 problems selected from the TPTP library *)
|
|
26 |
(* ========================================================================= *)
|
|
27 |
|
|
28 |
(*
|
|
29 |
* Original timings for John Harrison's MESON_TAC.
|
|
30 |
* Timings below on a 600MHz Pentium III (perch)
|
|
31 |
*
|
|
32 |
* A few variable names have been primed to avoid clashing with constants.
|
|
33 |
*
|
|
34 |
* Changed numeric constants e.g. 0, 1, 2... to num0, num1, num2...
|
|
35 |
*
|
|
36 |
* Here's a list giving typical CPU times, as well as common names and
|
|
37 |
* literature references.
|
|
38 |
*
|
|
39 |
* BOO003-1 34.6 B2 part 1 [McCharen, et al., 1976]; Lemma proved [Overbeek, et al., 1976]; prob2_part1.ver1.in [ANL]
|
|
40 |
* BOO004-1 36.7 B2 part 2 [McCharen, et al., 1976]; Lemma proved [Overbeek, et al., 1976]; prob2_part2.ver1 [ANL]
|
|
41 |
* BOO005-1 47.4 B3 part 1 [McCharen, et al., 1976]; B5 [McCharen, et al., 1976]; Lemma proved [Overbeek, et al., 1976]; prob3_part1.ver1.in [ANL]
|
|
42 |
* BOO006-1 48.4 B3 part 2 [McCharen, et al., 1976]; B6 [McCharen, et al., 1976]; Lemma proved [Overbeek, et al., 1976]; prob3_part2.ver1 [ANL]
|
|
43 |
* BOO011-1 19.0 B7 [McCharen, et al., 1976]; prob7.ver1 [ANL]
|
|
44 |
* CAT001-3 45.2 C1 [McCharen, et al., 1976]; p1.ver3.in [ANL]
|
|
45 |
* CAT003-3 10.5 C3 [McCharen, et al., 1976]; p3.ver3.in [ANL]
|
|
46 |
* CAT005-1 480.1 C5 [McCharen, et al., 1976]; p5.ver1.in [ANL]
|
|
47 |
* CAT007-1 11.9 C7 [McCharen, et al., 1976]; p7.ver1.in [ANL]
|
|
48 |
* CAT018-1 81.3 p18.ver1.in [ANL]
|
|
49 |
* COL001-2 16.0 C1 [Wos & McCune, 1988]
|
|
50 |
* COL023-1 5.1 [McCune & Wos, 1988]
|
|
51 |
* COL032-1 15.8 [McCune & Wos, 1988]
|
|
52 |
* COL052-2 13.2 bird4.ver2.in [ANL]
|
|
53 |
* COL075-2 116.9 [Jech, 1994]
|
|
54 |
* COM001-1 1.7 shortburst [Wilson & Minker, 1976]
|
|
55 |
* COM002-1 4.4 burstall [Wilson & Minker, 1976]
|
|
56 |
* COM002-2 7.4
|
|
57 |
* COM003-2 22.1 [Brushi, 1991]
|
|
58 |
* COM004-1 45.1
|
|
59 |
* GEO003-1 71.7 T3 [McCharen, et al., 1976]; t3.ver1.in [ANL]
|
|
60 |
* GEO017-2 78.8 D4.1 [Quaife, 1989]
|
|
61 |
* GEO027-3 181.5 D10.1 [Quaife, 1989]
|
|
62 |
* GEO058-2 104.0 R4 [Quaife, 1989]
|
|
63 |
* GEO079-1 2.4 GEOMETRY THEOREM [Slagle, 1967]
|
|
64 |
* GRP001-1 47.8 CADE-11 Competition 1 [Overbeek, 1990]; G1 [McCharen, et al., 1976]; THEOREM 1 [Lusk & McCune, 1993]; wos10 [Wilson & Minker, 1976]; xsquared.ver1.in [ANL]; [Robinson, 1963]
|
|
65 |
* GRP008-1 50.4 Problem 4 [Wos, 1965]; wos4 [Wilson & Minker, 1976]
|
|
66 |
* GRP013-1 40.2 Problem 11 [Wos, 1965]; wos11 [Wilson & Minker, 1976]
|
|
67 |
* GRP037-3 43.8 Problem 17 [Wos, 1965]; wos17 [Wilson & Minker, 1976]
|
|
68 |
* GRP031-2 3.2 ls23 [Lawrence & Starkey, 1974]; ls23 [Wilson & Minker, 1976]
|
|
69 |
* GRP034-4 2.5 ls26 [Lawrence & Starkey, 1974]; ls26 [Wilson & Minker, 1976]
|
|
70 |
* GRP047-2 11.7 [Veroff, 1992]
|
|
71 |
* GRP130-1 170.6 Bennett QG8 [TPTP]; QG8 [Slaney, 1993]
|
|
72 |
* GRP156-1 48.7 ax_mono1c [Schulz, 1995]
|
|
73 |
* GRP168-1 159.1 p01a [Schulz, 1995]
|
|
74 |
* HEN003-3 39.9 HP3 [McCharen, et al., 1976]
|
|
75 |
* HEN007-2 125.7 H7 [McCharen, et al., 1976]
|
|
76 |
* HEN008-4 62.0 H8 [McCharen, et al., 1976]
|
|
77 |
* HEN009-5 136.3 H9 [McCharen, et al., 1976]; hp9.ver3.in [ANL]
|
|
78 |
* HEN012-3 48.5 new.ver2.in [ANL]
|
|
79 |
* LCL010-1 370.9 EC-73 [McCune & Wos, 1992]; ec_yq.in [OTTER]
|
|
80 |
* LCL077-2 51.6 morgan.two.ver1.in [ANL]
|
|
81 |
* LCL082-1 14.6 IC-1.1 [Wos, et al., 1990]; IC-65 [McCune & Wos, 1992]; ls2 [SETHEO]; S1 [Pfenning, 1988]
|
|
82 |
* LCL111-1 585.6 CADE-11 Competition 6 [Overbeek, 1990]; mv25.in [OTTER]; MV-57 [McCune & Wos, 1992]; mv.in part 2 [OTTER]; ovb6 [SETHEO]; THEOREM 6 [Lusk & McCune, 1993]
|
|
83 |
* LCL143-1 10.9 Lattice structure theorem 2 [Bonacina, 1991]
|
|
84 |
* LCL182-1 271.6 Problem 2.16 [Whitehead & Russell, 1927]
|
|
85 |
* LCL200-1 12.0 Problem 2.46 [Whitehead & Russell, 1927]
|
|
86 |
* LCL215-1 214.4 Problem 2.62 [Whitehead & Russell, 1927]; Problem 2.63 [Whitehead & Russell, 1927]
|
|
87 |
* LCL230-2 0.2 Pelletier 5 [Pelletier, 1986]
|
|
88 |
* LDA003-1 68.5 Problem 3 [Jech, 1993]
|
|
89 |
* MSC002-1 9.2 DBABHP [Michie, et al., 1972]; DBABHP [Wilson & Minker, 1976]
|
|
90 |
* MSC003-1 3.2 HASPARTS-T1 [Wilson & Minker, 1976]
|
|
91 |
* MSC004-1 9.3 HASPARTS-T2 [Wilson & Minker, 1976]
|
|
92 |
* MSC005-1 1.8 Problem 5.1 [Plaisted, 1982]
|
|
93 |
* MSC006-1 39.0 nonob.lop [SETHEO]
|
|
94 |
* NUM001-1 14.0 Chang-Lee-10a [Chang, 1970]; ls28 [Lawrence & Starkey, 1974]; ls28 [Wilson & Minker, 1976]
|
|
95 |
* NUM021-1 52.3 ls65 [Lawrence & Starkey, 1974]; ls65 [Wilson & Minker, 1976]
|
|
96 |
* NUM024-1 64.6 ls75 [Lawrence & Starkey, 1974]; ls75 [Wilson & Minker, 1976]
|
|
97 |
* NUM180-1 621.2 LIM2.1 [Quaife]
|
|
98 |
* NUM228-1 575.9 TRECDEF4 cor. [Quaife]
|
|
99 |
* PLA002-1 37.4 Problem 5.7 [Plaisted, 1982]
|
|
100 |
* PLA006-1 7.2 [Segre & Elkan, 1994]
|
|
101 |
* PLA017-1 484.8 [Segre & Elkan, 1994]
|
|
102 |
* PLA022-1 19.1 [Segre & Elkan, 1994]
|
|
103 |
* PLA022-2 19.7 [Segre & Elkan, 1994]
|
|
104 |
* PRV001-1 10.3 PV1 [McCharen, et al., 1976]
|
|
105 |
* PRV003-1 3.9 E2 [McCharen, et al., 1976]; v2.lop [SETHEO]
|
|
106 |
* PRV005-1 4.3 E4 [McCharen, et al., 1976]; v4.lop [SETHEO]
|
|
107 |
* PRV006-1 6.0 E5 [McCharen, et al., 1976]; v5.lop [SETHEO]
|
|
108 |
* PRV009-1 2.2 Hoares FIND [Bledsoe, 1977]; Problem 5.5 [Plaisted, 1982]
|
|
109 |
* PUZ012-1 3.5 Boxes-of-fruit [Wos, 1988]; Boxes-of-fruit [Wos, et al., 1992]; boxes.ver1.in [ANL]
|
|
110 |
* PUZ020-1 56.6 knightknave.in [ANL]
|
|
111 |
* PUZ025-1 58.4 Problem 35 [Smullyan, 1978]; tandl35.ver1.in [ANL]
|
|
112 |
* PUZ029-1 5.1 pigs.ver1.in [ANL]
|
|
113 |
* RNG001-3 82.4 EX6-T? [Wilson & Minker, 1976]; ex6.lop [SETHEO]; Example 6a [Fleisig, et al., 1974]; FEX6T1 [SPRFN]; FEX6T2 [SPRFN]
|
|
114 |
* RNG001-5 399.8 Problem 21 [Wos, 1965]; wos21 [Wilson & Minker, 1976]
|
|
115 |
* RNG011-5 8.4 CADE-11 Competition Eq-10 [Overbeek, 1990]; PROBLEM 10 [Zhang, 1993]; THEOREM EQ-10 [Lusk & McCune, 1993]
|
|
116 |
* RNG023-6 9.1 [Stevens, 1987]
|
|
117 |
* RNG028-2 9.3 PROOF III [Anantharaman & Hsiang, 1990]
|
|
118 |
* RNG038-2 16.2 Problem 27 [Wos, 1965]; wos27 [Wilson & Minker, 1976]
|
|
119 |
* RNG040-2 180.5 Problem 29 [Wos, 1965]; wos29 [Wilson & Minker, 1976]
|
|
120 |
* RNG041-1 35.8 Problem 30 [Wos, 1965]; wos30 [Wilson & Minker, 1976]
|
|
121 |
* ROB010-1 205.0 Lemma 3.3 [Winker, 1990]; RA2 [Lusk & Wos, 1992]
|
|
122 |
* ROB013-1 23.6 Lemma 3.5 [Winker, 1990]
|
|
123 |
* ROB016-1 15.2 Corollary 3.7 [Winker, 1990]
|
|
124 |
* ROB021-1 230.4 [McCune, 1992]
|
|
125 |
* SET005-1 192.2 ls108 [Lawrence & Starkey, 1974]; ls108 [Wilson & Minker, 1976]
|
|
126 |
* SET009-1 10.5 ls116 [Lawrence & Starkey, 1974]; ls116 [Wilson & Minker, 1976]
|
|
127 |
* SET025-4 694.7 Lemma 10 [Boyer, et al, 1986]
|
|
128 |
* SET046-5 2.3 p42.in [ANL]; Pelletier 42 [Pelletier, 1986]
|
|
129 |
* SET047-5 3.7 p43.in [ANL]; Pelletier 43 [Pelletier, 1986]
|
|
130 |
* SYN034-1 2.8 QW [Michie, et al., 1972]; QW [Wilson & Minker, 1976]
|
|
131 |
* SYN071-1 1.9 Pelletier 48 [Pelletier, 1986]
|
|
132 |
* SYN349-1 61.7 Ch17N5 [Tammet, 1994]
|
|
133 |
* SYN352-1 5.5 Ch18N4 [Tammet, 1994]
|
|
134 |
* TOP001-2 61.1 Lemma 1a [Wick & McCune, 1989]
|
|
135 |
* TOP002-2 0.4 Lemma 1b [Wick & McCune, 1989]
|
|
136 |
* TOP004-1 181.6 Lemma 1d [Wick & McCune, 1989]
|
|
137 |
* TOP004-2 9.0 Lemma 1d [Wick & McCune, 1989]
|
|
138 |
* TOP005-2 139.8 Lemma 1e [Wick & McCune, 1989]
|
|
139 |
*)
|
|
140 |
|
|
141 |
(*51194 inferences so far. Searching to depth 13. 232.9 secs*)
|
|
142 |
val BOO003_1 = prove_hard
|
|
143 |
("(! X. equal(X::'a,X)) & \
|
|
144 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
145 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
146 |
\ (! X Y. sum(X::'a,Y,add(X::'a,Y))) & \
|
|
147 |
\ (! X Y. product(X::'a,Y,multiply(X::'a,Y))) & \
|
|
148 |
\ (! Y X Z. sum(X::'a,Y,Z) --> sum(Y::'a,X,Z)) & \
|
|
149 |
\ (! Y X Z. product(X::'a,Y,Z) --> product(Y::'a,X,Z)) & \
|
|
150 |
\ (! X. sum(additive_identity::'a,X,X)) & \
|
|
151 |
\ (! X. sum(X::'a,additive_identity,X)) & \
|
|
152 |
\ (! X. product(multiplicative_identity::'a,X,X)) & \
|
|
153 |
\ (! X. product(X::'a,multiplicative_identity,X)) & \
|
|
154 |
\ (! Y Z X V3 V1 V2 V4. product(X::'a,Y,V1) & product(X::'a,Z,V2) & sum(Y::'a,Z,V3) & product(X::'a,V3,V4) --> sum(V1::'a,V2,V4)) & \
|
|
155 |
\ (! Y Z V1 V2 X V3 V4. product(X::'a,Y,V1) & product(X::'a,Z,V2) & sum(Y::'a,Z,V3) & sum(V1::'a,V2,V4) --> product(X::'a,V3,V4)) & \
|
|
156 |
\ (! Y Z V3 X V1 V2 V4. product(Y::'a,X,V1) & product(Z::'a,X,V2) & sum(Y::'a,Z,V3) & product(V3::'a,X,V4) --> sum(V1::'a,V2,V4)) & \
|
|
157 |
\ (! Y Z V1 V2 V3 X V4. product(Y::'a,X,V1) & product(Z::'a,X,V2) & sum(Y::'a,Z,V3) & sum(V1::'a,V2,V4) --> product(V3::'a,X,V4)) & \
|
|
158 |
\ (! Y Z X V3 V1 V2 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & sum(X::'a,V3,V4) --> product(V1::'a,V2,V4)) & \
|
|
159 |
\ (! Y Z V1 V2 X V3 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(X::'a,V3,V4)) & \
|
|
160 |
\ (! Y Z V3 X V1 V2 V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & sum(V3::'a,X,V4) --> product(V1::'a,V2,V4)) & \
|
|
161 |
\ (! Y Z V1 V2 V3 X V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(V3::'a,X,V4)) & \
|
|
162 |
\ (! X. sum(inverse(X),X,multiplicative_identity)) & \
|
|
163 |
\ (! X. sum(X::'a,inverse(X),multiplicative_identity)) & \
|
|
164 |
\ (! X. product(inverse(X),X,additive_identity)) & \
|
|
165 |
\ (! X. product(X::'a,inverse(X),additive_identity)) & \
|
|
166 |
\ (! X Y U V. sum(X::'a,Y,U) & sum(X::'a,Y,V) --> equal(U::'a,V)) & \
|
|
167 |
\ (! X Y U V. product(X::'a,Y,U) & product(X::'a,Y,V) --> equal(U::'a,V)) & \
|
|
168 |
\ (! X Y W Z. equal(X::'a,Y) & sum(X::'a,W,Z) --> sum(Y::'a,W,Z)) & \
|
|
169 |
\ (! X W Y Z. equal(X::'a,Y) & sum(W::'a,X,Z) --> sum(W::'a,Y,Z)) & \
|
|
170 |
\ (! X W Z Y. equal(X::'a,Y) & sum(W::'a,Z,X) --> sum(W::'a,Z,Y)) & \
|
|
171 |
\ (! X Y W Z. equal(X::'a,Y) & product(X::'a,W,Z) --> product(Y::'a,W,Z)) & \
|
|
172 |
\ (! X W Y Z. equal(X::'a,Y) & product(W::'a,X,Z) --> product(W::'a,Y,Z)) & \
|
|
173 |
\ (! X W Z Y. equal(X::'a,Y) & product(W::'a,Z,X) --> product(W::'a,Z,Y)) & \
|
|
174 |
\ (! X Y W. equal(X::'a,Y) --> equal(add(X::'a,W),add(Y::'a,W))) & \
|
|
175 |
\ (! X W Y. equal(X::'a,Y) --> equal(add(W::'a,X),add(W::'a,Y))) & \
|
|
176 |
\ (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) & \
|
|
177 |
\ (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) & \
|
|
178 |
\ (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) & \
|
|
179 |
\ (~product(x::'a,x,x)) --> False",
|
|
180 |
meson_tac);
|
|
181 |
|
|
182 |
(*51194 inferences so far. Searching to depth 13. 204.6 secs
|
|
183 |
Strange! The previous problem also has 51194 inferences at depth 13. They
|
|
184 |
must be very similar!*)
|
|
185 |
val BOO004_1 = prove_hard
|
|
186 |
("(! X. equal(X::'a,X)) & \
|
|
187 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
188 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
189 |
\ (! X Y. sum(X::'a,Y,add(X::'a,Y))) & \
|
|
190 |
\ (! X Y. product(X::'a,Y,multiply(X::'a,Y))) & \
|
|
191 |
\ (! Y X Z. sum(X::'a,Y,Z) --> sum(Y::'a,X,Z)) & \
|
|
192 |
\ (! Y X Z. product(X::'a,Y,Z) --> product(Y::'a,X,Z)) & \
|
|
193 |
\ (! X. sum(additive_identity::'a,X,X)) & \
|
|
194 |
\ (! X. sum(X::'a,additive_identity,X)) & \
|
|
195 |
\ (! X. product(multiplicative_identity::'a,X,X)) & \
|
|
196 |
\ (! X. product(X::'a,multiplicative_identity,X)) & \
|
|
197 |
\ (! Y Z X V3 V1 V2 V4. product(X::'a,Y,V1) & product(X::'a,Z,V2) & sum(Y::'a,Z,V3) & product(X::'a,V3,V4) --> sum(V1::'a,V2,V4)) & \
|
|
198 |
\ (! Y Z V1 V2 X V3 V4. product(X::'a,Y,V1) & product(X::'a,Z,V2) & sum(Y::'a,Z,V3) & sum(V1::'a,V2,V4) --> product(X::'a,V3,V4)) & \
|
|
199 |
\ (! Y Z V3 X V1 V2 V4. product(Y::'a,X,V1) & product(Z::'a,X,V2) & sum(Y::'a,Z,V3) & product(V3::'a,X,V4) --> sum(V1::'a,V2,V4)) & \
|
|
200 |
\ (! Y Z V1 V2 V3 X V4. product(Y::'a,X,V1) & product(Z::'a,X,V2) & sum(Y::'a,Z,V3) & sum(V1::'a,V2,V4) --> product(V3::'a,X,V4)) & \
|
|
201 |
\ (! Y Z X V3 V1 V2 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & sum(X::'a,V3,V4) --> product(V1::'a,V2,V4)) & \
|
|
202 |
\ (! Y Z V1 V2 X V3 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(X::'a,V3,V4)) & \
|
|
203 |
\ (! Y Z V3 X V1 V2 V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & sum(V3::'a,X,V4) --> product(V1::'a,V2,V4)) & \
|
|
204 |
\ (! Y Z V1 V2 V3 X V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(V3::'a,X,V4)) & \
|
|
205 |
\ (! X. sum(inverse(X),X,multiplicative_identity)) & \
|
|
206 |
\ (! X. sum(X::'a,inverse(X),multiplicative_identity)) & \
|
|
207 |
\ (! X. product(inverse(X),X,additive_identity)) & \
|
|
208 |
\ (! X. product(X::'a,inverse(X),additive_identity)) & \
|
|
209 |
\ (! X Y U V. sum(X::'a,Y,U) & sum(X::'a,Y,V) --> equal(U::'a,V)) & \
|
|
210 |
\ (! X Y U V. product(X::'a,Y,U) & product(X::'a,Y,V) --> equal(U::'a,V)) & \
|
|
211 |
\ (! X Y W Z. equal(X::'a,Y) & sum(X::'a,W,Z) --> sum(Y::'a,W,Z)) & \
|
|
212 |
\ (! X W Y Z. equal(X::'a,Y) & sum(W::'a,X,Z) --> sum(W::'a,Y,Z)) & \
|
|
213 |
\ (! X W Z Y. equal(X::'a,Y) & sum(W::'a,Z,X) --> sum(W::'a,Z,Y)) & \
|
|
214 |
\ (! X Y W Z. equal(X::'a,Y) & product(X::'a,W,Z) --> product(Y::'a,W,Z)) & \
|
|
215 |
\ (! X W Y Z. equal(X::'a,Y) & product(W::'a,X,Z) --> product(W::'a,Y,Z)) & \
|
|
216 |
\ (! X W Z Y. equal(X::'a,Y) & product(W::'a,Z,X) --> product(W::'a,Z,Y)) & \
|
|
217 |
\ (! X Y W. equal(X::'a,Y) --> equal(add(X::'a,W),add(Y::'a,W))) & \
|
|
218 |
\ (! X W Y. equal(X::'a,Y) --> equal(add(W::'a,X),add(W::'a,Y))) & \
|
|
219 |
\ (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) & \
|
|
220 |
\ (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) & \
|
|
221 |
\ (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) & \
|
|
222 |
\ (~sum(x::'a,x,x)) --> False",
|
|
223 |
meson_tac);
|
|
224 |
|
|
225 |
(*74799 inferences so far. Searching to depth 13. 290.0 secs*)
|
|
226 |
val BOO005_1 = prove_hard
|
|
227 |
("(! X. equal(X::'a,X)) & \
|
|
228 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
229 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
230 |
\ (! X Y. sum(X::'a,Y,add(X::'a,Y))) & \
|
|
231 |
\ (! X Y. product(X::'a,Y,multiply(X::'a,Y))) & \
|
|
232 |
\ (! Y X Z. sum(X::'a,Y,Z) --> sum(Y::'a,X,Z)) & \
|
|
233 |
\ (! Y X Z. product(X::'a,Y,Z) --> product(Y::'a,X,Z)) & \
|
|
234 |
\ (! X. sum(additive_identity::'a,X,X)) & \
|
|
235 |
\ (! X. sum(X::'a,additive_identity,X)) & \
|
|
236 |
\ (! X. product(multiplicative_identity::'a,X,X)) & \
|
|
237 |
\ (! X. product(X::'a,multiplicative_identity,X)) & \
|
|
238 |
\ (! Y Z X V3 V1 V2 V4. product(X::'a,Y,V1) & product(X::'a,Z,V2) & sum(Y::'a,Z,V3) & product(X::'a,V3,V4) --> sum(V1::'a,V2,V4)) & \
|
|
239 |
\ (! Y Z V1 V2 X V3 V4. product(X::'a,Y,V1) & product(X::'a,Z,V2) & sum(Y::'a,Z,V3) & sum(V1::'a,V2,V4) --> product(X::'a,V3,V4)) & \
|
|
240 |
\ (! Y Z V3 X V1 V2 V4. product(Y::'a,X,V1) & product(Z::'a,X,V2) & sum(Y::'a,Z,V3) & product(V3::'a,X,V4) --> sum(V1::'a,V2,V4)) & \
|
|
241 |
\ (! Y Z V1 V2 V3 X V4. product(Y::'a,X,V1) & product(Z::'a,X,V2) & sum(Y::'a,Z,V3) & sum(V1::'a,V2,V4) --> product(V3::'a,X,V4)) & \
|
|
242 |
\ (! Y Z X V3 V1 V2 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & sum(X::'a,V3,V4) --> product(V1::'a,V2,V4)) & \
|
|
243 |
\ (! Y Z V1 V2 X V3 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(X::'a,V3,V4)) & \
|
|
244 |
\ (! Y Z V3 X V1 V2 V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & sum(V3::'a,X,V4) --> product(V1::'a,V2,V4)) & \
|
|
245 |
\ (! Y Z V1 V2 V3 X V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(V3::'a,X,V4)) & \
|
|
246 |
\ (! X. sum(inverse(X),X,multiplicative_identity)) & \
|
|
247 |
\ (! X. sum(X::'a,inverse(X),multiplicative_identity)) & \
|
|
248 |
\ (! X. product(inverse(X),X,additive_identity)) & \
|
|
249 |
\ (! X. product(X::'a,inverse(X),additive_identity)) & \
|
|
250 |
\ (! X Y U V. sum(X::'a,Y,U) & sum(X::'a,Y,V) --> equal(U::'a,V)) & \
|
|
251 |
\ (! X Y U V. product(X::'a,Y,U) & product(X::'a,Y,V) --> equal(U::'a,V)) & \
|
|
252 |
\ (! X Y W Z. equal(X::'a,Y) & sum(X::'a,W,Z) --> sum(Y::'a,W,Z)) & \
|
|
253 |
\ (! X W Y Z. equal(X::'a,Y) & sum(W::'a,X,Z) --> sum(W::'a,Y,Z)) & \
|
|
254 |
\ (! X W Z Y. equal(X::'a,Y) & sum(W::'a,Z,X) --> sum(W::'a,Z,Y)) & \
|
|
255 |
\ (! X Y W Z. equal(X::'a,Y) & product(X::'a,W,Z) --> product(Y::'a,W,Z)) & \
|
|
256 |
\ (! X W Y Z. equal(X::'a,Y) & product(W::'a,X,Z) --> product(W::'a,Y,Z)) & \
|
|
257 |
\ (! X W Z Y. equal(X::'a,Y) & product(W::'a,Z,X) --> product(W::'a,Z,Y)) & \
|
|
258 |
\ (! X Y W. equal(X::'a,Y) --> equal(add(X::'a,W),add(Y::'a,W))) & \
|
|
259 |
\ (! X W Y. equal(X::'a,Y) --> equal(add(W::'a,X),add(W::'a,Y))) & \
|
|
260 |
\ (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) & \
|
|
261 |
\ (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) & \
|
|
262 |
\ (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) & \
|
|
263 |
\ (~sum(x::'a,multiplicative_identity,multiplicative_identity)) --> False",
|
|
264 |
meson_tac);
|
|
265 |
|
|
266 |
(*74799 inferences so far. Searching to depth 13. 314.6 secs*)
|
|
267 |
val BOO006_1 = prove_hard
|
|
268 |
("(! X. equal(X::'a,X)) & \
|
|
269 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
270 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
271 |
\ (! X Y. sum(X::'a,Y,add(X::'a,Y))) & \
|
|
272 |
\ (! X Y. product(X::'a,Y,multiply(X::'a,Y))) & \
|
|
273 |
\ (! Y X Z. sum(X::'a,Y,Z) --> sum(Y::'a,X,Z)) & \
|
|
274 |
\ (! Y X Z. product(X::'a,Y,Z) --> product(Y::'a,X,Z)) & \
|
|
275 |
\ (! X. sum(additive_identity::'a,X,X)) & \
|
|
276 |
\ (! X. sum(X::'a,additive_identity,X)) & \
|
|
277 |
\ (! X. product(multiplicative_identity::'a,X,X)) & \
|
|
278 |
\ (! X. product(X::'a,multiplicative_identity,X)) & \
|
|
279 |
\ (! Y Z X V3 V1 V2 V4. product(X::'a,Y,V1) & product(X::'a,Z,V2) & sum(Y::'a,Z,V3) & product(X::'a,V3,V4) --> sum(V1::'a,V2,V4)) & \
|
|
280 |
\ (! Y Z V1 V2 X V3 V4. product(X::'a,Y,V1) & product(X::'a,Z,V2) & sum(Y::'a,Z,V3) & sum(V1::'a,V2,V4) --> product(X::'a,V3,V4)) & \
|
|
281 |
\ (! Y Z V3 X V1 V2 V4. product(Y::'a,X,V1) & product(Z::'a,X,V2) & sum(Y::'a,Z,V3) & product(V3::'a,X,V4) --> sum(V1::'a,V2,V4)) & \
|
|
282 |
\ (! Y Z V1 V2 V3 X V4. product(Y::'a,X,V1) & product(Z::'a,X,V2) & sum(Y::'a,Z,V3) & sum(V1::'a,V2,V4) --> product(V3::'a,X,V4)) & \
|
|
283 |
\ (! Y Z X V3 V1 V2 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & sum(X::'a,V3,V4) --> product(V1::'a,V2,V4)) & \
|
|
284 |
\ (! Y Z V1 V2 X V3 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(X::'a,V3,V4)) & \
|
|
285 |
\ (! Y Z V3 X V1 V2 V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & sum(V3::'a,X,V4) --> product(V1::'a,V2,V4)) & \
|
|
286 |
\ (! Y Z V1 V2 V3 X V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(V3::'a,X,V4)) & \
|
|
287 |
\ (! X. sum(inverse(X),X,multiplicative_identity)) & \
|
|
288 |
\ (! X. sum(X::'a,inverse(X),multiplicative_identity)) & \
|
|
289 |
\ (! X. product(inverse(X),X,additive_identity)) & \
|
|
290 |
\ (! X. product(X::'a,inverse(X),additive_identity)) & \
|
|
291 |
\ (! X Y U V. sum(X::'a,Y,U) & sum(X::'a,Y,V) --> equal(U::'a,V)) & \
|
|
292 |
\ (! X Y U V. product(X::'a,Y,U) & product(X::'a,Y,V) --> equal(U::'a,V)) & \
|
|
293 |
\ (! X Y W Z. equal(X::'a,Y) & sum(X::'a,W,Z) --> sum(Y::'a,W,Z)) & \
|
|
294 |
\ (! X W Y Z. equal(X::'a,Y) & sum(W::'a,X,Z) --> sum(W::'a,Y,Z)) & \
|
|
295 |
\ (! X W Z Y. equal(X::'a,Y) & sum(W::'a,Z,X) --> sum(W::'a,Z,Y)) & \
|
|
296 |
\ (! X Y W Z. equal(X::'a,Y) & product(X::'a,W,Z) --> product(Y::'a,W,Z)) & \
|
|
297 |
\ (! X W Y Z. equal(X::'a,Y) & product(W::'a,X,Z) --> product(W::'a,Y,Z)) & \
|
|
298 |
\ (! X W Z Y. equal(X::'a,Y) & product(W::'a,Z,X) --> product(W::'a,Z,Y)) & \
|
|
299 |
\ (! X Y W. equal(X::'a,Y) --> equal(add(X::'a,W),add(Y::'a,W))) & \
|
|
300 |
\ (! X W Y. equal(X::'a,Y) --> equal(add(W::'a,X),add(W::'a,Y))) & \
|
|
301 |
\ (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) & \
|
|
302 |
\ (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) & \
|
|
303 |
\ (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) & \
|
|
304 |
\ (~product(x::'a,additive_identity,additive_identity)) --> False",
|
|
305 |
meson_tac);
|
|
306 |
|
|
307 |
(*5 inferences so far. Searching to depth 5. 1.3 secs*)
|
|
308 |
val BOO011_1 = prove
|
|
309 |
("(! X. equal(X::'a,X)) & \
|
|
310 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
311 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
312 |
\ (! X Y. sum(X::'a,Y,add(X::'a,Y))) & \
|
|
313 |
\ (! X Y. product(X::'a,Y,multiply(X::'a,Y))) & \
|
|
314 |
\ (! Y X Z. sum(X::'a,Y,Z) --> sum(Y::'a,X,Z)) & \
|
|
315 |
\ (! Y X Z. product(X::'a,Y,Z) --> product(Y::'a,X,Z)) & \
|
|
316 |
\ (! X. sum(additive_identity::'a,X,X)) & \
|
|
317 |
\ (! X. sum(X::'a,additive_identity,X)) & \
|
|
318 |
\ (! X. product(multiplicative_identity::'a,X,X)) & \
|
|
319 |
\ (! X. product(X::'a,multiplicative_identity,X)) & \
|
|
320 |
\ (! Y Z X V3 V1 V2 V4. product(X::'a,Y,V1) & product(X::'a,Z,V2) & sum(Y::'a,Z,V3) & product(X::'a,V3,V4) --> sum(V1::'a,V2,V4)) & \
|
|
321 |
\ (! Y Z V1 V2 X V3 V4. product(X::'a,Y,V1) & product(X::'a,Z,V2) & sum(Y::'a,Z,V3) & sum(V1::'a,V2,V4) --> product(X::'a,V3,V4)) & \
|
|
322 |
\ (! Y Z V3 X V1 V2 V4. product(Y::'a,X,V1) & product(Z::'a,X,V2) & sum(Y::'a,Z,V3) & product(V3::'a,X,V4) --> sum(V1::'a,V2,V4)) & \
|
|
323 |
\ (! Y Z V1 V2 V3 X V4. product(Y::'a,X,V1) & product(Z::'a,X,V2) & sum(Y::'a,Z,V3) & sum(V1::'a,V2,V4) --> product(V3::'a,X,V4)) & \
|
|
324 |
\ (! Y Z X V3 V1 V2 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & sum(X::'a,V3,V4) --> product(V1::'a,V2,V4)) & \
|
|
325 |
\ (! Y Z V1 V2 X V3 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(X::'a,V3,V4)) & \
|
|
326 |
\ (! Y Z V3 X V1 V2 V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & sum(V3::'a,X,V4) --> product(V1::'a,V2,V4)) & \
|
|
327 |
\ (! Y Z V1 V2 V3 X V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(V3::'a,X,V4)) & \
|
|
328 |
\ (! X. sum(inverse(X),X,multiplicative_identity)) & \
|
|
329 |
\ (! X. sum(X::'a,inverse(X),multiplicative_identity)) & \
|
|
330 |
\ (! X. product(inverse(X),X,additive_identity)) & \
|
|
331 |
\ (! X. product(X::'a,inverse(X),additive_identity)) & \
|
|
332 |
\ (! X Y U V. sum(X::'a,Y,U) & sum(X::'a,Y,V) --> equal(U::'a,V)) & \
|
|
333 |
\ (! X Y U V. product(X::'a,Y,U) & product(X::'a,Y,V) --> equal(U::'a,V)) & \
|
|
334 |
\ (! X Y W Z. equal(X::'a,Y) & sum(X::'a,W,Z) --> sum(Y::'a,W,Z)) & \
|
|
335 |
\ (! X W Y Z. equal(X::'a,Y) & sum(W::'a,X,Z) --> sum(W::'a,Y,Z)) & \
|
|
336 |
\ (! X W Z Y. equal(X::'a,Y) & sum(W::'a,Z,X) --> sum(W::'a,Z,Y)) & \
|
|
337 |
\ (! X Y W Z. equal(X::'a,Y) & product(X::'a,W,Z) --> product(Y::'a,W,Z)) & \
|
|
338 |
\ (! X W Y Z. equal(X::'a,Y) & product(W::'a,X,Z) --> product(W::'a,Y,Z)) & \
|
|
339 |
\ (! X W Z Y. equal(X::'a,Y) & product(W::'a,Z,X) --> product(W::'a,Z,Y)) & \
|
|
340 |
\ (! X Y W. equal(X::'a,Y) --> equal(add(X::'a,W),add(Y::'a,W))) & \
|
|
341 |
\ (! X W Y. equal(X::'a,Y) --> equal(add(W::'a,X),add(W::'a,Y))) & \
|
|
342 |
\ (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) & \
|
|
343 |
\ (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) & \
|
|
344 |
\ (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) & \
|
|
345 |
\ (~equal(inverse(additive_identity),multiplicative_identity)) --> False",
|
|
346 |
meson_tac);
|
|
347 |
|
|
348 |
(*4007 inferences so far. Searching to depth 9. 13 secs*)
|
|
349 |
val CAT001_3 = prove_hard
|
|
350 |
("(! X. equal(X::'a,X)) & \
|
|
351 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
352 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
353 |
\ (! Y X. equivalent(X::'a,Y) --> there_exists(X)) & \
|
|
354 |
\ (! X Y. equivalent(X::'a,Y) --> equal(X::'a,Y)) & \
|
|
355 |
\ (! X Y. there_exists(X) & equal(X::'a,Y) --> equivalent(X::'a,Y)) & \
|
|
356 |
\ (! X. there_exists(domain(X)) --> there_exists(X)) & \
|
|
357 |
\ (! X. there_exists(codomain(X)) --> there_exists(X)) & \
|
|
358 |
\ (! Y X. there_exists(compos(X::'a,Y)) --> there_exists(domain(X))) & \
|
|
359 |
\ (! X Y. there_exists(compos(X::'a,Y)) --> equal(domain(X),codomain(Y))) & \
|
|
360 |
\ (! X Y. there_exists(domain(X)) & equal(domain(X),codomain(Y)) --> there_exists(compos(X::'a,Y))) & \
|
|
361 |
\ (! X Y Z. equal(compos(X::'a,compos(Y::'a,Z)),compos(compos(X::'a,Y),Z))) & \
|
|
362 |
\ (! X. equal(compos(X::'a,domain(X)),X)) & \
|
|
363 |
\ (! X. equal(compos(codomain(X),X),X)) & \
|
|
364 |
\ (! X Y. equivalent(X::'a,Y) --> there_exists(Y)) & \
|
|
365 |
\ (! X Y. there_exists(X) & there_exists(Y) & equal(X::'a,Y) --> equivalent(X::'a,Y)) & \
|
|
366 |
\ (! Y X. there_exists(compos(X::'a,Y)) --> there_exists(codomain(X))) & \
|
|
367 |
\ (! X Y. there_exists(f1(X::'a,Y)) | equal(X::'a,Y)) & \
|
|
368 |
\ (! X Y. equal(X::'a,f1(X::'a,Y)) | equal(Y::'a,f1(X::'a,Y)) | equal(X::'a,Y)) & \
|
|
369 |
\ (! X Y. equal(X::'a,f1(X::'a,Y)) & equal(Y::'a,f1(X::'a,Y)) --> equal(X::'a,Y)) & \
|
|
370 |
\ (! X Y. equal(X::'a,Y) & there_exists(X) --> there_exists(Y)) & \
|
|
371 |
\ (! X Y Z. equal(X::'a,Y) & equivalent(X::'a,Z) --> equivalent(Y::'a,Z)) & \
|
|
372 |
\ (! X Z Y. equal(X::'a,Y) & equivalent(Z::'a,X) --> equivalent(Z::'a,Y)) & \
|
|
373 |
\ (! X Y. equal(X::'a,Y) --> equal(domain(X),domain(Y))) & \
|
|
374 |
\ (! X Y. equal(X::'a,Y) --> equal(codomain(X),codomain(Y))) & \
|
|
375 |
\ (! X Y Z. equal(X::'a,Y) --> equal(compos(X::'a,Z),compos(Y::'a,Z))) & \
|
|
376 |
\ (! X Z Y. equal(X::'a,Y) --> equal(compos(Z::'a,X),compos(Z::'a,Y))) & \
|
|
377 |
\ (! A B C. equal(A::'a,B) --> equal(f1(A::'a,C),f1(B::'a,C))) & \
|
|
378 |
\ (! D F' E. equal(D::'a,E) --> equal(f1(F'::'a,D),f1(F'::'a,E))) & \
|
|
379 |
\ (there_exists(compos(a::'a,b))) & \
|
|
380 |
\ (! Y X Z. equal(compos(compos(a::'a,b),X),Y) & equal(compos(compos(a::'a,b),Z),Y) --> equal(X::'a,Z)) & \
|
|
381 |
\ (there_exists(compos(b::'a,h))) & \
|
|
382 |
\ (equal(compos(b::'a,h),compos(b::'a,g))) & \
|
|
383 |
\ (~equal(h::'a,g)) --> False",
|
|
384 |
meson_tac);
|
|
385 |
|
|
386 |
(*245 inferences so far. Searching to depth 7. 1.0 secs*)
|
|
387 |
val CAT003_3 = prove
|
|
388 |
("(! X. equal(X::'a,X)) & \
|
|
389 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
390 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
391 |
\ (! Y X. equivalent(X::'a,Y) --> there_exists(X)) & \
|
|
392 |
\ (! X Y. equivalent(X::'a,Y) --> equal(X::'a,Y)) & \
|
|
393 |
\ (! X Y. there_exists(X) & equal(X::'a,Y) --> equivalent(X::'a,Y)) & \
|
|
394 |
\ (! X. there_exists(domain(X)) --> there_exists(X)) & \
|
|
395 |
\ (! X. there_exists(codomain(X)) --> there_exists(X)) & \
|
|
396 |
\ (! Y X. there_exists(compos(X::'a,Y)) --> there_exists(domain(X))) & \
|
|
397 |
\ (! X Y. there_exists(compos(X::'a,Y)) --> equal(domain(X),codomain(Y))) & \
|
|
398 |
\ (! X Y. there_exists(domain(X)) & equal(domain(X),codomain(Y)) --> there_exists(compos(X::'a,Y))) & \
|
|
399 |
\ (! X Y Z. equal(compos(X::'a,compos(Y::'a,Z)),compos(compos(X::'a,Y),Z))) & \
|
|
400 |
\ (! X. equal(compos(X::'a,domain(X)),X)) & \
|
|
401 |
\ (! X. equal(compos(codomain(X),X),X)) & \
|
|
402 |
\ (! X Y. equivalent(X::'a,Y) --> there_exists(Y)) & \
|
|
403 |
\ (! X Y. there_exists(X) & there_exists(Y) & equal(X::'a,Y) --> equivalent(X::'a,Y)) & \
|
|
404 |
\ (! Y X. there_exists(compos(X::'a,Y)) --> there_exists(codomain(X))) & \
|
|
405 |
\ (! X Y. there_exists(f1(X::'a,Y)) | equal(X::'a,Y)) & \
|
|
406 |
\ (! X Y. equal(X::'a,f1(X::'a,Y)) | equal(Y::'a,f1(X::'a,Y)) | equal(X::'a,Y)) & \
|
|
407 |
\ (! X Y. equal(X::'a,f1(X::'a,Y)) & equal(Y::'a,f1(X::'a,Y)) --> equal(X::'a,Y)) & \
|
|
408 |
\ (! X Y. equal(X::'a,Y) & there_exists(X) --> there_exists(Y)) & \
|
|
409 |
\ (! X Y Z. equal(X::'a,Y) & equivalent(X::'a,Z) --> equivalent(Y::'a,Z)) & \
|
|
410 |
\ (! X Z Y. equal(X::'a,Y) & equivalent(Z::'a,X) --> equivalent(Z::'a,Y)) & \
|
|
411 |
\ (! X Y. equal(X::'a,Y) --> equal(domain(X),domain(Y))) & \
|
|
412 |
\ (! X Y. equal(X::'a,Y) --> equal(codomain(X),codomain(Y))) & \
|
|
413 |
\ (! X Y Z. equal(X::'a,Y) --> equal(compos(X::'a,Z),compos(Y::'a,Z))) & \
|
|
414 |
\ (! X Z Y. equal(X::'a,Y) --> equal(compos(Z::'a,X),compos(Z::'a,Y))) & \
|
|
415 |
\ (! A B C. equal(A::'a,B) --> equal(f1(A::'a,C),f1(B::'a,C))) & \
|
|
416 |
\ (! D F' E. equal(D::'a,E) --> equal(f1(F'::'a,D),f1(F'::'a,E))) & \
|
|
417 |
\ (there_exists(compos(a::'a,b))) & \
|
|
418 |
\ (! Y X Z. equal(compos(X::'a,compos(a::'a,b)),Y) & equal(compos(Z::'a,compos(a::'a,b)),Y) --> equal(X::'a,Z)) & \
|
|
419 |
\ (there_exists(h)) & \
|
|
420 |
\ (equal(compos(h::'a,a),compos(g::'a,a))) & \
|
|
421 |
\ (~equal(g::'a,h)) --> False",
|
|
422 |
meson_tac);
|
|
423 |
|
|
424 |
(*54288 inferences so far. Searching to depth 14. 118.0 secs*)
|
|
425 |
val CAT005_1 = prove_hard
|
|
426 |
("(! X. equal(X::'a,X)) & \
|
|
427 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
428 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
429 |
\ (! X Y. defined(X::'a,Y) --> product(X::'a,Y,compos(X::'a,Y))) & \
|
|
430 |
\ (! Z X Y. product(X::'a,Y,Z) --> defined(X::'a,Y)) & \
|
|
431 |
\ (! X Xy Y Z. product(X::'a,Y,Xy) & defined(Xy::'a,Z) --> defined(Y::'a,Z)) & \
|
|
432 |
\ (! Y Xy Z X Yz. product(X::'a,Y,Xy) & product(Y::'a,Z,Yz) & defined(Xy::'a,Z) --> defined(X::'a,Yz)) & \
|
|
433 |
\ (! Xy Y Z X Yz Xyz. product(X::'a,Y,Xy) & product(Xy::'a,Z,Xyz) & product(Y::'a,Z,Yz) --> product(X::'a,Yz,Xyz)) & \
|
|
434 |
\ (! Z Yz X Y. product(Y::'a,Z,Yz) & defined(X::'a,Yz) --> defined(X::'a,Y)) & \
|
|
435 |
\ (! Y X Yz Xy Z. product(Y::'a,Z,Yz) & product(X::'a,Y,Xy) & defined(X::'a,Yz) --> defined(Xy::'a,Z)) & \
|
|
436 |
\ (! Yz X Y Xy Z Xyz. product(Y::'a,Z,Yz) & product(X::'a,Yz,Xyz) & product(X::'a,Y,Xy) --> product(Xy::'a,Z,Xyz)) & \
|
|
437 |
\ (! Y X Z. defined(X::'a,Y) & defined(Y::'a,Z) & identity_map(Y) --> defined(X::'a,Z)) & \
|
|
438 |
\ (! X. identity_map(domain(X))) & \
|
|
439 |
\ (! X. identity_map(codomain(X))) & \
|
|
440 |
\ (! X. defined(X::'a,domain(X))) & \
|
|
441 |
\ (! X. defined(codomain(X),X)) & \
|
|
442 |
\ (! X. product(X::'a,domain(X),X)) & \
|
|
443 |
\ (! X. product(codomain(X),X,X)) & \
|
|
444 |
\ (! X Y. defined(X::'a,Y) & identity_map(X) --> product(X::'a,Y,Y)) & \
|
|
445 |
\ (! Y X. defined(X::'a,Y) & identity_map(Y) --> product(X::'a,Y,X)) & \
|
|
446 |
\ (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) & \
|
|
447 |
\ (! X Y Z W. equal(X::'a,Y) & product(X::'a,Z,W) --> product(Y::'a,Z,W)) & \
|
|
448 |
\ (! X Z Y W. equal(X::'a,Y) & product(Z::'a,X,W) --> product(Z::'a,Y,W)) & \
|
|
449 |
\ (! X Z W Y. equal(X::'a,Y) & product(Z::'a,W,X) --> product(Z::'a,W,Y)) & \
|
|
450 |
\ (! X Y. equal(X::'a,Y) --> equal(domain(X),domain(Y))) & \
|
|
451 |
\ (! X Y. equal(X::'a,Y) --> equal(codomain(X),codomain(Y))) & \
|
|
452 |
\ (! X Y. equal(X::'a,Y) & identity_map(X) --> identity_map(Y)) & \
|
|
453 |
\ (! X Y Z. equal(X::'a,Y) & defined(X::'a,Z) --> defined(Y::'a,Z)) & \
|
|
454 |
\ (! X Z Y. equal(X::'a,Y) & defined(Z::'a,X) --> defined(Z::'a,Y)) & \
|
|
455 |
\ (! X Z Y. equal(X::'a,Y) --> equal(compos(Z::'a,X),compos(Z::'a,Y))) & \
|
|
456 |
\ (! X Y Z. equal(X::'a,Y) --> equal(compos(X::'a,Z),compos(Y::'a,Z))) & \
|
|
457 |
\ (defined(a::'a,d)) & \
|
|
458 |
\ (identity_map(d)) & \
|
|
459 |
\ (~equal(domain(a),d)) --> False",
|
|
460 |
meson_tac);
|
|
461 |
|
|
462 |
|
|
463 |
(*1728 inferences so far. Searching to depth 10. 5.8 secs*)
|
|
464 |
val CAT007_1 = prove_hard
|
|
465 |
("(! X. equal(X::'a,X)) & \
|
|
466 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
467 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
468 |
\ (! X Y. defined(X::'a,Y) --> product(X::'a,Y,compos(X::'a,Y))) & \
|
|
469 |
\ (! Z X Y. product(X::'a,Y,Z) --> defined(X::'a,Y)) & \
|
|
470 |
\ (! X Xy Y Z. product(X::'a,Y,Xy) & defined(Xy::'a,Z) --> defined(Y::'a,Z)) & \
|
|
471 |
\ (! Y Xy Z X Yz. product(X::'a,Y,Xy) & product(Y::'a,Z,Yz) & defined(Xy::'a,Z) --> defined(X::'a,Yz)) & \
|
|
472 |
\ (! Xy Y Z X Yz Xyz. product(X::'a,Y,Xy) & product(Xy::'a,Z,Xyz) & product(Y::'a,Z,Yz) --> product(X::'a,Yz,Xyz)) & \
|
|
473 |
\ (! Z Yz X Y. product(Y::'a,Z,Yz) & defined(X::'a,Yz) --> defined(X::'a,Y)) & \
|
|
474 |
\ (! Y X Yz Xy Z. product(Y::'a,Z,Yz) & product(X::'a,Y,Xy) & defined(X::'a,Yz) --> defined(Xy::'a,Z)) & \
|
|
475 |
\ (! Yz X Y Xy Z Xyz. product(Y::'a,Z,Yz) & product(X::'a,Yz,Xyz) & product(X::'a,Y,Xy) --> product(Xy::'a,Z,Xyz)) & \
|
|
476 |
\ (! Y X Z. defined(X::'a,Y) & defined(Y::'a,Z) & identity_map(Y) --> defined(X::'a,Z)) & \
|
|
477 |
\ (! X. identity_map(domain(X))) & \
|
|
478 |
\ (! X. identity_map(codomain(X))) & \
|
|
479 |
\ (! X. defined(X::'a,domain(X))) & \
|
|
480 |
\ (! X. defined(codomain(X),X)) & \
|
|
481 |
\ (! X. product(X::'a,domain(X),X)) & \
|
|
482 |
\ (! X. product(codomain(X),X,X)) & \
|
|
483 |
\ (! X Y. defined(X::'a,Y) & identity_map(X) --> product(X::'a,Y,Y)) & \
|
|
484 |
\ (! Y X. defined(X::'a,Y) & identity_map(Y) --> product(X::'a,Y,X)) & \
|
|
485 |
\ (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) & \
|
|
486 |
\ (! X Y Z W. equal(X::'a,Y) & product(X::'a,Z,W) --> product(Y::'a,Z,W)) & \
|
|
487 |
\ (! X Z Y W. equal(X::'a,Y) & product(Z::'a,X,W) --> product(Z::'a,Y,W)) & \
|
|
488 |
\ (! X Z W Y. equal(X::'a,Y) & product(Z::'a,W,X) --> product(Z::'a,W,Y)) & \
|
|
489 |
\ (! X Y. equal(X::'a,Y) --> equal(domain(X),domain(Y))) & \
|
|
490 |
\ (! X Y. equal(X::'a,Y) --> equal(codomain(X),codomain(Y))) & \
|
|
491 |
\ (! X Y. equal(X::'a,Y) & identity_map(X) --> identity_map(Y)) & \
|
|
492 |
\ (! X Y Z. equal(X::'a,Y) & defined(X::'a,Z) --> defined(Y::'a,Z)) & \
|
|
493 |
\ (! X Z Y. equal(X::'a,Y) & defined(Z::'a,X) --> defined(Z::'a,Y)) & \
|
|
494 |
\ (! X Z Y. equal(X::'a,Y) --> equal(compos(Z::'a,X),compos(Z::'a,Y))) & \
|
|
495 |
\ (! X Y Z. equal(X::'a,Y) --> equal(compos(X::'a,Z),compos(Y::'a,Z))) & \
|
|
496 |
\ (equal(domain(a),codomain(b))) & \
|
|
497 |
\ (~defined(a::'a,b)) --> False",
|
|
498 |
meson_tac);
|
|
499 |
|
|
500 |
(*82895 inferences so far. Searching to depth 13. 355 secs*)
|
|
501 |
val CAT018_1 = prove_hard
|
|
502 |
("(! X. equal(X::'a,X)) & \
|
|
503 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
504 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
505 |
\ (! X Y. defined(X::'a,Y) --> product(X::'a,Y,compos(X::'a,Y))) & \
|
|
506 |
\ (! Z X Y. product(X::'a,Y,Z) --> defined(X::'a,Y)) & \
|
|
507 |
\ (! X Xy Y Z. product(X::'a,Y,Xy) & defined(Xy::'a,Z) --> defined(Y::'a,Z)) & \
|
|
508 |
\ (! Y Xy Z X Yz. product(X::'a,Y,Xy) & product(Y::'a,Z,Yz) & defined(Xy::'a,Z) --> defined(X::'a,Yz)) & \
|
|
509 |
\ (! Xy Y Z X Yz Xyz. product(X::'a,Y,Xy) & product(Xy::'a,Z,Xyz) & product(Y::'a,Z,Yz) --> product(X::'a,Yz,Xyz)) & \
|
|
510 |
\ (! Z Yz X Y. product(Y::'a,Z,Yz) & defined(X::'a,Yz) --> defined(X::'a,Y)) & \
|
|
511 |
\ (! Y X Yz Xy Z. product(Y::'a,Z,Yz) & product(X::'a,Y,Xy) & defined(X::'a,Yz) --> defined(Xy::'a,Z)) & \
|
|
512 |
\ (! Yz X Y Xy Z Xyz. product(Y::'a,Z,Yz) & product(X::'a,Yz,Xyz) & product(X::'a,Y,Xy) --> product(Xy::'a,Z,Xyz)) & \
|
|
513 |
\ (! Y X Z. defined(X::'a,Y) & defined(Y::'a,Z) & identity_map(Y) --> defined(X::'a,Z)) & \
|
|
514 |
\ (! X. identity_map(domain(X))) & \
|
|
515 |
\ (! X. identity_map(codomain(X))) & \
|
|
516 |
\ (! X. defined(X::'a,domain(X))) & \
|
|
517 |
\ (! X. defined(codomain(X),X)) & \
|
|
518 |
\ (! X. product(X::'a,domain(X),X)) & \
|
|
519 |
\ (! X. product(codomain(X),X,X)) & \
|
|
520 |
\ (! X Y. defined(X::'a,Y) & identity_map(X) --> product(X::'a,Y,Y)) & \
|
|
521 |
\ (! Y X. defined(X::'a,Y) & identity_map(Y) --> product(X::'a,Y,X)) & \
|
|
522 |
\ (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) & \
|
|
523 |
\ (! X Y Z W. equal(X::'a,Y) & product(X::'a,Z,W) --> product(Y::'a,Z,W)) & \
|
|
524 |
\ (! X Z Y W. equal(X::'a,Y) & product(Z::'a,X,W) --> product(Z::'a,Y,W)) & \
|
|
525 |
\ (! X Z W Y. equal(X::'a,Y) & product(Z::'a,W,X) --> product(Z::'a,W,Y)) & \
|
|
526 |
\ (! X Y. equal(X::'a,Y) --> equal(domain(X),domain(Y))) & \
|
|
527 |
\ (! X Y. equal(X::'a,Y) --> equal(codomain(X),codomain(Y))) & \
|
|
528 |
\ (! X Y. equal(X::'a,Y) & identity_map(X) --> identity_map(Y)) & \
|
|
529 |
\ (! X Y Z. equal(X::'a,Y) & defined(X::'a,Z) --> defined(Y::'a,Z)) & \
|
|
530 |
\ (! X Z Y. equal(X::'a,Y) & defined(Z::'a,X) --> defined(Z::'a,Y)) & \
|
|
531 |
\ (! X Z Y. equal(X::'a,Y) --> equal(compos(Z::'a,X),compos(Z::'a,Y))) & \
|
|
532 |
\ (! X Y Z. equal(X::'a,Y) --> equal(compos(X::'a,Z),compos(Y::'a,Z))) & \
|
|
533 |
\ (defined(a::'a,b)) & \
|
|
534 |
\ (defined(b::'a,c)) & \
|
|
535 |
\ (~defined(a::'a,compos(b::'a,c))) --> False",
|
|
536 |
meson_tac);
|
|
537 |
|
|
538 |
(*1118 inferences so far. Searching to depth 8. 2.3 secs*)
|
|
539 |
val COL001_2 = prove
|
|
540 |
("(! X. equal(X::'a,X)) & \
|
|
541 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
542 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
543 |
\ (! X Y Z. equal(apply(apply(apply(s::'a,X),Y),Z),apply(apply(X::'a,Z),apply(Y::'a,Z)))) & \
|
|
544 |
\ (! Y X. equal(apply(apply(k::'a,X),Y),X)) & \
|
|
545 |
\ (! X Y Z. equal(apply(apply(apply(b::'a,X),Y),Z),apply(X::'a,apply(Y::'a,Z)))) & \
|
|
546 |
\ (! X. equal(apply(i::'a,X),X)) & \
|
|
547 |
\ (! A B C. equal(A::'a,B) --> equal(apply(A::'a,C),apply(B::'a,C))) & \
|
|
548 |
\ (! D F' E. equal(D::'a,E) --> equal(apply(F'::'a,D),apply(F'::'a,E))) & \
|
|
549 |
\ (! X. equal(apply(apply(apply(s::'a,apply(b::'a,X)),i),apply(apply(s::'a,apply(b::'a,X)),i)),apply(x::'a,apply(apply(apply(s::'a,apply(b::'a,X)),i),apply(apply(s::'a,apply(b::'a,X)),i))))) & \
|
|
550 |
\ (! Y. ~equal(Y::'a,apply(combinator::'a,Y))) --> False",
|
|
551 |
meson_tac);
|
|
552 |
|
|
553 |
(*500 inferences so far. Searching to depth 8. 0.9 secs*)
|
|
554 |
val COL023_1 = prove
|
|
555 |
("(! X. equal(X::'a,X)) & \
|
|
556 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
557 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
558 |
\ (! X Y Z. equal(apply(apply(apply(b::'a,X),Y),Z),apply(X::'a,apply(Y::'a,Z)))) & \
|
|
559 |
\ (! X Y Z. equal(apply(apply(apply(n::'a,X),Y),Z),apply(apply(apply(X::'a,Z),Y),Z))) & \
|
|
560 |
\ (! A B C. equal(A::'a,B) --> equal(apply(A::'a,C),apply(B::'a,C))) & \
|
|
561 |
\ (! D F' E. equal(D::'a,E) --> equal(apply(F'::'a,D),apply(F'::'a,E))) & \
|
|
562 |
\ (! Y. ~equal(Y::'a,apply(combinator::'a,Y))) --> False",
|
|
563 |
meson_tac);
|
|
564 |
|
|
565 |
(*3018 inferences so far. Searching to depth 10. 4.3 secs*)
|
|
566 |
val COL032_1 = prove_hard
|
|
567 |
("(! X. equal(X::'a,X)) & \
|
|
568 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
569 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
570 |
\ (! X. equal(apply(m::'a,X),apply(X::'a,X))) & \
|
|
571 |
\ (! Y X Z. equal(apply(apply(apply(q::'a,X),Y),Z),apply(Y::'a,apply(X::'a,Z)))) & \
|
|
572 |
\ (! A B C. equal(A::'a,B) --> equal(apply(A::'a,C),apply(B::'a,C))) & \
|
|
573 |
\ (! D F' E. equal(D::'a,E) --> equal(apply(F'::'a,D),apply(F'::'a,E))) & \
|
|
574 |
\ (! G H. equal(G::'a,H) --> equal(f(G),f(H))) & \
|
|
575 |
\ (! Y. ~equal(apply(Y::'a,f(Y)),apply(f(Y),apply(Y::'a,f(Y))))) --> False",
|
|
576 |
meson_tac);
|
|
577 |
|
|
578 |
(*381878 inferences so far. Searching to depth 13. 670.4 secs*)
|
|
579 |
val COL052_2 = prove_hard
|
|
580 |
("(! X. equal(X::'a,X)) & \
|
|
581 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
582 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
583 |
\ (! X Y W. equal(response(compos(X::'a,Y),W),response(X::'a,response(Y::'a,W)))) & \
|
|
584 |
\ (! X Y. agreeable(X) --> equal(response(X::'a,common_bird(Y)),response(Y::'a,common_bird(Y)))) & \
|
|
585 |
\ (! Z X. equal(response(X::'a,Z),response(compatible(X),Z)) --> agreeable(X)) & \
|
|
586 |
\ (! A B. equal(A::'a,B) --> equal(common_bird(A),common_bird(B))) & \
|
|
587 |
\ (! C D. equal(C::'a,D) --> equal(compatible(C),compatible(D))) & \
|
|
588 |
\ (! Q R. equal(Q::'a,R) & agreeable(Q) --> agreeable(R)) & \
|
|
589 |
\ (! A B C. equal(A::'a,B) --> equal(compos(A::'a,C),compos(B::'a,C))) & \
|
|
590 |
\ (! D F' E. equal(D::'a,E) --> equal(compos(F'::'a,D),compos(F'::'a,E))) & \
|
|
591 |
\ (! G H I'. equal(G::'a,H) --> equal(response(G::'a,I'),response(H::'a,I'))) & \
|
|
592 |
\ (! J L K'. equal(J::'a,K') --> equal(response(L::'a,J),response(L::'a,K'))) & \
|
|
593 |
\ (agreeable(c)) & \
|
|
594 |
\ (~agreeable(a)) & \
|
|
595 |
\ (equal(c::'a,compos(a::'a,b))) --> False",
|
|
596 |
meson_tac);
|
|
597 |
|
|
598 |
(*13201 inferences so far. Searching to depth 11. 31.9 secs*)
|
|
599 |
val COL075_2 = prove_hard
|
|
600 |
("(! X. equal(X::'a,X)) & \
|
|
601 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
602 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
603 |
\ (! Y X. equal(apply(apply(k::'a,X),Y),X)) & \
|
|
604 |
\ (! X Y Z. equal(apply(apply(apply(abstraction::'a,X),Y),Z),apply(apply(X::'a,apply(k::'a,Z)),apply(Y::'a,Z)))) & \
|
|
605 |
\ (! D E F'. equal(D::'a,E) --> equal(apply(D::'a,F'),apply(E::'a,F'))) & \
|
|
606 |
\ (! G I' H. equal(G::'a,H) --> equal(apply(I'::'a,G),apply(I'::'a,H))) & \
|
|
607 |
\ (! A B. equal(A::'a,B) --> equal(b(A),b(B))) & \
|
|
608 |
\ (! C D. equal(C::'a,D) --> equal(c(C),c(D))) & \
|
|
609 |
\ (! Y. ~equal(apply(apply(Y::'a,b(Y)),c(Y)),apply(b(Y),b(Y)))) --> False",
|
|
610 |
meson_tac);
|
|
611 |
|
|
612 |
(*33 inferences so far. Searching to depth 7. 0.1 secs*)
|
|
613 |
val COM001_1 = prove
|
|
614 |
("(! Goal_state Start_state. follows(Goal_state::'a,Start_state) --> succeeds(Goal_state::'a,Start_state)) & \
|
|
615 |
\ (! Goal_state Intermediate_state Start_state. succeeds(Goal_state::'a,Intermediate_state) & succeeds(Intermediate_state::'a,Start_state) --> succeeds(Goal_state::'a,Start_state)) & \
|
|
616 |
\ (! Start_state Label Goal_state. has(Start_state::'a,goto(Label)) & labels(Label::'a,Goal_state) --> succeeds(Goal_state::'a,Start_state)) & \
|
|
617 |
\ (! Start_state Condition Goal_state. has(Start_state::'a,ifthen(Condition::'a,Goal_state)) --> succeeds(Goal_state::'a,Start_state)) & \
|
|
618 |
\ (labels(loop::'a,p3)) & \
|
|
619 |
\ (has(p3::'a,ifthen(equal(register_j::'a,n),p4))) & \
|
|
620 |
\ (has(p4::'a,goto(out))) & \
|
|
621 |
\ (follows(p5::'a,p4)) & \
|
|
622 |
\ (follows(p8::'a,p3)) & \
|
|
623 |
\ (has(p8::'a,goto(loop))) & \
|
|
624 |
\ (~succeeds(p3::'a,p3)) --> False",
|
|
625 |
meson_tac);
|
|
626 |
|
|
627 |
(*533 inferences so far. Searching to depth 13. 0.3 secs*)
|
|
628 |
val COM002_1 = prove
|
|
629 |
("(! Goal_state Start_state. follows(Goal_state::'a,Start_state) --> succeeds(Goal_state::'a,Start_state)) & \
|
|
630 |
\ (! Goal_state Intermediate_state Start_state. succeeds(Goal_state::'a,Intermediate_state) & succeeds(Intermediate_state::'a,Start_state) --> succeeds(Goal_state::'a,Start_state)) & \
|
|
631 |
\ (! Start_state Label Goal_state. has(Start_state::'a,goto(Label)) & labels(Label::'a,Goal_state) --> succeeds(Goal_state::'a,Start_state)) & \
|
|
632 |
\ (! Start_state Condition Goal_state. has(Start_state::'a,ifthen(Condition::'a,Goal_state)) --> succeeds(Goal_state::'a,Start_state)) & \
|
|
633 |
\ (has(p1::'a,assign(register_j::'a,num0))) & \
|
|
634 |
\ (follows(p2::'a,p1)) & \
|
|
635 |
\ (has(p2::'a,assign(register_k::'a,num1))) & \
|
|
636 |
\ (labels(loop::'a,p3)) & \
|
|
637 |
\ (follows(p3::'a,p2)) & \
|
|
638 |
\ (has(p3::'a,ifthen(equal(register_j::'a,n),p4))) & \
|
|
639 |
\ (has(p4::'a,goto(out))) & \
|
|
640 |
\ (follows(p5::'a,p4)) & \
|
|
641 |
\ (follows(p6::'a,p3)) & \
|
|
642 |
\ (has(p6::'a,assign(register_k::'a,times(num2::'a,register_k)))) & \
|
|
643 |
\ (follows(p7::'a,p6)) & \
|
|
644 |
\ (has(p7::'a,assign(register_j::'a,plus(register_j::'a,num1)))) & \
|
|
645 |
\ (follows(p8::'a,p7)) & \
|
|
646 |
\ (has(p8::'a,goto(loop))) & \
|
|
647 |
\ (~succeeds(p3::'a,p3)) --> False",
|
|
648 |
meson_tac);
|
|
649 |
|
|
650 |
(*4821 inferences so far. Searching to depth 14. 1.3 secs*)
|
|
651 |
val COM002_2 = prove
|
|
652 |
("(! Goal_state Start_state. ~(fails(Goal_state::'a,Start_state) & follows(Goal_state::'a,Start_state))) & \
|
|
653 |
\ (! Goal_state Intermediate_state Start_state. fails(Goal_state::'a,Start_state) --> fails(Goal_state::'a,Intermediate_state) | fails(Intermediate_state::'a,Start_state)) & \
|
|
654 |
\ (! Start_state Label Goal_state. ~(fails(Goal_state::'a,Start_state) & has(Start_state::'a,goto(Label)) & labels(Label::'a,Goal_state))) & \
|
|
655 |
\ (! Start_state Condition Goal_state. ~(fails(Goal_state::'a,Start_state) & has(Start_state::'a,ifthen(Condition::'a,Goal_state)))) & \
|
|
656 |
\ (has(p1::'a,assign(register_j::'a,num0))) & \
|
|
657 |
\ (follows(p2::'a,p1)) & \
|
|
658 |
\ (has(p2::'a,assign(register_k::'a,num1))) & \
|
|
659 |
\ (labels(loop::'a,p3)) & \
|
|
660 |
\ (follows(p3::'a,p2)) & \
|
|
661 |
\ (has(p3::'a,ifthen(equal(register_j::'a,n),p4))) & \
|
|
662 |
\ (has(p4::'a,goto(out))) & \
|
|
663 |
\ (follows(p5::'a,p4)) & \
|
|
664 |
\ (follows(p6::'a,p3)) & \
|
|
665 |
\ (has(p6::'a,assign(register_k::'a,times(num2::'a,register_k)))) & \
|
|
666 |
\ (follows(p7::'a,p6)) & \
|
|
667 |
\ (has(p7::'a,assign(register_j::'a,plus(register_j::'a,num1)))) & \
|
|
668 |
\ (follows(p8::'a,p7)) & \
|
|
669 |
\ (has(p8::'a,goto(loop))) & \
|
|
670 |
\ (fails(p3::'a,p3)) --> False",
|
|
671 |
meson_tac);
|
|
672 |
|
|
673 |
(*98 inferences so far. Searching to depth 10. 1.1 secs*)
|
|
674 |
val COM003_2 = prove
|
|
675 |
("(! X Y Z. program_decides(X) & program(Y) --> decides(X::'a,Y,Z)) & \
|
|
676 |
\ (! X. program_decides(X) | program(f2(X))) & \
|
|
677 |
\ (! X. decides(X::'a,f2(X),f1(X)) --> program_decides(X)) & \
|
|
678 |
\ (! X. program_program_decides(X) --> program(X)) & \
|
|
679 |
\ (! X. program_program_decides(X) --> program_decides(X)) & \
|
|
680 |
\ (! X. program(X) & program_decides(X) --> program_program_decides(X)) & \
|
|
681 |
\ (! X. algorithm_program_decides(X) --> algorithm(X)) & \
|
|
682 |
\ (! X. algorithm_program_decides(X) --> program_decides(X)) & \
|
|
683 |
\ (! X. algorithm(X) & program_decides(X) --> algorithm_program_decides(X)) & \
|
|
684 |
\ (! Y X. program_halts2(X::'a,Y) --> program(X)) & \
|
|
685 |
\ (! X Y. program_halts2(X::'a,Y) --> halts2(X::'a,Y)) & \
|
|
686 |
\ (! X Y. program(X) & halts2(X::'a,Y) --> program_halts2(X::'a,Y)) & \
|
|
687 |
\ (! W X Y Z. halts3_outputs(X::'a,Y,Z,W) --> halts3(X::'a,Y,Z)) & \
|
|
688 |
\ (! Y Z X W. halts3_outputs(X::'a,Y,Z,W) --> outputs(X::'a,W)) & \
|
|
689 |
\ (! Y Z X W. halts3(X::'a,Y,Z) & outputs(X::'a,W) --> halts3_outputs(X::'a,Y,Z,W)) & \
|
|
690 |
\ (! Y X. program_not_halts2(X::'a,Y) --> program(X)) & \
|
|
691 |
\ (! X Y. ~(program_not_halts2(X::'a,Y) & halts2(X::'a,Y))) & \
|
|
692 |
\ (! X Y. program(X) --> program_not_halts2(X::'a,Y) | halts2(X::'a,Y)) & \
|
|
693 |
\ (! W X Y. halts2_outputs(X::'a,Y,W) --> halts2(X::'a,Y)) & \
|
|
694 |
\ (! Y X W. halts2_outputs(X::'a,Y,W) --> outputs(X::'a,W)) & \
|
|
695 |
\ (! Y X W. halts2(X::'a,Y) & outputs(X::'a,W) --> halts2_outputs(X::'a,Y,W)) & \
|
|
696 |
\ (! X W Y Z. program_halts2_halts3_outputs(X::'a,Y,Z,W) --> program_halts2(Y::'a,Z)) & \
|
|
697 |
\ (! X Y Z W. program_halts2_halts3_outputs(X::'a,Y,Z,W) --> halts3_outputs(X::'a,Y,Z,W)) & \
|
|
698 |
\ (! X Y Z W. program_halts2(Y::'a,Z) & halts3_outputs(X::'a,Y,Z,W) --> program_halts2_halts3_outputs(X::'a,Y,Z,W)) & \
|
|
699 |
\ (! X W Y Z. program_not_halts2_halts3_outputs(X::'a,Y,Z,W) --> program_not_halts2(Y::'a,Z)) & \
|
|
700 |
\ (! X Y Z W. program_not_halts2_halts3_outputs(X::'a,Y,Z,W) --> halts3_outputs(X::'a,Y,Z,W)) & \
|
|
701 |
\ (! X Y Z W. program_not_halts2(Y::'a,Z) & halts3_outputs(X::'a,Y,Z,W) --> program_not_halts2_halts3_outputs(X::'a,Y,Z,W)) & \
|
|
702 |
\ (! X W Y. program_halts2_halts2_outputs(X::'a,Y,W) --> program_halts2(Y::'a,Y)) & \
|
|
703 |
\ (! X Y W. program_halts2_halts2_outputs(X::'a,Y,W) --> halts2_outputs(X::'a,Y,W)) & \
|
|
704 |
\ (! X Y W. program_halts2(Y::'a,Y) & halts2_outputs(X::'a,Y,W) --> program_halts2_halts2_outputs(X::'a,Y,W)) & \
|
|
705 |
\ (! X W Y. program_not_halts2_halts2_outputs(X::'a,Y,W) --> program_not_halts2(Y::'a,Y)) & \
|
|
706 |
\ (! X Y W. program_not_halts2_halts2_outputs(X::'a,Y,W) --> halts2_outputs(X::'a,Y,W)) & \
|
|
707 |
\ (! X Y W. program_not_halts2(Y::'a,Y) & halts2_outputs(X::'a,Y,W) --> program_not_halts2_halts2_outputs(X::'a,Y,W)) & \
|
|
708 |
\ (! X. algorithm_program_decides(X) --> program_program_decides(c1)) & \
|
|
709 |
\ (! W Y Z. program_program_decides(W) --> program_halts2_halts3_outputs(W::'a,Y,Z,good)) & \
|
|
710 |
\ (! W Y Z. program_program_decides(W) --> program_not_halts2_halts3_outputs(W::'a,Y,Z,bad)) & \
|
|
711 |
\ (! W. program(W) & program_halts2_halts3_outputs(W::'a,f3(W),f3(W),good) & program_not_halts2_halts3_outputs(W::'a,f3(W),f3(W),bad) --> program(c2)) & \
|
|
712 |
\ (! W Y. program(W) & program_halts2_halts3_outputs(W::'a,f3(W),f3(W),good) & program_not_halts2_halts3_outputs(W::'a,f3(W),f3(W),bad) --> program_halts2_halts2_outputs(c2::'a,Y,good)) & \
|
|
713 |
\ (! W Y. program(W) & program_halts2_halts3_outputs(W::'a,f3(W),f3(W),good) & program_not_halts2_halts3_outputs(W::'a,f3(W),f3(W),bad) --> program_not_halts2_halts2_outputs(c2::'a,Y,bad)) & \
|
|
714 |
\ (! V. program(V) & program_halts2_halts2_outputs(V::'a,f4(V),good) & program_not_halts2_halts2_outputs(V::'a,f4(V),bad) --> program(c3)) & \
|
|
715 |
\ (! V Y. program(V) & program_halts2_halts2_outputs(V::'a,f4(V),good) & program_not_halts2_halts2_outputs(V::'a,f4(V),bad) & program_halts2(Y::'a,Y) --> halts2(c3::'a,Y)) & \
|
|
716 |
\ (! V Y. program(V) & program_halts2_halts2_outputs(V::'a,f4(V),good) & program_not_halts2_halts2_outputs(V::'a,f4(V),bad) --> program_not_halts2_halts2_outputs(c3::'a,Y,bad)) & \
|
|
717 |
\ (algorithm_program_decides(c4)) --> False",
|
|
718 |
meson_tac);
|
|
719 |
|
|
720 |
(****************SLOW
|
|
721 |
2100398 inferences so far. Searching to depth 12. No proof after 30 mins.
|
|
722 |
val COM004_1 = prove
|
|
723 |
("(! X. equal(X::'a,X)) & \
|
|
724 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
725 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
726 |
\ (! C D P Q X Y. failure_node(X::'a,or(C::'a,P)) & failure_node(Y::'a,or(D::'a,Q)) & contradictory(P::'a,Q) & siblings(X::'a,Y) --> failure_node(parent_of(X::'a,Y),or(C::'a,D))) & \
|
|
727 |
\ (! X. contradictory(negate(X),X)) & \
|
|
728 |
\ (! X. contradictory(X::'a,negate(X))) & \
|
|
729 |
\ (! X. siblings(left_child_of(X),right_child_of(X))) & \
|
|
730 |
\ (! D E. equal(D::'a,E) --> equal(left_child_of(D),left_child_of(E))) & \
|
|
731 |
\ (! F' G. equal(F'::'a,G) --> equal(negate(F'),negate(G))) & \
|
|
732 |
\ (! H I' J. equal(H::'a,I') --> equal(or(H::'a,J),or(I'::'a,J))) & \
|
|
733 |
\ (! K' M L. equal(K'::'a,L) --> equal(or(M::'a,K'),or(M::'a,L))) & \
|
|
734 |
\ (! N O_ P. equal(N::'a,O_) --> equal(parent_of(N::'a,P),parent_of(O_::'a,P))) & \
|
|
735 |
\ (! Q S' R. equal(Q::'a,R) --> equal(parent_of(S'::'a,Q),parent_of(S'::'a,R))) & \
|
|
736 |
\ (! T' U. equal(T'::'a,U) --> equal(right_child_of(T'),right_child_of(U))) & \
|
|
737 |
\ (! V W X. equal(V::'a,W) & contradictory(V::'a,X) --> contradictory(W::'a,X)) & \
|
|
738 |
\ (! Y A1 Z. equal(Y::'a,Z) & contradictory(A1::'a,Y) --> contradictory(A1::'a,Z)) & \
|
|
739 |
\ (! B1 C1 D1. equal(B1::'a,C1) & failure_node(B1::'a,D1) --> failure_node(C1::'a,D1)) & \
|
|
740 |
\ (! E1 G1 F1. equal(E1::'a,F1) & failure_node(G1::'a,E1) --> failure_node(G1::'a,F1)) & \
|
|
741 |
\ (! H1 I1 J1. equal(H1::'a,I1) & siblings(H1::'a,J1) --> siblings(I1::'a,J1)) & \
|
|
742 |
\ (! K1 M1 L1. equal(K1::'a,L1) & siblings(M1::'a,K1) --> siblings(M1::'a,L1)) & \
|
|
743 |
\ (failure_node(n_left::'a,or(empty::'a,atom))) & \
|
|
744 |
\ (failure_node(n_right::'a,or(empty::'a,negate(atom)))) & \
|
|
745 |
\ (equal(n_left::'a,left_child_of(n))) & \
|
|
746 |
\ (equal(n_right::'a,right_child_of(n))) & \
|
|
747 |
\ (! Z. ~failure_node(Z::'a,or(empty::'a,empty))) --> False",
|
|
748 |
meson_tac);
|
|
749 |
****************)
|
|
750 |
|
|
751 |
(*179 inferences so far. Searching to depth 7. 3.9 secs*)
|
|
752 |
val GEO003_1 = prove_hard
|
|
753 |
("(! X. equal(X::'a,X)) & \
|
|
754 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
755 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
756 |
\ (! X Y. between(X::'a,Y,X) --> equal(X::'a,Y)) & \
|
|
757 |
\ (! V X Y Z. between(X::'a,Y,V) & between(Y::'a,Z,V) --> between(X::'a,Y,Z)) & \
|
|
758 |
\ (! Y X V Z. between(X::'a,Y,Z) & between(X::'a,Y,V) --> equal(X::'a,Y) | between(X::'a,Z,V) | between(X::'a,V,Z)) & \
|
|
759 |
\ (! Y X. equidistant(X::'a,Y,Y,X)) & \
|
|
760 |
\ (! Z X Y. equidistant(X::'a,Y,Z,Z) --> equal(X::'a,Y)) & \
|
|
761 |
\ (! X Y Z V V2 W. equidistant(X::'a,Y,Z,V) & equidistant(X::'a,Y,V2,W) --> equidistant(Z::'a,V,V2,W)) & \
|
|
762 |
\ (! W X Z V Y. between(X::'a,W,V) & between(Y::'a,V,Z) --> between(X::'a,outer_pasch(W::'a,X,Y,Z,V),Y)) & \
|
|
763 |
\ (! W X Y Z V. between(X::'a,W,V) & between(Y::'a,V,Z) --> between(Z::'a,W,outer_pasch(W::'a,X,Y,Z,V))) & \
|
|
764 |
\ (! W X Y Z V. between(X::'a,V,W) & between(Y::'a,V,Z) --> equal(X::'a,V) | between(X::'a,Z,euclid1(W::'a,X,Y,Z,V))) & \
|
|
765 |
\ (! W X Y Z V. between(X::'a,V,W) & between(Y::'a,V,Z) --> equal(X::'a,V) | between(X::'a,Y,euclid2(W::'a,X,Y,Z,V))) & \
|
|
766 |
\ (! W X Y Z V. between(X::'a,V,W) & between(Y::'a,V,Z) --> equal(X::'a,V) | between(euclid1(W::'a,X,Y,Z,V),W,euclid2(W::'a,X,Y,Z,V))) & \
|
|
767 |
\ (! X1 Y1 X Y Z V Z1 V1. equidistant(X::'a,Y,X1,Y1) & equidistant(Y::'a,Z,Y1,Z1) & equidistant(X::'a,V,X1,V1) & equidistant(Y::'a,V,Y1,V1) & between(X::'a,Y,Z) & between(X1::'a,Y1,Z1) --> equal(X::'a,Y) | equidistant(Z::'a,V,Z1,V1)) & \
|
|
768 |
\ (! X Y W V. between(X::'a,Y,extension(X::'a,Y,W,V))) & \
|
|
769 |
\ (! X Y W V. equidistant(Y::'a,extension(X::'a,Y,W,V),W,V)) & \
|
|
770 |
\ (~between(lower_dimension_point_1::'a,lower_dimension_point_2,lower_dimension_point_3)) & \
|
|
771 |
\ (~between(lower_dimension_point_2::'a,lower_dimension_point_3,lower_dimension_point_1)) & \
|
|
772 |
\ (~between(lower_dimension_point_3::'a,lower_dimension_point_1,lower_dimension_point_2)) & \
|
|
773 |
\ (! Z X Y W V. equidistant(X::'a,W,X,V) & equidistant(Y::'a,W,Y,V) & equidistant(Z::'a,W,Z,V) --> between(X::'a,Y,Z) | between(Y::'a,Z,X) | between(Z::'a,X,Y) | equal(W::'a,V)) & \
|
|
774 |
\ (! X Y Z X1 Z1 V. equidistant(V::'a,X,V,X1) & equidistant(V::'a,Z,V,Z1) & between(V::'a,X,Z) & between(X::'a,Y,Z) --> equidistant(V::'a,Y,Z,continuous(X::'a,Y,Z,X1,Z1,V))) & \
|
|
775 |
\ (! X Y Z X1 V Z1. equidistant(V::'a,X,V,X1) & equidistant(V::'a,Z,V,Z1) & between(V::'a,X,Z) & between(X::'a,Y,Z) --> between(X1::'a,continuous(X::'a,Y,Z,X1,Z1,V),Z1)) & \
|
|
776 |
\ (! X Y W Z. equal(X::'a,Y) & between(X::'a,W,Z) --> between(Y::'a,W,Z)) & \
|
|
777 |
\ (! X W Y Z. equal(X::'a,Y) & between(W::'a,X,Z) --> between(W::'a,Y,Z)) & \
|
|
778 |
\ (! X W Z Y. equal(X::'a,Y) & between(W::'a,Z,X) --> between(W::'a,Z,Y)) & \
|
|
779 |
\ (! X Y V W Z. equal(X::'a,Y) & equidistant(X::'a,V,W,Z) --> equidistant(Y::'a,V,W,Z)) & \
|
|
780 |
\ (! X V Y W Z. equal(X::'a,Y) & equidistant(V::'a,X,W,Z) --> equidistant(V::'a,Y,W,Z)) & \
|
|
781 |
\ (! X V W Y Z. equal(X::'a,Y) & equidistant(V::'a,W,X,Z) --> equidistant(V::'a,W,Y,Z)) & \
|
|
782 |
\ (! X V W Z Y. equal(X::'a,Y) & equidistant(V::'a,W,Z,X) --> equidistant(V::'a,W,Z,Y)) & \
|
|
783 |
\ (! X Y V1 V2 V3 V4. equal(X::'a,Y) --> equal(outer_pasch(X::'a,V1,V2,V3,V4),outer_pasch(Y::'a,V1,V2,V3,V4))) & \
|
|
784 |
\ (! X V1 Y V2 V3 V4. equal(X::'a,Y) --> equal(outer_pasch(V1::'a,X,V2,V3,V4),outer_pasch(V1::'a,Y,V2,V3,V4))) & \
|
|
785 |
\ (! X V1 V2 Y V3 V4. equal(X::'a,Y) --> equal(outer_pasch(V1::'a,V2,X,V3,V4),outer_pasch(V1::'a,V2,Y,V3,V4))) & \
|
|
786 |
\ (! X V1 V2 V3 Y V4. equal(X::'a,Y) --> equal(outer_pasch(V1::'a,V2,V3,X,V4),outer_pasch(V1::'a,V2,V3,Y,V4))) & \
|
|
787 |
\ (! X V1 V2 V3 V4 Y. equal(X::'a,Y) --> equal(outer_pasch(V1::'a,V2,V3,V4,X),outer_pasch(V1::'a,V2,V3,V4,Y))) & \
|
|
788 |
\ (! A B C D E F'. equal(A::'a,B) --> equal(euclid1(A::'a,C,D,E,F'),euclid1(B::'a,C,D,E,F'))) & \
|
|
789 |
\ (! G I' H J K' L. equal(G::'a,H) --> equal(euclid1(I'::'a,G,J,K',L),euclid1(I'::'a,H,J,K',L))) & \
|
|
790 |
\ (! M O_ P N Q R. equal(M::'a,N) --> equal(euclid1(O_::'a,P,M,Q,R),euclid1(O_::'a,P,N,Q,R))) & \
|
|
791 |
\ (! S' U V W T' X. equal(S'::'a,T') --> equal(euclid1(U::'a,V,W,S',X),euclid1(U::'a,V,W,T',X))) & \
|
|
792 |
\ (! Y A1 B1 C1 D1 Z. equal(Y::'a,Z) --> equal(euclid1(A1::'a,B1,C1,D1,Y),euclid1(A1::'a,B1,C1,D1,Z))) & \
|
|
793 |
\ (! E1 F1 G1 H1 I1 J1. equal(E1::'a,F1) --> equal(euclid2(E1::'a,G1,H1,I1,J1),euclid2(F1::'a,G1,H1,I1,J1))) & \
|
|
794 |
\ (! K1 M1 L1 N1 O1 P1. equal(K1::'a,L1) --> equal(euclid2(M1::'a,K1,N1,O1,P1),euclid2(M1::'a,L1,N1,O1,P1))) & \
|
|
795 |
\ (! Q1 S1 T1 R1 U1 V1. equal(Q1::'a,R1) --> equal(euclid2(S1::'a,T1,Q1,U1,V1),euclid2(S1::'a,T1,R1,U1,V1))) & \
|
|
796 |
\ (! W1 Y1 Z1 A2 X1 B2. equal(W1::'a,X1) --> equal(euclid2(Y1::'a,Z1,A2,W1,B2),euclid2(Y1::'a,Z1,A2,X1,B2))) & \
|
|
797 |
\ (! C2 E2 F2 G2 H2 D2. equal(C2::'a,D2) --> equal(euclid2(E2::'a,F2,G2,H2,C2),euclid2(E2::'a,F2,G2,H2,D2))) & \
|
|
798 |
\ (! X Y V1 V2 V3. equal(X::'a,Y) --> equal(extension(X::'a,V1,V2,V3),extension(Y::'a,V1,V2,V3))) & \
|
|
799 |
\ (! X V1 Y V2 V3. equal(X::'a,Y) --> equal(extension(V1::'a,X,V2,V3),extension(V1::'a,Y,V2,V3))) & \
|
|
800 |
\ (! X V1 V2 Y V3. equal(X::'a,Y) --> equal(extension(V1::'a,V2,X,V3),extension(V1::'a,V2,Y,V3))) & \
|
|
801 |
\ (! X V1 V2 V3 Y. equal(X::'a,Y) --> equal(extension(V1::'a,V2,V3,X),extension(V1::'a,V2,V3,Y))) & \
|
|
802 |
\ (! X Y V1 V2 V3 V4 V5. equal(X::'a,Y) --> equal(continuous(X::'a,V1,V2,V3,V4,V5),continuous(Y::'a,V1,V2,V3,V4,V5))) & \
|
|
803 |
\ (! X V1 Y V2 V3 V4 V5. equal(X::'a,Y) --> equal(continuous(V1::'a,X,V2,V3,V4,V5),continuous(V1::'a,Y,V2,V3,V4,V5))) & \
|
|
804 |
\ (! X V1 V2 Y V3 V4 V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,X,V3,V4,V5),continuous(V1::'a,V2,Y,V3,V4,V5))) & \
|
|
805 |
\ (! X V1 V2 V3 Y V4 V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,X,V4,V5),continuous(V1::'a,V2,V3,Y,V4,V5))) & \
|
|
806 |
\ (! X V1 V2 V3 V4 Y V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,V4,X,V5),continuous(V1::'a,V2,V3,V4,Y,V5))) & \
|
|
807 |
\ (! X V1 V2 V3 V4 V5 Y. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,V4,V5,X),continuous(V1::'a,V2,V3,V4,V5,Y))) & \
|
|
808 |
\ (~between(a::'a,b,b)) --> False",
|
|
809 |
meson_tac);
|
|
810 |
|
|
811 |
(*4272 inferences so far. Searching to depth 10. 29.4 secs*)
|
|
812 |
val GEO017_2 = prove_hard
|
|
813 |
("(! X. equal(X::'a,X)) & \
|
|
814 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
815 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
816 |
\ (! Y X. equidistant(X::'a,Y,Y,X)) & \
|
|
817 |
\ (! X Y Z V V2 W. equidistant(X::'a,Y,Z,V) & equidistant(X::'a,Y,V2,W) --> equidistant(Z::'a,V,V2,W)) & \
|
|
818 |
\ (! Z X Y. equidistant(X::'a,Y,Z,Z) --> equal(X::'a,Y)) & \
|
|
819 |
\ (! X Y W V. between(X::'a,Y,extension(X::'a,Y,W,V))) & \
|
|
820 |
\ (! X Y W V. equidistant(Y::'a,extension(X::'a,Y,W,V),W,V)) & \
|
|
821 |
\ (! X1 Y1 X Y Z V Z1 V1. equidistant(X::'a,Y,X1,Y1) & equidistant(Y::'a,Z,Y1,Z1) & equidistant(X::'a,V,X1,V1) & equidistant(Y::'a,V,Y1,V1) & between(X::'a,Y,Z) & between(X1::'a,Y1,Z1) --> equal(X::'a,Y) | equidistant(Z::'a,V,Z1,V1)) & \
|
|
822 |
\ (! X Y. between(X::'a,Y,X) --> equal(X::'a,Y)) & \
|
|
823 |
\ (! U V W X Y. between(U::'a,V,W) & between(Y::'a,X,W) --> between(V::'a,inner_pasch(U::'a,V,W,X,Y),Y)) & \
|
|
824 |
\ (! V W X Y U. between(U::'a,V,W) & between(Y::'a,X,W) --> between(X::'a,inner_pasch(U::'a,V,W,X,Y),U)) & \
|
|
825 |
\ (~between(lower_dimension_point_1::'a,lower_dimension_point_2,lower_dimension_point_3)) & \
|
|
826 |
\ (~between(lower_dimension_point_2::'a,lower_dimension_point_3,lower_dimension_point_1)) & \
|
|
827 |
\ (~between(lower_dimension_point_3::'a,lower_dimension_point_1,lower_dimension_point_2)) & \
|
|
828 |
\ (! Z X Y W V. equidistant(X::'a,W,X,V) & equidistant(Y::'a,W,Y,V) & equidistant(Z::'a,W,Z,V) --> between(X::'a,Y,Z) | between(Y::'a,Z,X) | between(Z::'a,X,Y) | equal(W::'a,V)) & \
|
|
829 |
\ (! U V W X Y. between(U::'a,W,Y) & between(V::'a,W,X) --> equal(U::'a,W) | between(U::'a,V,euclid1(U::'a,V,W,X,Y))) & \
|
|
830 |
\ (! U V W X Y. between(U::'a,W,Y) & between(V::'a,W,X) --> equal(U::'a,W) | between(U::'a,X,euclid2(U::'a,V,W,X,Y))) & \
|
|
831 |
\ (! U V W X Y. between(U::'a,W,Y) & between(V::'a,W,X) --> equal(U::'a,W) | between(euclid1(U::'a,V,W,X,Y),Y,euclid2(U::'a,V,W,X,Y))) & \
|
|
832 |
\ (! U V V1 W X X1. equidistant(U::'a,V,U,V1) & equidistant(U::'a,X,U,X1) & between(U::'a,V,X) & between(V::'a,W,X) --> between(V1::'a,continuous(U::'a,V,V1,W,X,X1),X1)) & \
|
|
833 |
\ (! U V V1 W X X1. equidistant(U::'a,V,U,V1) & equidistant(U::'a,X,U,X1) & between(U::'a,V,X) & between(V::'a,W,X) --> equidistant(U::'a,W,U,continuous(U::'a,V,V1,W,X,X1))) & \
|
|
834 |
\ (! X Y W Z. equal(X::'a,Y) & between(X::'a,W,Z) --> between(Y::'a,W,Z)) & \
|
|
835 |
\ (! X W Y Z. equal(X::'a,Y) & between(W::'a,X,Z) --> between(W::'a,Y,Z)) & \
|
|
836 |
\ (! X W Z Y. equal(X::'a,Y) & between(W::'a,Z,X) --> between(W::'a,Z,Y)) & \
|
|
837 |
\ (! X Y V W Z. equal(X::'a,Y) & equidistant(X::'a,V,W,Z) --> equidistant(Y::'a,V,W,Z)) & \
|
|
838 |
\ (! X V Y W Z. equal(X::'a,Y) & equidistant(V::'a,X,W,Z) --> equidistant(V::'a,Y,W,Z)) & \
|
|
839 |
\ (! X V W Y Z. equal(X::'a,Y) & equidistant(V::'a,W,X,Z) --> equidistant(V::'a,W,Y,Z)) & \
|
|
840 |
\ (! X V W Z Y. equal(X::'a,Y) & equidistant(V::'a,W,Z,X) --> equidistant(V::'a,W,Z,Y)) & \
|
|
841 |
\ (! X Y V1 V2 V3 V4. equal(X::'a,Y) --> equal(inner_pasch(X::'a,V1,V2,V3,V4),inner_pasch(Y::'a,V1,V2,V3,V4))) & \
|
|
842 |
\ (! X V1 Y V2 V3 V4. equal(X::'a,Y) --> equal(inner_pasch(V1::'a,X,V2,V3,V4),inner_pasch(V1::'a,Y,V2,V3,V4))) & \
|
|
843 |
\ (! X V1 V2 Y V3 V4. equal(X::'a,Y) --> equal(inner_pasch(V1::'a,V2,X,V3,V4),inner_pasch(V1::'a,V2,Y,V3,V4))) & \
|
|
844 |
\ (! X V1 V2 V3 Y V4. equal(X::'a,Y) --> equal(inner_pasch(V1::'a,V2,V3,X,V4),inner_pasch(V1::'a,V2,V3,Y,V4))) & \
|
|
845 |
\ (! X V1 V2 V3 V4 Y. equal(X::'a,Y) --> equal(inner_pasch(V1::'a,V2,V3,V4,X),inner_pasch(V1::'a,V2,V3,V4,Y))) & \
|
|
846 |
\ (! A B C D E F'. equal(A::'a,B) --> equal(euclid1(A::'a,C,D,E,F'),euclid1(B::'a,C,D,E,F'))) & \
|
|
847 |
\ (! G I' H J K' L. equal(G::'a,H) --> equal(euclid1(I'::'a,G,J,K',L),euclid1(I'::'a,H,J,K',L))) & \
|
|
848 |
\ (! M O_ P N Q R. equal(M::'a,N) --> equal(euclid1(O_::'a,P,M,Q,R),euclid1(O_::'a,P,N,Q,R))) & \
|
|
849 |
\ (! S' U V W T' X. equal(S'::'a,T') --> equal(euclid1(U::'a,V,W,S',X),euclid1(U::'a,V,W,T',X))) & \
|
|
850 |
\ (! Y A1 B1 C1 D1 Z. equal(Y::'a,Z) --> equal(euclid1(A1::'a,B1,C1,D1,Y),euclid1(A1::'a,B1,C1,D1,Z))) & \
|
|
851 |
\ (! E1 F1 G1 H1 I1 J1. equal(E1::'a,F1) --> equal(euclid2(E1::'a,G1,H1,I1,J1),euclid2(F1::'a,G1,H1,I1,J1))) & \
|
|
852 |
\ (! K1 M1 L1 N1 O1 P1. equal(K1::'a,L1) --> equal(euclid2(M1::'a,K1,N1,O1,P1),euclid2(M1::'a,L1,N1,O1,P1))) & \
|
|
853 |
\ (! Q1 S1 T1 R1 U1 V1. equal(Q1::'a,R1) --> equal(euclid2(S1::'a,T1,Q1,U1,V1),euclid2(S1::'a,T1,R1,U1,V1))) & \
|
|
854 |
\ (! W1 Y1 Z1 A2 X1 B2. equal(W1::'a,X1) --> equal(euclid2(Y1::'a,Z1,A2,W1,B2),euclid2(Y1::'a,Z1,A2,X1,B2))) & \
|
|
855 |
\ (! C2 E2 F2 G2 H2 D2. equal(C2::'a,D2) --> equal(euclid2(E2::'a,F2,G2,H2,C2),euclid2(E2::'a,F2,G2,H2,D2))) & \
|
|
856 |
\ (! X Y V1 V2 V3. equal(X::'a,Y) --> equal(extension(X::'a,V1,V2,V3),extension(Y::'a,V1,V2,V3))) & \
|
|
857 |
\ (! X V1 Y V2 V3. equal(X::'a,Y) --> equal(extension(V1::'a,X,V2,V3),extension(V1::'a,Y,V2,V3))) & \
|
|
858 |
\ (! X V1 V2 Y V3. equal(X::'a,Y) --> equal(extension(V1::'a,V2,X,V3),extension(V1::'a,V2,Y,V3))) & \
|
|
859 |
\ (! X V1 V2 V3 Y. equal(X::'a,Y) --> equal(extension(V1::'a,V2,V3,X),extension(V1::'a,V2,V3,Y))) & \
|
|
860 |
\ (! X Y V1 V2 V3 V4 V5. equal(X::'a,Y) --> equal(continuous(X::'a,V1,V2,V3,V4,V5),continuous(Y::'a,V1,V2,V3,V4,V5))) & \
|
|
861 |
\ (! X V1 Y V2 V3 V4 V5. equal(X::'a,Y) --> equal(continuous(V1::'a,X,V2,V3,V4,V5),continuous(V1::'a,Y,V2,V3,V4,V5))) & \
|
|
862 |
\ (! X V1 V2 Y V3 V4 V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,X,V3,V4,V5),continuous(V1::'a,V2,Y,V3,V4,V5))) & \
|
|
863 |
\ (! X V1 V2 V3 Y V4 V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,X,V4,V5),continuous(V1::'a,V2,V3,Y,V4,V5))) & \
|
|
864 |
\ (! X V1 V2 V3 V4 Y V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,V4,X,V5),continuous(V1::'a,V2,V3,V4,Y,V5))) & \
|
|
865 |
\ (! X V1 V2 V3 V4 V5 Y. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,V4,V5,X),continuous(V1::'a,V2,V3,V4,V5,Y))) & \
|
|
866 |
\ (equidistant(u::'a,v,w,x)) & \
|
|
867 |
\ (~equidistant(u::'a,v,x,w)) --> False",
|
|
868 |
meson_tac);
|
|
869 |
|
|
870 |
(****************SLOW
|
|
871 |
382903 inferences so far. Searching to depth 9. No proof after 35 minutes.
|
|
872 |
val GEO027_3 = prove_hard
|
|
873 |
("(! X. equal(X::'a,X)) & \
|
|
874 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
875 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
876 |
\ (! Y X. equidistant(X::'a,Y,Y,X)) & \
|
|
877 |
\ (! X Y Z V V2 W. equidistant(X::'a,Y,Z,V) & equidistant(X::'a,Y,V2,W) --> equidistant(Z::'a,V,V2,W)) & \
|
|
878 |
\ (! Z X Y. equidistant(X::'a,Y,Z,Z) --> equal(X::'a,Y)) & \
|
|
879 |
\ (! X Y W V. between(X::'a,Y,extension(X::'a,Y,W,V))) & \
|
|
880 |
\ (! X Y W V. equidistant(Y::'a,extension(X::'a,Y,W,V),W,V)) & \
|
|
881 |
\ (! X1 Y1 X Y Z V Z1 V1. equidistant(X::'a,Y,X1,Y1) & equidistant(Y::'a,Z,Y1,Z1) & equidistant(X::'a,V,X1,V1) & equidistant(Y::'a,V,Y1,V1) & between(X::'a,Y,Z) & between(X1::'a,Y1,Z1) --> equal(X::'a,Y) | equidistant(Z::'a,V,Z1,V1)) & \
|
|
882 |
\ (! X Y. between(X::'a,Y,X) --> equal(X::'a,Y)) & \
|
|
883 |
\ (! U V W X Y. between(U::'a,V,W) & between(Y::'a,X,W) --> between(V::'a,inner_pasch(U::'a,V,W,X,Y),Y)) & \
|
|
884 |
\ (! V W X Y U. between(U::'a,V,W) & between(Y::'a,X,W) --> between(X::'a,inner_pasch(U::'a,V,W,X,Y),U)) & \
|
|
885 |
\ (~between(lower_dimension_point_1::'a,lower_dimension_point_2,lower_dimension_point_3)) & \
|
|
886 |
\ (~between(lower_dimension_point_2::'a,lower_dimension_point_3,lower_dimension_point_1)) & \
|
|
887 |
\ (~between(lower_dimension_point_3::'a,lower_dimension_point_1,lower_dimension_point_2)) & \
|
|
888 |
\ (! Z X Y W V. equidistant(X::'a,W,X,V) & equidistant(Y::'a,W,Y,V) & equidistant(Z::'a,W,Z,V) --> between(X::'a,Y,Z) | between(Y::'a,Z,X) | between(Z::'a,X,Y) | equal(W::'a,V)) & \
|
|
889 |
\ (! U V W X Y. between(U::'a,W,Y) & between(V::'a,W,X) --> equal(U::'a,W) | between(U::'a,V,euclid1(U::'a,V,W,X,Y))) & \
|
|
890 |
\ (! U V W X Y. between(U::'a,W,Y) & between(V::'a,W,X) --> equal(U::'a,W) | between(U::'a,X,euclid2(U::'a,V,W,X,Y))) & \
|
|
891 |
\ (! U V W X Y. between(U::'a,W,Y) & between(V::'a,W,X) --> equal(U::'a,W) | between(euclid1(U::'a,V,W,X,Y),Y,euclid2(U::'a,V,W,X,Y))) & \
|
|
892 |
\ (! U V V1 W X X1. equidistant(U::'a,V,U,V1) & equidistant(U::'a,X,U,X1) & between(U::'a,V,X) & between(V::'a,W,X) --> between(V1::'a,continuous(U::'a,V,V1,W,X,X1),X1)) & \
|
|
893 |
\ (! U V V1 W X X1. equidistant(U::'a,V,U,V1) & equidistant(U::'a,X,U,X1) & between(U::'a,V,X) & between(V::'a,W,X) --> equidistant(U::'a,W,U,continuous(U::'a,V,V1,W,X,X1))) & \
|
|
894 |
\ (! X Y W Z. equal(X::'a,Y) & between(X::'a,W,Z) --> between(Y::'a,W,Z)) & \
|
|
895 |
\ (! X W Y Z. equal(X::'a,Y) & between(W::'a,X,Z) --> between(W::'a,Y,Z)) & \
|
|
896 |
\ (! X W Z Y. equal(X::'a,Y) & between(W::'a,Z,X) --> between(W::'a,Z,Y)) & \
|
|
897 |
\ (! X Y V W Z. equal(X::'a,Y) & equidistant(X::'a,V,W,Z) --> equidistant(Y::'a,V,W,Z)) & \
|
|
898 |
\ (! X V Y W Z. equal(X::'a,Y) & equidistant(V::'a,X,W,Z) --> equidistant(V::'a,Y,W,Z)) & \
|
|
899 |
\ (! X V W Y Z. equal(X::'a,Y) & equidistant(V::'a,W,X,Z) --> equidistant(V::'a,W,Y,Z)) & \
|
|
900 |
\ (! X V W Z Y. equal(X::'a,Y) & equidistant(V::'a,W,Z,X) --> equidistant(V::'a,W,Z,Y)) & \
|
|
901 |
\ (! X Y V1 V2 V3 V4. equal(X::'a,Y) --> equal(inner_pasch(X::'a,V1,V2,V3,V4),inner_pasch(Y::'a,V1,V2,V3,V4))) & \
|
|
902 |
\ (! X V1 Y V2 V3 V4. equal(X::'a,Y) --> equal(inner_pasch(V1::'a,X,V2,V3,V4),inner_pasch(V1::'a,Y,V2,V3,V4))) & \
|
|
903 |
\ (! X V1 V2 Y V3 V4. equal(X::'a,Y) --> equal(inner_pasch(V1::'a,V2,X,V3,V4),inner_pasch(V1::'a,V2,Y,V3,V4))) & \
|
|
904 |
\ (! X V1 V2 V3 Y V4. equal(X::'a,Y) --> equal(inner_pasch(V1::'a,V2,V3,X,V4),inner_pasch(V1::'a,V2,V3,Y,V4))) & \
|
|
905 |
\ (! X V1 V2 V3 V4 Y. equal(X::'a,Y) --> equal(inner_pasch(V1::'a,V2,V3,V4,X),inner_pasch(V1::'a,V2,V3,V4,Y))) & \
|
|
906 |
\ (! A B C D E F'. equal(A::'a,B) --> equal(euclid1(A::'a,C,D,E,F'),euclid1(B::'a,C,D,E,F'))) & \
|
|
907 |
\ (! G I' H J K' L. equal(G::'a,H) --> equal(euclid1(I'::'a,G,J,K',L),euclid1(I'::'a,H,J,K',L))) & \
|
|
908 |
\ (! M O_ P N Q R. equal(M::'a,N) --> equal(euclid1(O_::'a,P,M,Q,R),euclid1(O_::'a,P,N,Q,R))) & \
|
|
909 |
\ (! S' U V W T' X. equal(S'::'a,T') --> equal(euclid1(U::'a,V,W,S',X),euclid1(U::'a,V,W,T',X))) & \
|
|
910 |
\ (! Y A1 B1 C1 D1 Z. equal(Y::'a,Z) --> equal(euclid1(A1::'a,B1,C1,D1,Y),euclid1(A1::'a,B1,C1,D1,Z))) & \
|
|
911 |
\ (! E1 F1 G1 H1 I1 J1. equal(E1::'a,F1) --> equal(euclid2(E1::'a,G1,H1,I1,J1),euclid2(F1::'a,G1,H1,I1,J1))) & \
|
|
912 |
\ (! K1 M1 L1 N1 O1 P1. equal(K1::'a,L1) --> equal(euclid2(M1::'a,K1,N1,O1,P1),euclid2(M1::'a,L1,N1,O1,P1))) & \
|
|
913 |
\ (! Q1 S1 T1 R1 U1 V1. equal(Q1::'a,R1) --> equal(euclid2(S1::'a,T1,Q1,U1,V1),euclid2(S1::'a,T1,R1,U1,V1))) & \
|
|
914 |
\ (! W1 Y1 Z1 A2 X1 B2. equal(W1::'a,X1) --> equal(euclid2(Y1::'a,Z1,A2,W1,B2),euclid2(Y1::'a,Z1,A2,X1,B2))) & \
|
|
915 |
\ (! C2 E2 F2 G2 H2 D2. equal(C2::'a,D2) --> equal(euclid2(E2::'a,F2,G2,H2,C2),euclid2(E2::'a,F2,G2,H2,D2))) & \
|
|
916 |
\ (! X Y V1 V2 V3. equal(X::'a,Y) --> equal(extension(X::'a,V1,V2,V3),extension(Y::'a,V1,V2,V3))) & \
|
|
917 |
\ (! X V1 Y V2 V3. equal(X::'a,Y) --> equal(extension(V1::'a,X,V2,V3),extension(V1::'a,Y,V2,V3))) & \
|
|
918 |
\ (! X V1 V2 Y V3. equal(X::'a,Y) --> equal(extension(V1::'a,V2,X,V3),extension(V1::'a,V2,Y,V3))) & \
|
|
919 |
\ (! X V1 V2 V3 Y. equal(X::'a,Y) --> equal(extension(V1::'a,V2,V3,X),extension(V1::'a,V2,V3,Y))) & \
|
|
920 |
\ (! X Y V1 V2 V3 V4 V5. equal(X::'a,Y) --> equal(continuous(X::'a,V1,V2,V3,V4,V5),continuous(Y::'a,V1,V2,V3,V4,V5))) & \
|
|
921 |
\ (! X V1 Y V2 V3 V4 V5. equal(X::'a,Y) --> equal(continuous(V1::'a,X,V2,V3,V4,V5),continuous(V1::'a,Y,V2,V3,V4,V5))) & \
|
|
922 |
\ (! X V1 V2 Y V3 V4 V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,X,V3,V4,V5),continuous(V1::'a,V2,Y,V3,V4,V5))) & \
|
|
923 |
\ (! X V1 V2 V3 Y V4 V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,X,V4,V5),continuous(V1::'a,V2,V3,Y,V4,V5))) & \
|
|
924 |
\ (! X V1 V2 V3 V4 Y V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,V4,X,V5),continuous(V1::'a,V2,V3,V4,Y,V5))) & \
|
|
925 |
\ (! X V1 V2 V3 V4 V5 Y. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,V4,V5,X),continuous(V1::'a,V2,V3,V4,V5,Y))) & \
|
|
926 |
\ (! U V. equal(reflection(U::'a,V),extension(U::'a,V,U,V))) & \
|
|
927 |
\ (! X Y Z. equal(X::'a,Y) --> equal(reflection(X::'a,Z),reflection(Y::'a,Z))) & \
|
|
928 |
\ (! A1 C1 B1. equal(A1::'a,B1) --> equal(reflection(C1::'a,A1),reflection(C1::'a,B1))) & \
|
|
929 |
\ (! U V. equidistant(U::'a,V,U,V)) & \
|
|
930 |
\ (! W X U V. equidistant(U::'a,V,W,X) --> equidistant(W::'a,X,U,V)) & \
|
|
931 |
\ (! V U W X. equidistant(U::'a,V,W,X) --> equidistant(V::'a,U,W,X)) & \
|
|
932 |
\ (! U V X W. equidistant(U::'a,V,W,X) --> equidistant(U::'a,V,X,W)) & \
|
|
933 |
\ (! V U X W. equidistant(U::'a,V,W,X) --> equidistant(V::'a,U,X,W)) & \
|
|
934 |
\ (! W X V U. equidistant(U::'a,V,W,X) --> equidistant(W::'a,X,V,U)) & \
|
|
935 |
\ (! X W U V. equidistant(U::'a,V,W,X) --> equidistant(X::'a,W,U,V)) & \
|
|
936 |
\ (! X W V U. equidistant(U::'a,V,W,X) --> equidistant(X::'a,W,V,U)) & \
|
|
937 |
\ (! W X U V Y Z. equidistant(U::'a,V,W,X) & equidistant(W::'a,X,Y,Z) --> equidistant(U::'a,V,Y,Z)) & \
|
|
938 |
\ (! U V W. equal(V::'a,extension(U::'a,V,W,W))) & \
|
|
939 |
\ (! W X U V Y. equal(Y::'a,extension(U::'a,V,W,X)) --> between(U::'a,V,Y)) & \
|
|
940 |
\ (! U V. between(U::'a,V,reflection(U::'a,V))) & \
|
|
941 |
\ (! U V. equidistant(V::'a,reflection(U::'a,V),U,V)) & \
|
|
942 |
\ (! U V. equal(U::'a,V) --> equal(V::'a,reflection(U::'a,V))) & \
|
|
943 |
\ (! U. equal(U::'a,reflection(U::'a,U))) & \
|
|
944 |
\ (! U V. equal(V::'a,reflection(U::'a,V)) --> equal(U::'a,V)) & \
|
|
945 |
\ (! U V. equidistant(U::'a,U,V,V)) & \
|
|
946 |
\ (! V V1 U W U1 W1. equidistant(U::'a,V,U1,V1) & equidistant(V::'a,W,V1,W1) & between(U::'a,V,W) & between(U1::'a,V1,W1) --> equidistant(U::'a,W,U1,W1)) & \
|
|
947 |
\ (! U V W X. between(U::'a,V,W) & between(U::'a,V,X) & equidistant(V::'a,W,V,X) --> equal(U::'a,V) | equal(W::'a,X)) & \
|
|
948 |
\ (between(u::'a,v,w)) & \
|
|
949 |
\ (~equal(u::'a,v)) & \
|
|
950 |
\ (~equal(w::'a,extension(u::'a,v,v,w))) --> False",
|
|
951 |
meson_tac);
|
|
952 |
****************)
|
|
953 |
|
|
954 |
(*313884 inferences so far. Searching to depth 10. 887 secs: 15 mins.*)
|
|
955 |
val GEO058_2 = prove_hard
|
|
956 |
("(! X. equal(X::'a,X)) & \
|
|
957 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
958 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
959 |
\ (! Y X. equidistant(X::'a,Y,Y,X)) & \
|
|
960 |
\ (! X Y Z V V2 W. equidistant(X::'a,Y,Z,V) & equidistant(X::'a,Y,V2,W) --> equidistant(Z::'a,V,V2,W)) & \
|
|
961 |
\ (! Z X Y. equidistant(X::'a,Y,Z,Z) --> equal(X::'a,Y)) & \
|
|
962 |
\ (! X Y W V. between(X::'a,Y,extension(X::'a,Y,W,V))) & \
|
|
963 |
\ (! X Y W V. equidistant(Y::'a,extension(X::'a,Y,W,V),W,V)) & \
|
|
964 |
\ (! X1 Y1 X Y Z V Z1 V1. equidistant(X::'a,Y,X1,Y1) & equidistant(Y::'a,Z,Y1,Z1) & equidistant(X::'a,V,X1,V1) & equidistant(Y::'a,V,Y1,V1) & between(X::'a,Y,Z) & between(X1::'a,Y1,Z1) --> equal(X::'a,Y) | equidistant(Z::'a,V,Z1,V1)) & \
|
|
965 |
\ (! X Y. between(X::'a,Y,X) --> equal(X::'a,Y)) & \
|
|
966 |
\ (! U V W X Y. between(U::'a,V,W) & between(Y::'a,X,W) --> between(V::'a,inner_pasch(U::'a,V,W,X,Y),Y)) & \
|
|
967 |
\ (! V W X Y U. between(U::'a,V,W) & between(Y::'a,X,W) --> between(X::'a,inner_pasch(U::'a,V,W,X,Y),U)) & \
|
|
968 |
\ (~between(lower_dimension_point_1::'a,lower_dimension_point_2,lower_dimension_point_3)) & \
|
|
969 |
\ (~between(lower_dimension_point_2::'a,lower_dimension_point_3,lower_dimension_point_1)) & \
|
|
970 |
\ (~between(lower_dimension_point_3::'a,lower_dimension_point_1,lower_dimension_point_2)) & \
|
|
971 |
\ (! Z X Y W V. equidistant(X::'a,W,X,V) & equidistant(Y::'a,W,Y,V) & equidistant(Z::'a,W,Z,V) --> between(X::'a,Y,Z) | between(Y::'a,Z,X) | between(Z::'a,X,Y) | equal(W::'a,V)) & \
|
|
972 |
\ (! U V W X Y. between(U::'a,W,Y) & between(V::'a,W,X) --> equal(U::'a,W) | between(U::'a,V,euclid1(U::'a,V,W,X,Y))) & \
|
|
973 |
\ (! U V W X Y. between(U::'a,W,Y) & between(V::'a,W,X) --> equal(U::'a,W) | between(U::'a,X,euclid2(U::'a,V,W,X,Y))) & \
|
|
974 |
\ (! U V W X Y. between(U::'a,W,Y) & between(V::'a,W,X) --> equal(U::'a,W) | between(euclid1(U::'a,V,W,X,Y),Y,euclid2(U::'a,V,W,X,Y))) & \
|
|
975 |
\ (! U V V1 W X X1. equidistant(U::'a,V,U,V1) & equidistant(U::'a,X,U,X1) & between(U::'a,V,X) & between(V::'a,W,X) --> between(V1::'a,continuous(U::'a,V,V1,W,X,X1),X1)) & \
|
|
976 |
\ (! U V V1 W X X1. equidistant(U::'a,V,U,V1) & equidistant(U::'a,X,U,X1) & between(U::'a,V,X) & between(V::'a,W,X) --> equidistant(U::'a,W,U,continuous(U::'a,V,V1,W,X,X1))) & \
|
|
977 |
\ (! X Y W Z. equal(X::'a,Y) & between(X::'a,W,Z) --> between(Y::'a,W,Z)) & \
|
|
978 |
\ (! X W Y Z. equal(X::'a,Y) & between(W::'a,X,Z) --> between(W::'a,Y,Z)) & \
|
|
979 |
\ (! X W Z Y. equal(X::'a,Y) & between(W::'a,Z,X) --> between(W::'a,Z,Y)) & \
|
|
980 |
\ (! X Y V W Z. equal(X::'a,Y) & equidistant(X::'a,V,W,Z) --> equidistant(Y::'a,V,W,Z)) & \
|
|
981 |
\ (! X V Y W Z. equal(X::'a,Y) & equidistant(V::'a,X,W,Z) --> equidistant(V::'a,Y,W,Z)) & \
|
|
982 |
\ (! X V W Y Z. equal(X::'a,Y) & equidistant(V::'a,W,X,Z) --> equidistant(V::'a,W,Y,Z)) & \
|
|
983 |
\ (! X V W Z Y. equal(X::'a,Y) & equidistant(V::'a,W,Z,X) --> equidistant(V::'a,W,Z,Y)) & \
|
|
984 |
\ (! X Y V1 V2 V3 V4. equal(X::'a,Y) --> equal(inner_pasch(X::'a,V1,V2,V3,V4),inner_pasch(Y::'a,V1,V2,V3,V4))) & \
|
|
985 |
\ (! X V1 Y V2 V3 V4. equal(X::'a,Y) --> equal(inner_pasch(V1::'a,X,V2,V3,V4),inner_pasch(V1::'a,Y,V2,V3,V4))) & \
|
|
986 |
\ (! X V1 V2 Y V3 V4. equal(X::'a,Y) --> equal(inner_pasch(V1::'a,V2,X,V3,V4),inner_pasch(V1::'a,V2,Y,V3,V4))) & \
|
|
987 |
\ (! X V1 V2 V3 Y V4. equal(X::'a,Y) --> equal(inner_pasch(V1::'a,V2,V3,X,V4),inner_pasch(V1::'a,V2,V3,Y,V4))) & \
|
|
988 |
\ (! X V1 V2 V3 V4 Y. equal(X::'a,Y) --> equal(inner_pasch(V1::'a,V2,V3,V4,X),inner_pasch(V1::'a,V2,V3,V4,Y))) & \
|
|
989 |
\ (! A B C D E F'. equal(A::'a,B) --> equal(euclid1(A::'a,C,D,E,F'),euclid1(B::'a,C,D,E,F'))) & \
|
|
990 |
\ (! G I' H J K' L. equal(G::'a,H) --> equal(euclid1(I'::'a,G,J,K',L),euclid1(I'::'a,H,J,K',L))) & \
|
|
991 |
\ (! M O_ P N Q R. equal(M::'a,N) --> equal(euclid1(O_::'a,P,M,Q,R),euclid1(O_::'a,P,N,Q,R))) & \
|
|
992 |
\ (! S' U V W T' X. equal(S'::'a,T') --> equal(euclid1(U::'a,V,W,S',X),euclid1(U::'a,V,W,T',X))) & \
|
|
993 |
\ (! Y A1 B1 C1 D1 Z. equal(Y::'a,Z) --> equal(euclid1(A1::'a,B1,C1,D1,Y),euclid1(A1::'a,B1,C1,D1,Z))) & \
|
|
994 |
\ (! E1 F1 G1 H1 I1 J1. equal(E1::'a,F1) --> equal(euclid2(E1::'a,G1,H1,I1,J1),euclid2(F1::'a,G1,H1,I1,J1))) & \
|
|
995 |
\ (! K1 M1 L1 N1 O1 P1. equal(K1::'a,L1) --> equal(euclid2(M1::'a,K1,N1,O1,P1),euclid2(M1::'a,L1,N1,O1,P1))) & \
|
|
996 |
\ (! Q1 S1 T1 R1 U1 V1. equal(Q1::'a,R1) --> equal(euclid2(S1::'a,T1,Q1,U1,V1),euclid2(S1::'a,T1,R1,U1,V1))) & \
|
|
997 |
\ (! W1 Y1 Z1 A2 X1 B2. equal(W1::'a,X1) --> equal(euclid2(Y1::'a,Z1,A2,W1,B2),euclid2(Y1::'a,Z1,A2,X1,B2))) & \
|
|
998 |
\ (! C2 E2 F2 G2 H2 D2. equal(C2::'a,D2) --> equal(euclid2(E2::'a,F2,G2,H2,C2),euclid2(E2::'a,F2,G2,H2,D2))) & \
|
|
999 |
\ (! X Y V1 V2 V3. equal(X::'a,Y) --> equal(extension(X::'a,V1,V2,V3),extension(Y::'a,V1,V2,V3))) & \
|
|
1000 |
\ (! X V1 Y V2 V3. equal(X::'a,Y) --> equal(extension(V1::'a,X,V2,V3),extension(V1::'a,Y,V2,V3))) & \
|
|
1001 |
\ (! X V1 V2 Y V3. equal(X::'a,Y) --> equal(extension(V1::'a,V2,X,V3),extension(V1::'a,V2,Y,V3))) & \
|
|
1002 |
\ (! X V1 V2 V3 Y. equal(X::'a,Y) --> equal(extension(V1::'a,V2,V3,X),extension(V1::'a,V2,V3,Y))) & \
|
|
1003 |
\ (! X Y V1 V2 V3 V4 V5. equal(X::'a,Y) --> equal(continuous(X::'a,V1,V2,V3,V4,V5),continuous(Y::'a,V1,V2,V3,V4,V5))) & \
|
|
1004 |
\ (! X V1 Y V2 V3 V4 V5. equal(X::'a,Y) --> equal(continuous(V1::'a,X,V2,V3,V4,V5),continuous(V1::'a,Y,V2,V3,V4,V5))) & \
|
|
1005 |
\ (! X V1 V2 Y V3 V4 V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,X,V3,V4,V5),continuous(V1::'a,V2,Y,V3,V4,V5))) & \
|
|
1006 |
\ (! X V1 V2 V3 Y V4 V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,X,V4,V5),continuous(V1::'a,V2,V3,Y,V4,V5))) & \
|
|
1007 |
\ (! X V1 V2 V3 V4 Y V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,V4,X,V5),continuous(V1::'a,V2,V3,V4,Y,V5))) & \
|
|
1008 |
\ (! X V1 V2 V3 V4 V5 Y. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,V4,V5,X),continuous(V1::'a,V2,V3,V4,V5,Y))) & \
|
|
1009 |
\ (! U V. equal(reflection(U::'a,V),extension(U::'a,V,U,V))) & \
|
|
1010 |
\ (! X Y Z. equal(X::'a,Y) --> equal(reflection(X::'a,Z),reflection(Y::'a,Z))) & \
|
|
1011 |
\ (! A1 C1 B1. equal(A1::'a,B1) --> equal(reflection(C1::'a,A1),reflection(C1::'a,B1))) & \
|
|
1012 |
\ (equal(v::'a,reflection(u::'a,v))) & \
|
|
1013 |
\ (~equal(u::'a,v)) --> False",
|
|
1014 |
meson_tac);
|
|
1015 |
|
|
1016 |
(*0 inferences so far. Searching to depth 0. 0.2 secs*)
|
|
1017 |
val GEO079_1 = prove
|
|
1018 |
("(! U V W X Y Z. right_angle(U::'a,V,W) & right_angle(X::'a,Y,Z) --> eq(U::'a,V,W,X,Y,Z)) & \
|
|
1019 |
\ (! U V W X Y Z. congruent(U::'a,V,W,X,Y,Z) --> eq(U::'a,V,W,X,Y,Z)) & \
|
|
1020 |
\ (! V W U X. trapezoid(U::'a,V,W,X) --> parallel(V::'a,W,U,X)) & \
|
|
1021 |
\ (! U V X Y. parallel(U::'a,V,X,Y) --> eq(X::'a,V,U,V,X,Y)) & \
|
|
1022 |
\ (trapezoid(a::'a,b,c,d)) & \
|
|
1023 |
\ (~eq(a::'a,c,b,c,a,d)) --> False",
|
|
1024 |
meson_tac);
|
|
1025 |
|
|
1026 |
(****************SLOW
|
|
1027 |
2032008 inferences so far. Searching to depth 16. No proof after 30 minutes.
|
|
1028 |
val GRP001_1 = prove_hard
|
|
1029 |
("(! X. equal(X::'a,X)) & \
|
|
1030 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
1031 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
1032 |
\ (! X. product(identity::'a,X,X)) & \
|
|
1033 |
\ (! X. product(X::'a,identity,X)) & \
|
|
1034 |
\ (! X. product(inverse(X),X,identity)) & \
|
|
1035 |
\ (! X. product(X::'a,inverse(X),identity)) & \
|
|
1036 |
\ (! X Y. product(X::'a,Y,multiply(X::'a,Y))) & \
|
|
1037 |
\ (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) & \
|
|
1038 |
\ (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) & \
|
|
1039 |
\ (! Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) & \
|
|
1040 |
\ (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) & \
|
|
1041 |
\ (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) & \
|
|
1042 |
\ (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) & \
|
|
1043 |
\ (! X Y W Z. equal(X::'a,Y) & product(X::'a,W,Z) --> product(Y::'a,W,Z)) & \
|
|
1044 |
\ (! X W Y Z. equal(X::'a,Y) & product(W::'a,X,Z) --> product(W::'a,Y,Z)) & \
|
|
1045 |
\ (! X W Z Y. equal(X::'a,Y) & product(W::'a,Z,X) --> product(W::'a,Z,Y)) & \
|
|
1046 |
\ (! X. product(X::'a,X,identity)) & \
|
|
1047 |
\ (product(a::'a,b,c)) & \
|
|
1048 |
\ (~product(b::'a,a,c)) --> False",
|
|
1049 |
meson_tac);
|
|
1050 |
****************)
|
|
1051 |
|
|
1052 |
(*2386 inferences so far. Searching to depth 11. 8.7 secs*)
|
|
1053 |
val GRP008_1 = prove_hard
|
|
1054 |
("(! X. equal(X::'a,X)) & \
|
|
1055 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
1056 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
1057 |
\ (! X. product(identity::'a,X,X)) & \
|
|
1058 |
\ (! X. product(X::'a,identity,X)) & \
|
|
1059 |
\ (! X. product(inverse(X),X,identity)) & \
|
|
1060 |
\ (! X. product(X::'a,inverse(X),identity)) & \
|
|
1061 |
\ (! X Y. product(X::'a,Y,multiply(X::'a,Y))) & \
|
|
1062 |
\ (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) & \
|
|
1063 |
\ (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) & \
|
|
1064 |
\ (! Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) & \
|
|
1065 |
\ (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) & \
|
|
1066 |
\ (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) & \
|
|
1067 |
\ (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) & \
|
|
1068 |
\ (! X Y W Z. equal(X::'a,Y) & product(X::'a,W,Z) --> product(Y::'a,W,Z)) & \
|
|
1069 |
\ (! X W Y Z. equal(X::'a,Y) & product(W::'a,X,Z) --> product(W::'a,Y,Z)) & \
|
|
1070 |
\ (! X W Z Y. equal(X::'a,Y) & product(W::'a,Z,X) --> product(W::'a,Z,Y)) & \
|
|
1071 |
\ (! A B. equal(A::'a,B) --> equal(h(A),h(B))) & \
|
|
1072 |
\ (! C D. equal(C::'a,D) --> equal(j(C),j(D))) & \
|
|
1073 |
\ (! A B. equal(A::'a,B) & q(A) --> q(B)) & \
|
|
1074 |
\ (! B A C. q(A) & product(A::'a,B,C) --> product(B::'a,A,C)) & \
|
|
1075 |
\ (! A. product(j(A),A,h(A)) | product(A::'a,j(A),h(A)) | q(A)) & \
|
|
1076 |
\ (! A. product(j(A),A,h(A)) & product(A::'a,j(A),h(A)) --> q(A)) & \
|
|
1077 |
\ (~q(identity)) --> False",
|
|
1078 |
meson_tac);
|
|
1079 |
|
|
1080 |
(*8625 inferences so far. Searching to depth 11. 20 secs*)
|
|
1081 |
val GRP013_1 = prove_hard
|
|
1082 |
("(! X. equal(X::'a,X)) & \
|
|
1083 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
1084 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
1085 |
\ (! X. product(identity::'a,X,X)) & \
|
|
1086 |
\ (! X. product(X::'a,identity,X)) & \
|
|
1087 |
\ (! X. product(inverse(X),X,identity)) & \
|
|
1088 |
\ (! X. product(X::'a,inverse(X),identity)) & \
|
|
1089 |
\ (! X Y. product(X::'a,Y,multiply(X::'a,Y))) & \
|
|
1090 |
\ (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) & \
|
|
1091 |
\ (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) & \
|
|
1092 |
\ (! Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) & \
|
|
1093 |
\ (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) & \
|
|
1094 |
\ (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) & \
|
|
1095 |
\ (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) & \
|
|
1096 |
\ (! X Y W Z. equal(X::'a,Y) & product(X::'a,W,Z) --> product(Y::'a,W,Z)) & \
|
|
1097 |
\ (! X W Y Z. equal(X::'a,Y) & product(W::'a,X,Z) --> product(W::'a,Y,Z)) & \
|
|
1098 |
\ (! X W Z Y. equal(X::'a,Y) & product(W::'a,Z,X) --> product(W::'a,Z,Y)) & \
|
|
1099 |
\ (! A. product(A::'a,A,identity)) & \
|
|
1100 |
\ (product(a::'a,b,c)) & \
|
|
1101 |
\ (product(inverse(a),inverse(b),d)) & \
|
|
1102 |
\ (! A C B. product(inverse(A),inverse(B),C) --> product(A::'a,C,B)) & \
|
|
1103 |
\ (~product(c::'a,d,identity)) --> False",
|
|
1104 |
meson_tac);
|
|
1105 |
|
|
1106 |
(*2448 inferences so far. Searching to depth 10. 7.2 secs*)
|
|
1107 |
val GRP037_3 = prove_hard
|
|
1108 |
("(! X. equal(X::'a,X)) & \
|
|
1109 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
1110 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
1111 |
\ (! X. product(identity::'a,X,X)) & \
|
|
1112 |
\ (! X. product(X::'a,identity,X)) & \
|
|
1113 |
\ (! X. product(inverse(X),X,identity)) & \
|
|
1114 |
\ (! X. product(X::'a,inverse(X),identity)) & \
|
|
1115 |
\ (! X Y. product(X::'a,Y,multiply(X::'a,Y))) & \
|
|
1116 |
\ (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) & \
|
|
1117 |
\ (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) & \
|
|
1118 |
\ (! Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) & \
|
|
1119 |
\ (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) & \
|
|
1120 |
\ (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) & \
|
|
1121 |
\ (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) & \
|
|
1122 |
\ (! X Y W Z. equal(X::'a,Y) & product(X::'a,W,Z) --> product(Y::'a,W,Z)) & \
|
|
1123 |
\ (! X W Y Z. equal(X::'a,Y) & product(W::'a,X,Z) --> product(W::'a,Y,Z)) & \
|
|
1124 |
\ (! X W Z Y. equal(X::'a,Y) & product(W::'a,Z,X) --> product(W::'a,Z,Y)) & \
|
|
1125 |
\ (! A B C. subgroup_member(A) & subgroup_member(B) & product(A::'a,inverse(B),C) --> subgroup_member(C)) & \
|
|
1126 |
\ (! A B. equal(A::'a,B) & subgroup_member(A) --> subgroup_member(B)) & \
|
|
1127 |
\ (! A. subgroup_member(A) --> product(another_identity::'a,A,A)) & \
|
|
1128 |
\ (! A. subgroup_member(A) --> product(A::'a,another_identity,A)) & \
|
|
1129 |
\ (! A. subgroup_member(A) --> product(A::'a,another_inverse(A),another_identity)) & \
|
|
1130 |
\ (! A. subgroup_member(A) --> product(another_inverse(A),A,another_identity)) & \
|
|
1131 |
\ (! A. subgroup_member(A) --> subgroup_member(another_inverse(A))) & \
|
|
1132 |
\ (! A B. equal(A::'a,B) --> equal(another_inverse(A),another_inverse(B))) & \
|
|
1133 |
\ (! A C D B. product(A::'a,B,C) & product(A::'a,D,C) --> equal(D::'a,B)) & \
|
|
1134 |
\ (! B C D A. product(A::'a,B,C) & product(D::'a,B,C) --> equal(D::'a,A)) & \
|
|
1135 |
\ (subgroup_member(a)) & \
|
|
1136 |
\ (subgroup_member(another_identity)) & \
|
|
1137 |
\ (~equal(inverse(a),another_inverse(a))) --> False",
|
|
1138 |
meson_tac);
|
|
1139 |
|
|
1140 |
(*163 inferences so far. Searching to depth 11. 0.3 secs*)
|
|
1141 |
val GRP031_2 = prove
|
|
1142 |
("(! X Y. product(X::'a,Y,multiply(X::'a,Y))) & \
|
|
1143 |
\ (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) & \
|
|
1144 |
\ (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) & \
|
|
1145 |
\ (! Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) & \
|
|
1146 |
\ (! A. product(A::'a,inverse(A),identity)) & \
|
|
1147 |
\ (! A. product(A::'a,identity,A)) & \
|
|
1148 |
\ (! A. ~product(A::'a,a,identity)) --> False",
|
|
1149 |
meson_tac);
|
|
1150 |
|
|
1151 |
(*47 inferences so far. Searching to depth 11. 0.2 secs*)
|
|
1152 |
val GRP034_4 = prove
|
|
1153 |
("(! X Y. product(X::'a,Y,multiply(X::'a,Y))) & \
|
|
1154 |
\ (! X. product(identity::'a,X,X)) & \
|
|
1155 |
\ (! X. product(X::'a,identity,X)) & \
|
|
1156 |
\ (! X. product(X::'a,inverse(X),identity)) & \
|
|
1157 |
\ (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) & \
|
|
1158 |
\ (! Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) & \
|
|
1159 |
\ (! B A C. subgroup_member(A) & subgroup_member(B) & product(B::'a,inverse(A),C) --> subgroup_member(C)) & \
|
|
1160 |
\ (subgroup_member(a)) & \
|
|
1161 |
\ (~subgroup_member(inverse(a))) --> False",
|
|
1162 |
meson_tac);
|
|
1163 |
|
|
1164 |
(*3287 inferences so far. Searching to depth 14. 3.5 secs*)
|
|
1165 |
val GRP047_2 = prove_hard
|
|
1166 |
("(! X. product(identity::'a,X,X)) & \
|
|
1167 |
\ (! X. product(inverse(X),X,identity)) & \
|
|
1168 |
\ (! X Y. product(X::'a,Y,multiply(X::'a,Y))) & \
|
|
1169 |
\ (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) & \
|
|
1170 |
\ (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) & \
|
|
1171 |
\ (! Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) & \
|
|
1172 |
\ (! X W Z Y. equal(X::'a,Y) & product(W::'a,Z,X) --> product(W::'a,Z,Y)) & \
|
|
1173 |
\ (equal(a::'a,b)) & \
|
|
1174 |
\ (~equal(multiply(c::'a,a),multiply(c::'a,b))) --> False",
|
|
1175 |
meson_tac);
|
|
1176 |
|
|
1177 |
(*25559 inferences so far. Searching to depth 19. 16.9 secs*)
|
|
1178 |
val GRP130_1_002 = prove_hard
|
|
1179 |
("(group_element(e_1)) & \
|
|
1180 |
\ (group_element(e_2)) & \
|
|
1181 |
\ (~equal(e_1::'a,e_2)) & \
|
|
1182 |
\ (~equal(e_2::'a,e_1)) & \
|
|
1183 |
\ (! X Y. group_element(X) & group_element(Y) --> product(X::'a,Y,e_1) | product(X::'a,Y,e_2)) & \
|
|
1184 |
\ (! X Y W Z. product(X::'a,Y,W) & product(X::'a,Y,Z) --> equal(W::'a,Z)) & \
|
|
1185 |
\ (! X Y W Z. product(X::'a,W,Y) & product(X::'a,Z,Y) --> equal(W::'a,Z)) & \
|
|
1186 |
\ (! Y X W Z. product(W::'a,Y,X) & product(Z::'a,Y,X) --> equal(W::'a,Z)) & \
|
|
1187 |
\ (! Z1 Z2 Y X. product(X::'a,Y,Z1) & product(X::'a,Z1,Z2) --> product(Z2::'a,Y,X)) --> False",
|
|
1188 |
meson_tac);
|
|
1189 |
|
|
1190 |
(*3468 inferences so far. Searching to depth 10. 9.1 secs*)
|
|
1191 |
val GRP156_1 = prove_hard
|
|
1192 |
("(! X. equal(X::'a,X)) & \
|
|
1193 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
1194 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
1195 |
\ (! X. equal(multiply(identity::'a,X),X)) & \
|
|
1196 |
\ (! X. equal(multiply(inverse(X),X),identity)) & \
|
|
1197 |
\ (! X Y Z. equal(multiply(multiply(X::'a,Y),Z),multiply(X::'a,multiply(Y::'a,Z)))) & \
|
|
1198 |
\ (! A B. equal(A::'a,B) --> equal(inverse(A),inverse(B))) & \
|
|
1199 |
\ (! C D E. equal(C::'a,D) --> equal(multiply(C::'a,E),multiply(D::'a,E))) & \
|
|
1200 |
\ (! F' H G. equal(F'::'a,G) --> equal(multiply(H::'a,F'),multiply(H::'a,G))) & \
|
|
1201 |
\ (! Y X. equal(greatest_lower_bound(X::'a,Y),greatest_lower_bound(Y::'a,X))) & \
|
|
1202 |
\ (! Y X. equal(least_upper_bound(X::'a,Y),least_upper_bound(Y::'a,X))) & \
|
|
1203 |
\ (! X Y Z. equal(greatest_lower_bound(X::'a,greatest_lower_bound(Y::'a,Z)),greatest_lower_bound(greatest_lower_bound(X::'a,Y),Z))) & \
|
|
1204 |
\ (! X Y Z. equal(least_upper_bound(X::'a,least_upper_bound(Y::'a,Z)),least_upper_bound(least_upper_bound(X::'a,Y),Z))) & \
|
|
1205 |
\ (! X. equal(least_upper_bound(X::'a,X),X)) & \
|
|
1206 |
\ (! X. equal(greatest_lower_bound(X::'a,X),X)) & \
|
|
1207 |
\ (! Y X. equal(least_upper_bound(X::'a,greatest_lower_bound(X::'a,Y)),X)) & \
|
|
1208 |
\ (! Y X. equal(greatest_lower_bound(X::'a,least_upper_bound(X::'a,Y)),X)) & \
|
|
1209 |
\ (! Y X Z. equal(multiply(X::'a,least_upper_bound(Y::'a,Z)),least_upper_bound(multiply(X::'a,Y),multiply(X::'a,Z)))) & \
|
|
1210 |
\ (! Y X Z. equal(multiply(X::'a,greatest_lower_bound(Y::'a,Z)),greatest_lower_bound(multiply(X::'a,Y),multiply(X::'a,Z)))) & \
|
|
1211 |
\ (! Y Z X. equal(multiply(least_upper_bound(Y::'a,Z),X),least_upper_bound(multiply(Y::'a,X),multiply(Z::'a,X)))) & \
|
|
1212 |
\ (! Y Z X. equal(multiply(greatest_lower_bound(Y::'a,Z),X),greatest_lower_bound(multiply(Y::'a,X),multiply(Z::'a,X)))) & \
|
|
1213 |
\ (! A B C. equal(A::'a,B) --> equal(greatest_lower_bound(A::'a,C),greatest_lower_bound(B::'a,C))) & \
|
|
1214 |
\ (! A C B. equal(A::'a,B) --> equal(greatest_lower_bound(C::'a,A),greatest_lower_bound(C::'a,B))) & \
|
|
1215 |
\ (! A B C. equal(A::'a,B) --> equal(least_upper_bound(A::'a,C),least_upper_bound(B::'a,C))) & \
|
|
1216 |
\ (! A C B. equal(A::'a,B) --> equal(least_upper_bound(C::'a,A),least_upper_bound(C::'a,B))) & \
|
|
1217 |
\ (! A B C. equal(A::'a,B) --> equal(multiply(A::'a,C),multiply(B::'a,C))) & \
|
|
1218 |
\ (! A C B. equal(A::'a,B) --> equal(multiply(C::'a,A),multiply(C::'a,B))) & \
|
|
1219 |
\ (equal(least_upper_bound(a::'a,b),b)) & \
|
|
1220 |
\ (~equal(greatest_lower_bound(multiply(a::'a,c),multiply(b::'a,c)),multiply(a::'a,c))) --> False",
|
|
1221 |
meson_tac);
|
|
1222 |
|
|
1223 |
(*4394 inferences so far. Searching to depth 10. 8.2 secs*)
|
|
1224 |
val GRP168_1 = prove_hard
|
|
1225 |
("(! X. equal(X::'a,X)) & \
|
|
1226 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
1227 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
1228 |
\ (! X. equal(multiply(identity::'a,X),X)) & \
|
|
1229 |
\ (! X. equal(multiply(inverse(X),X),identity)) & \
|
|
1230 |
\ (! X Y Z. equal(multiply(multiply(X::'a,Y),Z),multiply(X::'a,multiply(Y::'a,Z)))) & \
|
|
1231 |
\ (! A B. equal(A::'a,B) --> equal(inverse(A),inverse(B))) & \
|
|
1232 |
\ (! C D E. equal(C::'a,D) --> equal(multiply(C::'a,E),multiply(D::'a,E))) & \
|
|
1233 |
\ (! F' H G. equal(F'::'a,G) --> equal(multiply(H::'a,F'),multiply(H::'a,G))) & \
|
|
1234 |
\ (! Y X. equal(greatest_lower_bound(X::'a,Y),greatest_lower_bound(Y::'a,X))) & \
|
|
1235 |
\ (! Y X. equal(least_upper_bound(X::'a,Y),least_upper_bound(Y::'a,X))) & \
|
|
1236 |
\ (! X Y Z. equal(greatest_lower_bound(X::'a,greatest_lower_bound(Y::'a,Z)),greatest_lower_bound(greatest_lower_bound(X::'a,Y),Z))) & \
|
|
1237 |
\ (! X Y Z. equal(least_upper_bound(X::'a,least_upper_bound(Y::'a,Z)),least_upper_bound(least_upper_bound(X::'a,Y),Z))) & \
|
|
1238 |
\ (! X. equal(least_upper_bound(X::'a,X),X)) & \
|
|
1239 |
\ (! X. equal(greatest_lower_bound(X::'a,X),X)) & \
|
|
1240 |
\ (! Y X. equal(least_upper_bound(X::'a,greatest_lower_bound(X::'a,Y)),X)) & \
|
|
1241 |
\ (! Y X. equal(greatest_lower_bound(X::'a,least_upper_bound(X::'a,Y)),X)) & \
|
|
1242 |
\ (! Y X Z. equal(multiply(X::'a,least_upper_bound(Y::'a,Z)),least_upper_bound(multiply(X::'a,Y),multiply(X::'a,Z)))) & \
|
|
1243 |
\ (! Y X Z. equal(multiply(X::'a,greatest_lower_bound(Y::'a,Z)),greatest_lower_bound(multiply(X::'a,Y),multiply(X::'a,Z)))) & \
|
|
1244 |
\ (! Y Z X. equal(multiply(least_upper_bound(Y::'a,Z),X),least_upper_bound(multiply(Y::'a,X),multiply(Z::'a,X)))) & \
|
|
1245 |
\ (! Y Z X. equal(multiply(greatest_lower_bound(Y::'a,Z),X),greatest_lower_bound(multiply(Y::'a,X),multiply(Z::'a,X)))) & \
|
|
1246 |
\ (! A B C. equal(A::'a,B) --> equal(greatest_lower_bound(A::'a,C),greatest_lower_bound(B::'a,C))) & \
|
|
1247 |
\ (! A C B. equal(A::'a,B) --> equal(greatest_lower_bound(C::'a,A),greatest_lower_bound(C::'a,B))) & \
|
|
1248 |
\ (! A B C. equal(A::'a,B) --> equal(least_upper_bound(A::'a,C),least_upper_bound(B::'a,C))) & \
|
|
1249 |
\ (! A C B. equal(A::'a,B) --> equal(least_upper_bound(C::'a,A),least_upper_bound(C::'a,B))) & \
|
|
1250 |
\ (! A B C. equal(A::'a,B) --> equal(multiply(A::'a,C),multiply(B::'a,C))) & \
|
|
1251 |
\ (! A C B. equal(A::'a,B) --> equal(multiply(C::'a,A),multiply(C::'a,B))) & \
|
|
1252 |
\ (equal(least_upper_bound(a::'a,b),b)) & \
|
|
1253 |
\ (~equal(least_upper_bound(multiply(inverse(c),multiply(a::'a,c)),multiply(inverse(c),multiply(b::'a,c))),multiply(inverse(c),multiply(b::'a,c)))) --> False",
|
|
1254 |
meson_tac);
|
|
1255 |
|
|
1256 |
(*250258 inferences so far. Searching to depth 16. 406.2 secs*)
|
|
1257 |
val HEN003_3 = prove_hard
|
|
1258 |
("(! X. equal(X::'a,X)) & \
|
|
1259 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
1260 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
1261 |
\ (! X Y. less_equal(X::'a,Y) --> equal(divide(X::'a,Y),zero)) & \
|
|
1262 |
\ (! X Y. equal(divide(X::'a,Y),zero) --> less_equal(X::'a,Y)) & \
|
|
1263 |
\ (! Y X. less_equal(divide(X::'a,Y),X)) & \
|
|
1264 |
\ (! X Y Z. less_equal(divide(divide(X::'a,Z),divide(Y::'a,Z)),divide(divide(X::'a,Y),Z))) & \
|
|
1265 |
\ (! X. less_equal(zero::'a,X)) & \
|
|
1266 |
\ (! X Y. less_equal(X::'a,Y) & less_equal(Y::'a,X) --> equal(X::'a,Y)) & \
|
|
1267 |
\ (! X. less_equal(X::'a,identity)) & \
|
|
1268 |
\ (! A B C. equal(A::'a,B) --> equal(divide(A::'a,C),divide(B::'a,C))) & \
|
|
1269 |
\ (! D F' E. equal(D::'a,E) --> equal(divide(F'::'a,D),divide(F'::'a,E))) & \
|
|
1270 |
\ (! G H I'. equal(G::'a,H) & less_equal(G::'a,I') --> less_equal(H::'a,I')) & \
|
|
1271 |
\ (! J L K'. equal(J::'a,K') & less_equal(L::'a,J) --> less_equal(L::'a,K')) & \
|
|
1272 |
\ (~equal(divide(a::'a,a),zero)) --> False",
|
|
1273 |
meson_tac);
|
|
1274 |
|
|
1275 |
|
|
1276 |
(*202177 inferences so far. Searching to depth 14. 451 secs*)
|
|
1277 |
val HEN007_2 = prove_hard
|
|
1278 |
("(! X. equal(X::'a,X)) & \
|
|
1279 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
1280 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
1281 |
\ (! X Y. less_equal(X::'a,Y) --> quotient(X::'a,Y,zero)) & \
|
|
1282 |
\ (! X Y. quotient(X::'a,Y,zero) --> less_equal(X::'a,Y)) & \
|
|
1283 |
\ (! Y Z X. quotient(X::'a,Y,Z) --> less_equal(Z::'a,X)) & \
|
|
1284 |
\ (! Y X V3 V2 V1 Z V4 V5. quotient(X::'a,Y,V1) & quotient(Y::'a,Z,V2) & quotient(X::'a,Z,V3) & quotient(V3::'a,V2,V4) & quotient(V1::'a,Z,V5) --> less_equal(V4::'a,V5)) & \
|
|
1285 |
\ (! X. less_equal(zero::'a,X)) & \
|
|
1286 |
\ (! X Y. less_equal(X::'a,Y) & less_equal(Y::'a,X) --> equal(X::'a,Y)) & \
|
|
1287 |
\ (! X. less_equal(X::'a,identity)) & \
|
|
1288 |
\ (! X Y. quotient(X::'a,Y,divide(X::'a,Y))) & \
|
|
1289 |
\ (! X Y Z W. quotient(X::'a,Y,Z) & quotient(X::'a,Y,W) --> equal(Z::'a,W)) & \
|
|
1290 |
\ (! X Y W Z. equal(X::'a,Y) & quotient(X::'a,W,Z) --> quotient(Y::'a,W,Z)) & \
|
|
1291 |
\ (! X W Y Z. equal(X::'a,Y) & quotient(W::'a,X,Z) --> quotient(W::'a,Y,Z)) & \
|
|
1292 |
\ (! X W Z Y. equal(X::'a,Y) & quotient(W::'a,Z,X) --> quotient(W::'a,Z,Y)) & \
|
|
1293 |
\ (! X Z Y. equal(X::'a,Y) & less_equal(Z::'a,X) --> less_equal(Z::'a,Y)) & \
|
|
1294 |
\ (! X Y Z. equal(X::'a,Y) & less_equal(X::'a,Z) --> less_equal(Y::'a,Z)) & \
|
|
1295 |
\ (! X Y W. equal(X::'a,Y) --> equal(divide(X::'a,W),divide(Y::'a,W))) & \
|
|
1296 |
\ (! X W Y. equal(X::'a,Y) --> equal(divide(W::'a,X),divide(W::'a,Y))) & \
|
|
1297 |
\ (! X. quotient(X::'a,identity,zero)) & \
|
|
1298 |
\ (! X. quotient(zero::'a,X,zero)) & \
|
|
1299 |
\ (! X. quotient(X::'a,X,zero)) & \
|
|
1300 |
\ (! X. quotient(X::'a,zero,X)) & \
|
|
1301 |
\ (! Y X Z. less_equal(X::'a,Y) & less_equal(Y::'a,Z) --> less_equal(X::'a,Z)) & \
|
|
1302 |
\ (! W1 X Z W2 Y. quotient(X::'a,Y,W1) & less_equal(W1::'a,Z) & quotient(X::'a,Z,W2) --> less_equal(W2::'a,Y)) & \
|
|
1303 |
\ (less_equal(x::'a,y)) & \
|
|
1304 |
\ (quotient(z::'a,y,zQy)) & \
|
|
1305 |
\ (quotient(z::'a,x,zQx)) & \
|
|
1306 |
\ (~less_equal(zQy::'a,zQx)) --> False",
|
|
1307 |
meson_tac);
|
|
1308 |
|
|
1309 |
(*60026 inferences so far. Searching to depth 12. 42.2 secs*)
|
|
1310 |
val HEN008_4 = prove_hard
|
|
1311 |
("(! X. equal(X::'a,X)) & \
|
|
1312 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
1313 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
1314 |
\ (! X Y. less_equal(X::'a,Y) --> equal(divide(X::'a,Y),zero)) & \
|
|
1315 |
\ (! X Y. equal(divide(X::'a,Y),zero) --> less_equal(X::'a,Y)) & \
|
|
1316 |
\ (! Y X. less_equal(divide(X::'a,Y),X)) & \
|
|
1317 |
\ (! X Y Z. less_equal(divide(divide(X::'a,Z),divide(Y::'a,Z)),divide(divide(X::'a,Y),Z))) & \
|
|
1318 |
\ (! X. less_equal(zero::'a,X)) & \
|
|
1319 |
\ (! X Y. less_equal(X::'a,Y) & less_equal(Y::'a,X) --> equal(X::'a,Y)) & \
|
|
1320 |
\ (! X. less_equal(X::'a,identity)) & \
|
|
1321 |
\ (! A B C. equal(A::'a,B) --> equal(divide(A::'a,C),divide(B::'a,C))) & \
|
|
1322 |
\ (! D F' E. equal(D::'a,E) --> equal(divide(F'::'a,D),divide(F'::'a,E))) & \
|
|
1323 |
\ (! G H I'. equal(G::'a,H) & less_equal(G::'a,I') --> less_equal(H::'a,I')) & \
|
|
1324 |
\ (! J L K'. equal(J::'a,K') & less_equal(L::'a,J) --> less_equal(L::'a,K')) & \
|
|
1325 |
\ (! X. equal(divide(X::'a,identity),zero)) & \
|
|
1326 |
\ (! X. equal(divide(zero::'a,X),zero)) & \
|
|
1327 |
\ (! X. equal(divide(X::'a,X),zero)) & \
|
|
1328 |
\ (equal(divide(a::'a,zero),a)) & \
|
|
1329 |
\ (! Y X Z. less_equal(X::'a,Y) & less_equal(Y::'a,Z) --> less_equal(X::'a,Z)) & \
|
|
1330 |
\ (! X Z Y. less_equal(divide(X::'a,Y),Z) --> less_equal(divide(X::'a,Z),Y)) & \
|
|
1331 |
\ (! Y Z X. less_equal(X::'a,Y) --> less_equal(divide(Z::'a,Y),divide(Z::'a,X))) & \
|
|
1332 |
\ (less_equal(a::'a,b)) & \
|
|
1333 |
\ (~less_equal(divide(a::'a,c),divide(b::'a,c))) --> False",
|
|
1334 |
meson_tac);
|
|
1335 |
|
|
1336 |
|
|
1337 |
(*3160 inferences so far. Searching to depth 11. 3.5 secs*)
|
|
1338 |
val HEN009_5 = prove_hard
|
|
1339 |
("(! X. equal(X::'a,X)) & \
|
|
1340 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
1341 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
1342 |
\ (! Y X. equal(divide(divide(X::'a,Y),X),zero)) & \
|
|
1343 |
\ (! X Y Z. equal(divide(divide(divide(X::'a,Z),divide(Y::'a,Z)),divide(divide(X::'a,Y),Z)),zero)) & \
|
|
1344 |
\ (! X. equal(divide(zero::'a,X),zero)) & \
|
|
1345 |
\ (! X Y. equal(divide(X::'a,Y),zero) & equal(divide(Y::'a,X),zero) --> equal(X::'a,Y)) & \
|
|
1346 |
\ (! X. equal(divide(X::'a,identity),zero)) & \
|
|
1347 |
\ (! A B C. equal(A::'a,B) --> equal(divide(A::'a,C),divide(B::'a,C))) & \
|
|
1348 |
\ (! D F' E. equal(D::'a,E) --> equal(divide(F'::'a,D),divide(F'::'a,E))) & \
|
|
1349 |
\ (! Y X Z. equal(divide(X::'a,Y),zero) & equal(divide(Y::'a,Z),zero) --> equal(divide(X::'a,Z),zero)) & \
|
|
1350 |
\ (! X Z Y. equal(divide(divide(X::'a,Y),Z),zero) --> equal(divide(divide(X::'a,Z),Y),zero)) & \
|
|
1351 |
\ (! Y Z X. equal(divide(X::'a,Y),zero) --> equal(divide(divide(Z::'a,Y),divide(Z::'a,X)),zero)) & \
|
|
1352 |
\ (~equal(divide(identity::'a,a),divide(identity::'a,divide(identity::'a,divide(identity::'a,a))))) & \
|
|
1353 |
\ (equal(divide(identity::'a,a),b)) & \
|
|
1354 |
\ (equal(divide(identity::'a,b),c)) & \
|
|
1355 |
\ (equal(divide(identity::'a,c),d)) & \
|
|
1356 |
\ (~equal(b::'a,d)) --> False",
|
|
1357 |
meson_tac);
|
|
1358 |
|
|
1359 |
(*970373 inferences so far. Searching to depth 17. 890.0 secs*)
|
|
1360 |
val HEN012_3 = prove_hard
|
|
1361 |
("(! X. equal(X::'a,X)) & \
|
|
1362 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
1363 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
1364 |
\ (! X Y. less_equal(X::'a,Y) --> equal(divide(X::'a,Y),zero)) & \
|
|
1365 |
\ (! X Y. equal(divide(X::'a,Y),zero) --> less_equal(X::'a,Y)) & \
|
|
1366 |
\ (! Y X. less_equal(divide(X::'a,Y),X)) & \
|
|
1367 |
\ (! X Y Z. less_equal(divide(divide(X::'a,Z),divide(Y::'a,Z)),divide(divide(X::'a,Y),Z))) & \
|
|
1368 |
\ (! X. less_equal(zero::'a,X)) & \
|
|
1369 |
\ (! X Y. less_equal(X::'a,Y) & less_equal(Y::'a,X) --> equal(X::'a,Y)) & \
|
|
1370 |
\ (! X. less_equal(X::'a,identity)) & \
|
|
1371 |
\ (! A B C. equal(A::'a,B) --> equal(divide(A::'a,C),divide(B::'a,C))) & \
|
|
1372 |
\ (! D F' E. equal(D::'a,E) --> equal(divide(F'::'a,D),divide(F'::'a,E))) & \
|
|
1373 |
\ (! G H I'. equal(G::'a,H) & less_equal(G::'a,I') --> less_equal(H::'a,I')) & \
|
|
1374 |
\ (! J L K'. equal(J::'a,K') & less_equal(L::'a,J) --> less_equal(L::'a,K')) & \
|
|
1375 |
\ (~less_equal(a::'a,a)) --> False",
|
|
1376 |
meson_tac);
|
|
1377 |
|
|
1378 |
|
|
1379 |
(*1063 inferences so far. Searching to depth 20. 1.0 secs*)
|
|
1380 |
val LCL010_1 = prove
|
|
1381 |
("(! X Y. is_a_theorem(equivalent(X::'a,Y)) & is_a_theorem(X) --> is_a_theorem(Y)) & \
|
|
1382 |
\ (! X Z Y. is_a_theorem(equivalent(equivalent(X::'a,Y),equivalent(equivalent(X::'a,Z),equivalent(Z::'a,Y))))) & \
|
|
1383 |
\ (~is_a_theorem(equivalent(equivalent(a::'a,b),equivalent(equivalent(c::'a,b),equivalent(a::'a,c))))) --> False",
|
|
1384 |
meson_tac);
|
|
1385 |
|
|
1386 |
(*2549 inferences so far. Searching to depth 12. 1.4 secs*)
|
|
1387 |
val LCL077_2 = prove
|
|
1388 |
("(! X Y. is_a_theorem(implies(X,Y)) & is_a_theorem(X) --> is_a_theorem(Y)) & \
|
|
1389 |
\ (! Y X. is_a_theorem(implies(X,implies(Y,X)))) & \
|
|
1390 |
\ (! Y X Z. is_a_theorem(implies(implies(X,implies(Y,Z)),implies(implies(X,Y),implies(X,Z))))) & \
|
|
1391 |
\ (! Y X. is_a_theorem(implies(implies(not(X),not(Y)),implies(Y,X)))) & \
|
|
1392 |
\ (! X2 X1 X3. is_a_theorem(implies(X1,X2)) & is_a_theorem(implies(X2,X3)) --> is_a_theorem(implies(X1,X3))) & \
|
|
1393 |
\ (~is_a_theorem(implies(not(not(a)),a))) --> False",
|
|
1394 |
meson_tac);
|
|
1395 |
|
|
1396 |
(*2036 inferences so far. Searching to depth 20. 1.5 secs*)
|
|
1397 |
val LCL082_1 = prove
|
|
1398 |
("(! X Y. is_a_theorem(implies(X::'a,Y)) & is_a_theorem(X) --> is_a_theorem(Y)) & \
|
|
1399 |
\ (! Y Z U X. is_a_theorem(implies(implies(implies(X::'a,Y),Z),implies(implies(Z::'a,X),implies(U::'a,X))))) & \
|
|
1400 |
\ (~is_a_theorem(implies(a::'a,implies(b::'a,a)))) --> False",
|
|
1401 |
meson_tac);
|
|
1402 |
|
|
1403 |
(*1100 inferences so far. Searching to depth 13. 1.0 secs*)
|
|
1404 |
val LCL111_1 = prove
|
|
1405 |
("(! X Y. is_a_theorem(implies(X,Y)) & is_a_theorem(X) --> is_a_theorem(Y)) & \
|
|
1406 |
\ (! Y X. is_a_theorem(implies(X,implies(Y,X)))) & \
|
|
1407 |
\ (! Y X Z. is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))))) & \
|
|
1408 |
\ (! Y X. is_a_theorem(implies(implies(implies(X,Y),Y),implies(implies(Y,X),X)))) & \
|
|
1409 |
\ (! Y X. is_a_theorem(implies(implies(not(X),not(Y)),implies(Y,X)))) & \
|
|
1410 |
\ (~is_a_theorem(implies(implies(a,b),implies(implies(c,a),implies(c,b))))) --> False",
|
|
1411 |
meson_tac);
|
|
1412 |
|
|
1413 |
(*667 inferences so far. Searching to depth 9. 1.4 secs*)
|
|
1414 |
val LCL143_1 = prove
|
|
1415 |
("(! X. equal(X,X)) & \
|
|
1416 |
\ (! Y X. equal(X,Y) --> equal(Y,X)) & \
|
|
1417 |
\ (! Y X Z. equal(X,Y) & equal(Y,Z) --> equal(X,Z)) & \
|
|
1418 |
\ (! X. equal(implies(true,X),X)) & \
|
|
1419 |
\ (! Y X Z. equal(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))),true)) & \
|
|
1420 |
\ (! Y X. equal(implies(implies(X,Y),Y),implies(implies(Y,X),X))) & \
|
|
1421 |
\ (! Y X. equal(implies(implies(not(X),not(Y)),implies(Y,X)),true)) & \
|
|
1422 |
\ (! A B C. equal(A,B) --> equal(implies(A,C),implies(B,C))) & \
|
|
1423 |
\ (! D F' E. equal(D,E) --> equal(implies(F',D),implies(F',E))) & \
|
|
1424 |
\ (! G H. equal(G,H) --> equal(not(G),not(H))) & \
|
|
1425 |
\ (! X Y. equal(big_V(X,Y),implies(implies(X,Y),Y))) & \
|
|
1426 |
\ (! X Y. equal(big_hat(X,Y),not(big_V(not(X),not(Y))))) & \
|
|
1427 |
\ (! X Y. ordered(X,Y) --> equal(implies(X,Y),true)) & \
|
|
1428 |
\ (! X Y. equal(implies(X,Y),true) --> ordered(X,Y)) & \
|
|
1429 |
\ (! A B C. equal(A,B) --> equal(big_V(A,C),big_V(B,C))) & \
|
|
1430 |
\ (! D F' E. equal(D,E) --> equal(big_V(F',D),big_V(F',E))) & \
|
|
1431 |
\ (! G H I'. equal(G,H) --> equal(big_hat(G,I'),big_hat(H,I'))) & \
|
|
1432 |
\ (! J L K'. equal(J,K') --> equal(big_hat(L,J),big_hat(L,K'))) & \
|
|
1433 |
\ (! M N O_. equal(M,N) & ordered(M,O_) --> ordered(N,O_)) & \
|
|
1434 |
\ (! P R Q. equal(P,Q) & ordered(R,P) --> ordered(R,Q)) & \
|
|
1435 |
\ (ordered(x,y)) & \
|
|
1436 |
\ (~ordered(implies(z,x),implies(z,y))) --> False",
|
|
1437 |
meson_tac);
|
|
1438 |
|
|
1439 |
(*5245 inferences so far. Searching to depth 12. 4.6 secs*)
|
|
1440 |
val LCL182_1 = prove_hard
|
|
1441 |
("(! A. axiom(or(not(or(A,A)),A))) & \
|
|
1442 |
\ (! B A. axiom(or(not(A),or(B,A)))) & \
|
|
1443 |
\ (! B A. axiom(or(not(or(A,B)),or(B,A)))) & \
|
|
1444 |
\ (! B A C. axiom(or(not(or(A,or(B,C))),or(B,or(A,C))))) & \
|
|
1445 |
\ (! A C B. axiom(or(not(or(not(A),B)),or(not(or(C,A)),or(C,B))))) & \
|
|
1446 |
\ (! X. axiom(X) --> theorem(X)) & \
|
|
1447 |
\ (! X Y. axiom(or(not(Y),X)) & theorem(Y) --> theorem(X)) & \
|
|
1448 |
\ (! X Y Z. axiom(or(not(X),Y)) & theorem(or(not(Y),Z)) --> theorem(or(not(X),Z))) & \
|
|
1449 |
\ (~theorem(or(not(or(not(p),q)),or(not(not(q)),not(p))))) --> False",
|
|
1450 |
meson_tac);
|
|
1451 |
|
|
1452 |
(*410 inferences so far. Searching to depth 10. 0.3 secs*)
|
|
1453 |
val LCL200_1 = prove
|
|
1454 |
("(! A. axiom(or(not(or(A,A)),A))) & \
|
|
1455 |
\ (! B A. axiom(or(not(A),or(B,A)))) & \
|
|
1456 |
\ (! B A. axiom(or(not(or(A,B)),or(B,A)))) & \
|
|
1457 |
\ (! B A C. axiom(or(not(or(A,or(B,C))),or(B,or(A,C))))) & \
|
|
1458 |
\ (! A C B. axiom(or(not(or(not(A),B)),or(not(or(C,A)),or(C,B))))) & \
|
|
1459 |
\ (! X. axiom(X) --> theorem(X)) & \
|
|
1460 |
\ (! X Y. axiom(or(not(Y),X)) & theorem(Y) --> theorem(X)) & \
|
|
1461 |
\ (! X Y Z. axiom(or(not(X),Y)) & theorem(or(not(Y),Z)) --> theorem(or(not(X),Z))) & \
|
|
1462 |
\ (~theorem(or(not(not(or(p,q))),not(q)))) --> False",
|
|
1463 |
meson_tac);
|
|
1464 |
|
|
1465 |
(*5849 inferences so far. Searching to depth 12. 5.6 secs*)
|
|
1466 |
val LCL215_1 = prove_hard
|
|
1467 |
("(! A. axiom(or(not(or(A,A)),A))) & \
|
|
1468 |
\ (! B A. axiom(or(not(A),or(B,A)))) & \
|
|
1469 |
\ (! B A. axiom(or(not(or(A,B)),or(B,A)))) & \
|
|
1470 |
\ (! B A C. axiom(or(not(or(A,or(B,C))),or(B,or(A,C))))) & \
|
|
1471 |
\ (! A C B. axiom(or(not(or(not(A),B)),or(not(or(C,A)),or(C,B))))) & \
|
|
1472 |
\ (! X. axiom(X) --> theorem(X)) & \
|
|
1473 |
\ (! X Y. axiom(or(not(Y),X)) & theorem(Y) --> theorem(X)) & \
|
|
1474 |
\ (! X Y Z. axiom(or(not(X),Y)) & theorem(or(not(Y),Z)) --> theorem(or(not(X),Z))) & \
|
|
1475 |
\ (~theorem(or(not(or(not(p),q)),or(not(or(p,q)),q)))) --> False",
|
|
1476 |
meson_tac);
|
|
1477 |
|
|
1478 |
(*0 secs. Not sure that a search even starts!*)
|
|
1479 |
val LCL230_2 = prove
|
|
1480 |
("(q --> p | r) & \
|
|
1481 |
\ (~p) & \
|
|
1482 |
\ (q) & \
|
|
1483 |
\ (~r) --> False",
|
|
1484 |
meson_tac);
|
|
1485 |
|
|
1486 |
(*119585 inferences so far. Searching to depth 14. 262.4 secs*)
|
|
1487 |
val LDA003_1 = prove_hard
|
|
1488 |
("(! X. equal(X::'a,X)) & \
|
|
1489 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
1490 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
1491 |
\ (! Y X Z. equal(f(X::'a,f(Y::'a,Z)),f(f(X::'a,Y),f(X::'a,Z)))) & \
|
|
1492 |
\ (! X Y. left(X::'a,f(X::'a,Y))) & \
|
|
1493 |
\ (! Y X Z. left(X::'a,Y) & left(Y::'a,Z) --> left(X::'a,Z)) & \
|
|
1494 |
\ (equal(num2::'a,f(num1::'a,num1))) & \
|
|
1495 |
\ (equal(num3::'a,f(num2::'a,num1))) & \
|
|
1496 |
\ (equal(u::'a,f(num2::'a,num2))) & \
|
|
1497 |
\ (! A B C. equal(A::'a,B) --> equal(f(A::'a,C),f(B::'a,C))) & \
|
|
1498 |
\ (! D F' E. equal(D::'a,E) --> equal(f(F'::'a,D),f(F'::'a,E))) & \
|
|
1499 |
\ (! G H I'. equal(G::'a,H) & left(G::'a,I') --> left(H::'a,I')) & \
|
|
1500 |
\ (! J L K'. equal(J::'a,K') & left(L::'a,J) --> left(L::'a,K')) & \
|
|
1501 |
\ (~left(num3::'a,u)) --> False",
|
|
1502 |
meson_tac);
|
|
1503 |
|
|
1504 |
|
|
1505 |
(*2392 inferences so far. Searching to depth 12. 2.2 secs*)
|
|
1506 |
val MSC002_1 = prove
|
|
1507 |
("(at(something::'a,here,now)) & \
|
|
1508 |
\ (! Place Situation. hand_at(Place::'a,Situation) --> hand_at(Place::'a,let_go(Situation))) & \
|
|
1509 |
\ (! Place Another_place Situation. hand_at(Place::'a,Situation) --> hand_at(Another_place::'a,go(Another_place::'a,Situation))) & \
|
|
1510 |
\ (! Thing Situation. ~held(Thing::'a,let_go(Situation))) & \
|
|
1511 |
\ (! Situation Thing. at(Thing::'a,here,Situation) --> red(Thing)) & \
|
|
1512 |
\ (! Thing Place Situation. at(Thing::'a,Place,Situation) --> at(Thing::'a,Place,let_go(Situation))) & \
|
|
1513 |
\ (! Thing Place Situation. at(Thing::'a,Place,Situation) --> at(Thing::'a,Place,pick_up(Situation))) & \
|
|
1514 |
\ (! Thing Place Situation. at(Thing::'a,Place,Situation) --> grabbed(Thing::'a,pick_up(go(Place::'a,let_go(Situation))))) & \
|
|
1515 |
\ (! Thing Situation. red(Thing) & put(Thing::'a,there,Situation) --> answer(Situation)) & \
|
|
1516 |
\ (! Place Thing Another_place Situation. at(Thing::'a,Place,Situation) & grabbed(Thing::'a,Situation) --> put(Thing::'a,Another_place,go(Another_place::'a,Situation))) & \
|
|
1517 |
\ (! Thing Place Another_place Situation. at(Thing::'a,Place,Situation) --> held(Thing::'a,Situation) | at(Thing::'a,Place,go(Another_place::'a,Situation))) & \
|
|
1518 |
\ (! One_place Thing Place Situation. hand_at(One_place::'a,Situation) & held(Thing::'a,Situation) --> at(Thing::'a,Place,go(Place::'a,Situation))) & \
|
|
1519 |
\ (! Place Thing Situation. hand_at(Place::'a,Situation) & at(Thing::'a,Place,Situation) --> held(Thing::'a,pick_up(Situation))) & \
|
|
1520 |
\ (! Situation. ~answer(Situation)) --> False",
|
|
1521 |
meson_tac);
|
|
1522 |
|
|
1523 |
(*73 inferences so far. Searching to depth 10. 0.2 secs*)
|
|
1524 |
val MSC003_1 = prove
|
|
1525 |
("(! Number_of_small_parts Small_part Big_part Number_of_mid_parts Mid_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) --> in'(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Mid_part) | has_parts(Big_part::'a,times(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) & \
|
|
1526 |
\ (! Big_part Mid_part Number_of_mid_parts Number_of_small_parts Small_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) & has_parts(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Number_of_small_parts,Small_part) --> has_parts(Big_part::'a,times(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) & \
|
|
1527 |
\ (in'(john::'a,boy)) & \
|
|
1528 |
\ (! X. in'(X::'a,boy) --> in'(X::'a,human)) & \
|
|
1529 |
\ (! X. in'(X::'a,hand) --> has_parts(X::'a,num5,fingers)) & \
|
|
1530 |
\ (! X. in'(X::'a,human) --> has_parts(X::'a,num2,arm)) & \
|
|
1531 |
\ (! X. in'(X::'a,arm) --> has_parts(X::'a,num1,hand)) & \
|
|
1532 |
\ (~has_parts(john::'a,times(num2::'a,num1),hand)) --> False",
|
|
1533 |
meson_tac);
|
|
1534 |
|
|
1535 |
(*1486 inferences so far. Searching to depth 20. 1.2 secs*)
|
|
1536 |
val MSC004_1 = prove
|
|
1537 |
("(! Number_of_small_parts Small_part Big_part Number_of_mid_parts Mid_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) --> in'(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Mid_part) | has_parts(Big_part::'a,times(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) & \
|
|
1538 |
\ (! Big_part Mid_part Number_of_mid_parts Number_of_small_parts Small_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) & has_parts(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Number_of_small_parts,Small_part) --> has_parts(Big_part::'a,times(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) & \
|
|
1539 |
\ (in'(john::'a,boy)) & \
|
|
1540 |
\ (! X. in'(X::'a,boy) --> in'(X::'a,human)) & \
|
|
1541 |
\ (! X. in'(X::'a,hand) --> has_parts(X::'a,num5,fingers)) & \
|
|
1542 |
\ (! X. in'(X::'a,human) --> has_parts(X::'a,num2,arm)) & \
|
|
1543 |
\ (! X. in'(X::'a,arm) --> has_parts(X::'a,num1,hand)) & \
|
|
1544 |
\ (~has_parts(john::'a,times(times(num2::'a,num1),num5),fingers)) --> False",
|
|
1545 |
meson_tac);
|
|
1546 |
|
|
1547 |
(*100 inferences so far. Searching to depth 12. 0.1 secs*)
|
|
1548 |
val MSC005_1 = prove
|
|
1549 |
("(value(truth::'a,truth)) & \
|
|
1550 |
\ (value(falsity::'a,falsity)) & \
|
|
1551 |
\ (! X Y. value(X::'a,truth) & value(Y::'a,truth) --> value(xor(X::'a,Y),falsity)) & \
|
|
1552 |
\ (! X Y. value(X::'a,truth) & value(Y::'a,falsity) --> value(xor(X::'a,Y),truth)) & \
|
|
1553 |
\ (! X Y. value(X::'a,falsity) & value(Y::'a,truth) --> value(xor(X::'a,Y),truth)) & \
|
|
1554 |
\ (! X Y. value(X::'a,falsity) & value(Y::'a,falsity) --> value(xor(X::'a,Y),falsity)) & \
|
|
1555 |
\ (! Value. ~value(xor(xor(xor(xor(truth::'a,falsity),falsity),truth),falsity),Value)) --> False",
|
|
1556 |
meson_tac);
|
|
1557 |
|
|
1558 |
(*19116 inferences so far. Searching to depth 16. 15.9 secs*)
|
|
1559 |
val MSC006_1 = prove_hard
|
|
1560 |
("(! Y X Z. p(X::'a,Y) & p(Y::'a,Z) --> p(X::'a,Z)) & \
|
|
1561 |
\ (! Y X Z. q(X::'a,Y) & q(Y::'a,Z) --> q(X::'a,Z)) & \
|
|
1562 |
\ (! Y X. q(X::'a,Y) --> q(Y::'a,X)) & \
|
|
1563 |
\ (! X Y. p(X::'a,Y) | q(X::'a,Y)) & \
|
|
1564 |
\ (~p(a::'a,b)) & \
|
|
1565 |
\ (~q(c::'a,d)) --> False",
|
|
1566 |
meson_tac);
|
|
1567 |
|
|
1568 |
(*1713 inferences so far. Searching to depth 10. 2.8 secs*)
|
|
1569 |
val NUM001_1 = prove
|
|
1570 |
("(! A. equal(A::'a,A)) & \
|
|
1571 |
\ (! B A C. equal(A::'a,B) & equal(B::'a,C) --> equal(A::'a,C)) & \
|
|
1572 |
\ (! B A. equal(add(A::'a,B),add(B::'a,A))) & \
|
|
1573 |
\ (! A B C. equal(add(A::'a,add(B::'a,C)),add(add(A::'a,B),C))) & \
|
|
1574 |
\ (! B A. equal(subtract(add(A::'a,B),B),A)) & \
|
|
1575 |
\ (! A B. equal(A::'a,subtract(add(A::'a,B),B))) & \
|
|
1576 |
\ (! A C B. equal(add(subtract(A::'a,B),C),subtract(add(A::'a,C),B))) & \
|
|
1577 |
\ (! A C B. equal(subtract(add(A::'a,B),C),add(subtract(A::'a,C),B))) & \
|
|
1578 |
\ (! A C B D. equal(A::'a,B) & equal(C::'a,add(A::'a,D)) --> equal(C::'a,add(B::'a,D))) & \
|
|
1579 |
\ (! A C D B. equal(A::'a,B) & equal(C::'a,add(D::'a,A)) --> equal(C::'a,add(D::'a,B))) & \
|
|
1580 |
\ (! A C B D. equal(A::'a,B) & equal(C::'a,subtract(A::'a,D)) --> equal(C::'a,subtract(B::'a,D))) & \
|
|
1581 |
\ (! A C D B. equal(A::'a,B) & equal(C::'a,subtract(D::'a,A)) --> equal(C::'a,subtract(D::'a,B))) & \
|
|
1582 |
\ (~equal(add(add(a::'a,b),c),add(a::'a,add(b::'a,c)))) --> False",
|
|
1583 |
meson_tac);
|
|
1584 |
|
|
1585 |
(*20717 inferences so far. Searching to depth 11. 13.7 secs*)
|
|
1586 |
val NUM021_1 = prove_hard
|
|
1587 |
("(! X. equal(X::'a,X)) & \
|
|
1588 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
1589 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
1590 |
\ (! A. equal(add(A::'a,num0),A)) & \
|
|
1591 |
\ (! A B. equal(add(A::'a,successor(B)),successor(add(A::'a,B)))) & \
|
|
1592 |
\ (! A. equal(multiply(A::'a,num0),num0)) & \
|
|
1593 |
\ (! B A. equal(multiply(A::'a,successor(B)),add(multiply(A::'a,B),A))) & \
|
|
1594 |
\ (! A B. equal(successor(A),successor(B)) --> equal(A::'a,B)) & \
|
|
1595 |
\ (! A B. equal(A::'a,B) --> equal(successor(A),successor(B))) & \
|
|
1596 |
\ (! A C B. less(A::'a,B) & less(C::'a,A) --> less(C::'a,B)) & \
|
|
1597 |
\ (! A B C. equal(add(successor(A),B),C) --> less(B::'a,C)) & \
|
|
1598 |
\ (! A B. less(A::'a,B) --> equal(add(successor(predecessor_of_1st_minus_2nd(B::'a,A)),A),B)) & \
|
|
1599 |
\ (! A B. divides(A::'a,B) --> less(A::'a,B) | equal(A::'a,B)) & \
|
|
1600 |
\ (! A B. less(A::'a,B) --> divides(A::'a,B)) & \
|
|
1601 |
\ (! A B. equal(A::'a,B) --> divides(A::'a,B)) & \
|
|
1602 |
\ (less(b::'a,c)) & \
|
|
1603 |
\ (~less(b::'a,a)) & \
|
|
1604 |
\ (divides(c::'a,a)) & \
|
|
1605 |
\ (! A. ~equal(successor(A),num0)) --> False",
|
|
1606 |
meson_tac);
|
|
1607 |
|
|
1608 |
(*26320 inferences so far. Searching to depth 10. 26.4 secs*)
|
|
1609 |
val NUM024_1 = prove_hard
|
|
1610 |
("(! X. equal(X::'a,X)) & \
|
|
1611 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
1612 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
1613 |
\ (! A. equal(add(A::'a,num0),A)) & \
|
|
1614 |
\ (! A B. equal(add(A::'a,successor(B)),successor(add(A::'a,B)))) & \
|
|
1615 |
\ (! A. equal(multiply(A::'a,num0),num0)) & \
|
|
1616 |
\ (! B A. equal(multiply(A::'a,successor(B)),add(multiply(A::'a,B),A))) & \
|
|
1617 |
\ (! A B. equal(successor(A),successor(B)) --> equal(A::'a,B)) & \
|
|
1618 |
\ (! A B. equal(A::'a,B) --> equal(successor(A),successor(B))) & \
|
|
1619 |
\ (! A C B. less(A::'a,B) & less(C::'a,A) --> less(C::'a,B)) & \
|
|
1620 |
\ (! A B C. equal(add(successor(A),B),C) --> less(B::'a,C)) & \
|
|
1621 |
\ (! A B. less(A::'a,B) --> equal(add(successor(predecessor_of_1st_minus_2nd(B::'a,A)),A),B)) & \
|
|
1622 |
\ (! B A. equal(add(A::'a,B),add(B::'a,A))) & \
|
|
1623 |
\ (! B A C. equal(add(A::'a,B),add(C::'a,B)) --> equal(A::'a,C)) & \
|
|
1624 |
\ (less(a::'a,a)) & \
|
|
1625 |
\ (! A. ~equal(successor(A),num0)) --> False",
|
|
1626 |
meson_tac);
|
|
1627 |
|
|
1628 |
|
|
1629 |
(*1345 inferences so far. Searching to depth 7. 23.3 secs. BIG*)
|
|
1630 |
val NUM180_1 = prove_hard
|
|
1631 |
("(! X. equal(X::'a,X)) & \
|
|
1632 |
\ (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
|
|
1633 |
\ (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) & \
|
|
1634 |
\ (! X U Y. subclass(X::'a,Y) & member(U::'a,X) --> member(U::'a,Y)) & \
|
|
1635 |
\ (! X Y. member(not_subclass_element(X::'a,Y),X) | subclass(X::'a,Y)) & \
|
|
1636 |
\ (! X Y. member(not_subclass_element(X::'a,Y),Y) --> subclass(X::'a,Y)) & \
|
|
1637 |
\ (! X. subclass(X::'a,universal_class)) & \
|
|
1638 |
\ (! X Y. equal(X::'a,Y) --> subclass(X::'a,Y)) & \
|
|
1639 |
\ (! Y X. equal(X::'a,Y) --> subclass(Y::'a,X)) & \
|
|
1640 |
\ (! X Y. subclass(X::'a,Y) & subclass(Y::'a,X) --> equal(X::'a,Y)) & \
|
|
1641 |
\ (! X U Y. member(U::'a,unordered_pair(X::'a,Y)) --> equal(U::'a,X) | equal(U::'a,Y)) & \
|
|
1642 |
\ (! X Y. member(X::'a,universal_class) --> member(X::'a,unordered_pair(X::'a,Y))) & \
|
|
1643 |
\ (! X Y. member(Y::'a,universal_class) --> member(Y::'a,unordered_pair(X::'a,Y))) & \
|
|
1644 |
\ (! X Y. member(unordered_pair(X::'a,Y),universal_class)) & \
|
|
1645 |
\ (! X. equal(unordered_pair(X::'a,X),singleton(X))) & \
|
|
1646 |
\ (! X Y. equal(unordered_pair(singleton(X),unordered_pair(X::'a,singleton(Y))),ordered_pair(X::'a,Y))) & \
|
|
1647 |
\ (! V Y U X. member(ordered_pair(U::'a,V),cross_product(X::'a,Y)) --> member(U::'a,X)) & \
|
|
1648 |
\ (! U X V Y. member(ordered_pair(U::'a,V),cross_product(X::'a,Y)) --> member(V::'a,Y)) & \
|
|
1649 |
\ (! U V X Y. member(U::'a,X) & member(V::'a,Y) --> member(ordered_pair(U::'a,V),cross_product(X::'a,Y))) & \
|
|
1650 |
\ (! X Y Z. member(Z::'a,cross_product(X::'a,Y)) --> equal(ordered_pair(first(Z),second(Z)),Z)) & \
|
|
1651 |
\ (subclass(element_relation::'a,cross_product(universal_class::'a,universal_class))) & \
|
|
1652 |
\ (! X Y. member(ordered_pair(X::'a,Y),element_relation) --> member(X::'a,Y)) & \
|
|
1653 |
\ (! X Y. member(ordered_pair(X::'a,Y),cross_product(universal_class::'a,universal_class)) & member(X::'a,Y) --> member(ordered_pair(X::'a,Y),element_relation)) & \
|
|
1654 |
\ (! Y Z X. member(Z::'a,intersection(X::'a,Y)) --> member(Z::'a,X)) & \
|
|
1655 |
\ (! X Z Y. member(Z::'a,intersection(X::'a,Y)) --> member(Z::'a,Y)) & \
|
|
1656 |
\ (! Z X Y. member(Z::'a,X) & member(Z::'a,Y) --> member(Z::'a,intersection(X::'a,Y))) & \
|
|
1657 |
\ (! Z X. ~(member(Z::'a,complement(X)) & member(Z::'a,X))) & \
|
|
1658 |
\ (! Z X. member(Z::'a,universal_class) --> member(Z::'a,complement(X)) | member(Z::'a,X)) & \
|
|
1659 |
\ (! X Y. equal(complement(intersection(complement(X),complement(Y))),union(X::'a,Y))) & \
|
|
1660 |
\ (! X Y. equal(intersection(complement(intersection(X::'a,Y)),complement(intersection(complement(X),complement(Y)))),difference(X::'a,Y))) & \
|
|
1661 |
\ (! Xr X Y. equal(intersection(Xr::'a,cross_product(X::'a,Y)),restrct(Xr::'a,X,Y))) & \
|
|
1662 |
\ (! Xr X Y. equal(intersection(cross_product(X::'a,Y),Xr),restrct(Xr::'a,X,Y))) & \
|
|
1663 |
\ (! Z X. ~(equal(restrct(X::'a,singleton(Z),universal_class),null_class) & member(Z::'a,domain_of(X)))) & \
|
|
1664 |
\ (! Z X. member(Z::'a,universal_class) --> equal(restrct(X::'a,singleton(Z),universal_class),null_class) | member(Z::'a,domain_of(X))) & \
|
|
1665 |
\ (! X. subclass(rotate(X),cross_product(cross_product(universal_class::'a,universal_class),universal_class))) & \
|
|
1666 |
\ (! V W U X. member(ordered_pair(ordered_pair(U::'a,V),W),rotate(X)) --> member(ordered_pair(ordered_pair(V::'a,W),U),X)) & \
|
|
1667 |
\ (! U V W X. member(ordered_pair(ordered_pair(V::'a,W),U),X) & member(ordered_pair(ordered_pair(U::'a,V),W),cross_product(cross_product(universal_class::'a,universal_class),universal_class)) --> member(ordered_pair(ordered_pair(U::'a,V),W),rotate(X))) & \
|
|
1668 |
\ (! X. subclass(flip(X),cross_product(cross_product(universal_class::'a,universal_class),universal_class))) & \
|
|
1669 |
\ (! V U W X. member(ordered_pair(ordered_pair(U::'a,V),W),flip(X)) --> member(ordered_pair(ordered_pair(V::'a,U),W),X)) & \
|
|
1670 |
\ (! U V W X. member(ordered_pair(ordered_pair(V::'a,U),W),X) & member(ordered_pair(ordered_pair(U::'a,V),W),cross_product(cross_product(universal_class::'a,universal_class),universal_class)) --> member(ordered_pair(ordered_pair(U::'a,V),W),flip(X))) & \
|
|
1671 |
\ (! Y. equal(domain_of(flip(cross_product(Y::'a,universal_class))),inverse(Y))) & \
|
|
1672 |
\ (! Z. equal(domain_of(inverse(Z)),range_of(Z))) & \
|
|
1673 |
\ (! Z X Y. equal(first(not_subclass_element(restrct(Z::'a,X,singleton(Y)),null_class)),domain(Z::'a,X,Y))) & \
|
|
1674 |
\ (! Z X Y. equal(second(not_subclass_element(restrct(Z::'a,singleton(X),Y),null_class)),rng(Z::'a,X,Y))) & \
|
|
1675 |
\ (! Xr X. equal(range_of(restrct(Xr::'a,X,universal_class)),image_(Xr::'a,X))) & \
|
|
1676 |
\ (! X. equal(union(X::'a,singleton(X)),successor(X))) & \
|
|
1677 |
\ (subclass(successor_relation::'a,cross_product(universal_class::'a,universal_class))) & \
|
|
1678 |
\ (! X Y. member(ordered_pair(X::'a,Y),successor_relation) --> equal(successor(X),Y)) & \
|
|
1679 |
\ (! X Y. equal(successor(X),Y) & member(ordered_pair(X::'a,Y),cross_product(universal_class::'a,universal_class)) --> member(ordered_pair(X::'a,Y),successor_relation)) & \
|
|
1680 |
\ (! X. inductive(X) --> member(null_class::'a,X)) & \
|
|
1681 |
\ (! X. inductive(X) --> subclass(image_(successor_relation::'a,X),X)) & \
|
|
1682 |
\ (! X. member(null_class::'a,X) & subclass(image_(successor_relation::'a,X),X) --> inductive(X)) & \
|
|
1683 |
\ (inductive(omega)) & \
|
|
1684 |
\ (! Y. inductive(Y) --> subclass(omega::'a,Y)) & \
|
|
1685 |
\ (member(omega::'a,universal_class)) & \
|
|
1686 |
\ (! X. equal(domain_of(restrct(element_relation::'a,universal_class,X)),sum_class(X))) & \
|
|
1687 |
\ (! X. member(X::'a,universal_class) --> member(sum_class(X),universal_class)) & \
|
|
1688 |
\ (! X. equal(complement(image_(element_relation::'a,complement(X))),powerClass(X))) & \
|
|
1689 |
\ (! U. member(U::'a,universal_class) --> member(powerClass(U),universal_class)) & \
|
|
1690 |
\ (! Yr Xr. subclass(compos(Yr::'a,Xr),cross_product(universal_class::'a,universal_class))) & \
|
|
1691 |
\ (! Z Yr Xr Y. member(ordered_pair(Y::'a,Z),compos(Yr::'a,Xr)) --> member(Z::'a,image_(Yr::'a,image_(Xr::'a,singleton(Y))))) & \
|
|
1692 |
\ (! Y Z Yr Xr. member(Z::'a,image_(Yr::'a,image_(Xr::'a,singleton(Y)))) & member(ordered_pair(Y::'a,Z),cross_product(universal_class::'a,universal_class)) --> member(ordered_pair(Y::'a,Z),compos(Yr::'a,Xr))) & \
|
|
1693 |
\ (! X. single_valued_class(X) --> subclass(compos(X::'a,inverse(X)),identity_relation)) & \
|
|
1694 |
\ (! X. subclass(compos(X::'a,inverse(X)),identity_relation) --> single_valued_class(X)) & \
|
|
1695 |
\ (! Xf. function(Xf) --> subclass(Xf::'a,cross_product(universal_class::'a,universal_class))) & \
|
|
1696 |
\ (! Xf. function(Xf) --> subclass(compos(Xf::'a,inverse(Xf)),identity_relation)) & \
|
|
1697 |
\ (! Xf. subclass(Xf::'a,cross_product(universal_class::'a,universal_class)) & subclass(compos(Xf::'a,inverse(Xf)),identity_relation) --> function(Xf)) & \
|
|
1698 |
\ (! Xf X. function(Xf) & member(X::'a,universal_class) --> member(image_(Xf::'a,X),universal_class)) & \
|
|
1699 |
\ (! X. equal(X::'a,null_class) | member(regular(X),X)) & \
|
|
1700 |
\ (! X. equal(X::'a,null_class) | equal(intersection(X::'a,regular(X)),null_class)) & \
|
|
1701 |
\ (! Xf Y. equal(sum_class(image_(Xf::'a,singleton(Y))),apply(Xf::'a,Y))) & \
|
|
1702 |
\ (function(choice)) & \
|
|
1703 |
\ (! Y. member(Y::'a,universal_class) --> equal(Y::'a,null_class) | member(apply(choice::'a,Y),Y)) & \
|
|
1704 |
\ (! Xf. one_to_one(Xf) --> function(Xf)) & \
|
|
1705 |
\ (! Xf. one_to_one(Xf) --> function(inverse(Xf))) & \
|
|
1706 |
\ (! Xf. function(inverse(Xf)) & function(Xf) --> one_to_one(Xf)) & \
|
|
1707 |
\ (equal(intersection(cross_product(universal_class::'a,universal_class),intersection(cross_product(universal_class::'a,universal_class),complement(compos(complement(element_relation),inverse(element_relation))))),subset_relation)) & \
|
|
1708 |
\ (equal(intersection(inverse(subset_relation),subset_relation),identity_relation)) & \
|
|
1709 |
\ (! Xr. equal(complement(domain_of(intersection(Xr::'a,identity_relation))),diagonalise(Xr))) & \
|
|
1710 |
\ (! X. equal(intersection(domain_of(X),diagonalise(compos(inverse(element_relation),X))),cantor(X))) & \
|
|
1711 |
\ (! Xf. operation(Xf) --> function(Xf)) & \
|
|
1712 |
\ (! Xf. operation(Xf) --> equal(cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))),domain_of(Xf))) & \
|
|
1713 |
\ (! Xf. operation(Xf) --> subclass(range_of(Xf),domain_of(domain_of(Xf)))) & \
|
|
1714 |
\ (! Xf. function(Xf) & equal(cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))),domain_of(Xf)) & subclass(range_of(Xf),domain_of(domain_of(Xf))) --> operation(Xf)) & \
|
|
1715 |
\ (! Xf1 Xf2 Xh. compatible(Xh::'a,Xf1,Xf2) --> function(Xh)) & \
|
|
1716 |
\ (! Xf2 Xf1 Xh. compatible(Xh::'a,Xf1,Xf2) --> equal(domain_of(domain_of(Xf1)),domain_of(Xh))) & \
|
|
1717 |
\ (! Xf1 Xh Xf2. compatible(Xh::'a,Xf1,Xf2) --> subclass(range_of(Xh),domain_of(domain_of(Xf2)))) & \
|
|
1718 |
\ (! Xh Xh1 Xf1 Xf2. function(Xh) & equal(domain_of(domain_of(Xf1)),domain_of(Xh)) & subclass(range_of(Xh),domain_of(domain_of(Xf2))) --> compatible(Xh1::'a,Xf1,Xf2)) & \
|
|
1719 |
\ (! Xh Xf2 Xf1. homomorphism(Xh::'a,Xf1,Xf2) --> operation(Xf1)) & \
|
|
1720 |
\ (! Xh Xf1 Xf2. homomorphism(Xh::'a,Xf1,Xf2) --> operation(Xf2)) & \
|
|
1721 |
\ (! Xh Xf1 Xf2. homomorphism(Xh::'a,Xf1,Xf2) --> compatible(Xh::'a,Xf1,Xf2)) & \
|
|
1722 |
\ (! Xf2 Xh Xf1 X Y. homomorphism(Xh::'a,Xf1,Xf2) & member(ordered_pair(X::'a,Y),domain_of(Xf1)) --> equal(apply(Xf2::'a,ordered_pair(apply(Xh::'a,X),apply(Xh::'a,Y))),apply(Xh::'a,apply(Xf1::'a,ordered_pair(X::'a,Y))))) & \
|
|
1723 |
\ (! Xh Xf1 Xf2. operation(Xf1) & operation(Xf2) & compatible(Xh::'a,Xf1,Xf2) --> member(ordered_pair(not_homomorphism1(Xh::'a,Xf1,Xf2),not_homomorphism2(Xh::'a,Xf1,Xf2)),domain_of(Xf1)) | homomorphism(Xh::'a,Xf1,Xf2)) & \
|
|
1724 |
\ (! Xh Xf1 Xf2. operation(Xf1) & operation(Xf2) & compatible(Xh::'a,Xf1,Xf2) & equal(apply(Xf2::'a,ordered_pair(apply(Xh::'a,not_homomorphism1(Xh::'a,Xf1,Xf2)),apply(Xh::'a,not_homomorphism2(Xh::'a,Xf1,Xf2)))),apply(Xh::'a,apply(Xf1::'a,ordered_pair(not_homomorphism1(Xh::'a,Xf1,Xf2),not_homomorphism2(Xh::'a,Xf1,Xf2))))) --> homomorphism(Xh::'a,Xf1,Xf2)) & \
|
|
1725 |
\ (! D E F'. equal(D::'a,E) --> equal(apply(D::'a,F'),apply(E::'a,F'))) & \
|
|
1726 |
\ (! G I' H. equal(G::'a,H) --> equal(apply(I'::'a,G),apply(I'::'a,H))) & \
|
|
1727 |
\ (! J K'. equal(J::'a,K') --> equal(cantor(J),cantor(K'))) & \
|
|
1728 |
\ (! L M. equal(L::'a,M) --> equal(complement(L),complement(M))) & \
|
|
1729 |
\ (! N O_ P. equal(N::'a,O_) --> equal(compos(N::'a,P),compos(O_::'a,P))) & \
|
|
1730 |
\ (! Q S' R. equal(Q::'a,R) --> equal(compos(S'::'a,Q),compos(S'::'a,R))) & \
|
|
1731 |
\ (! T' U V. equal(T'::'a,U) --> equal(cross_product(T'::'a,V),cross_product(U::'a,V))) & \
|
|
1732 |
\ (! W Y X. equal(W::'a,X) --> equal(cross_product(Y::'a,W),cross_product(Y::'a,X))) & \
|
|
1733 |
\ (! Z A1. equal(Z::'a,A1) --> equal(diagonalise(Z),diagonalise(A1))) & \
|
|
1734 |
\ (! B1 C1 D1. equal(B1::'a,C1) --> equal(difference(B1::'a,D1),difference(C1::'a,D1))) & \
|
|
1735 |
\ (! E1 G1 F1. equal(E1::'a,F1) --> equal(difference(G1::'a,E1),difference(G1::'a,F1))) & \
|
|
1736 |
\ (! H1 I1 J1 K1. equal(H1::'a,I1) --> equal(domain(H1::'a,J1,K1),domain(I1::'a,J1,K1))) & \
|
|
1737 |
\ (! L1 N1 M1 O1. equal(L1::'a,M1) --> equal(domain(N1::'a,L1,O1),domain(N1::'a,M1,O1))) & \
|
|
1738 |
\ (! P1 R1 S1 Q1. equal(P1::'a,Q1) --> equal(domain(R1::'a,S1,P1),domain(R1::'a,S1,Q1))) & \
|
|
1739 |
\ (! T1 U1. equal(T1::'a,U1) --> equal(domain_of(T1),domain_of(U1))) & \
|
|
1740 |
\ (! V1 W1. equal(V1::'a,W1) --> equal(first(V1),first(W1))) & \
|
|
1741 |
\ (! X1 Y1. equal(X1::'a,Y1) --> equal(flip(X1),flip(Y1))) & \
|
|
1742 |
\ (! Z1 A2 B2. equal(Z1::'a,A2) --> equal(image_(Z1::'a,B2),image_(A2::'a,B2))) & \
|
|
1743 |
\ (! C2 E2 D2. equal(C2::'a,D2) --> equal(image_(E2::'a,C2),image_(E2::'a,D2))) & \
|
|
1744 |
\ (! F2 G2 H2. equal(F2::'a,G2) --> equal(intersection(F2::'a,H2),intersection(G2::'a,H2))) & \
|
|
1745 |
\ (! I2 K2 J2. equal(I2::'a,J2) --> equal(intersection(K2::'a,I2),intersection(K2::'a,J2))) & \
|
|
1746 |
\ (! L2 M2. equal(L2::'a,M2) --> equal(inverse(L2),inverse(M2))) & \
|
|
1747 |
\ (! N2 O2 P2 Q2. equal(N2::'a,O2) --> equal(not_homomorphism1(N2::'a,P2,Q2),not_homomorphism1(O2::'a,P2,Q2))) & \
|
|
1748 |
\ (! R2 T2 S2 U2. equal(R2::'a,S2) --> equal(not_homomorphism1(T2::'a,R2,U2),not_homomorphism1(T2::'a,S2,U2))) & \
|
|
1749 |
\ (! V2 X2 Y2 W2. equal(V2::'a,W2) --> equal(not_homomorphism1(X2::'a,Y2,V2),not_homomorphism1(X2::'a,Y2,W2))) & \
|
|
1750 |
\ (! Z2 A3 B3 C3. equal(Z2::'a,A3) --> equal(not_homomorphism2(Z2::'a,B3,C3),not_homomorphism2(A3::'a,B3,C3))) & \
|
|
1751 |
\ (! D3 F3 E3 G3. equal(D3::'a,E3) --> equal(not_homomorphism2(F3::'a,D3,G3),not_homomorphism2(F3::'a,E3,G3))) & \
|
|
1752 |
\ (! H3 J3 K3 I3. equal(H3::'a,I3) --> equal(not_homomorphism2(J3::'a,K3,H3),not_homomorphism2(J3::'a,K3,I3))) & \
|
|
1753 |
\ (! L3 M3 N3. equal(L3::'a,M3) --> equal(not_subclass_element(L3::'a,N3),not_subclass_element(M3::'a,N3))) & \
|
|
1754 |
\ (! O3 Q3 P3. equal(O3::'a,P3) --> equal(not_subclass_element(Q3::'a,O3),not_subclass_element(Q3::'a,P3))) & \
|
|
1755 |
\ (! R3 S3 T3. equal(R3::'a,S3) --> equal(ordered_pair(R3::'a,T3),ordered_pair(S3::'a,T3))) & \
|
|
1756 |
\ (! U3 W3 V3. equal(U3::'a,V3) --> equal(ordered_pair(W3::'a,U3),ordered_pair(W3::'a,V3))) & \
|
|
1757 |
\ (! X3 Y3. equal(X3::'a,Y3) --> equal(powerClass(X3),powerClass(Y3))) & \
|
|
1758 |
\ (! Z3 A4 B4 C4. equal(Z3::'a,A4) --> equal(rng(Z3::'a,B4,C4),rng(A4::'a,B4,C4))) & \
|
|
1759 |
\ (! D4 F4 E4 G4. equal(D4::'a,E4) --> equal(rng(F4::'a,D4,G4),rng(F4::'a,E4,G4))) & \
|
|
1760 |
\ (! H4 J4 K4 I4. equal(H4::'a,I4) --> equal(rng(J4::'a,K4,H4),rng(J4::'a,K4,I4))) & \
|
|
1761 |
\ (! L4 M4. equal(L4::'a,M4) --> equal(range_of(L4),range_of(M4))) & \
|
|
1762 |
\ (! N4 O4. equal(N4::'a,O4) --> equal(regular(N4),regular(O4))) & \
|
|
1763 |
\ (! P4 Q4 R4 S4. equal(P4::'a,Q4) --> equal(restrct(P4::'a,R4,S4),restrct(Q4::'a,R4,S4))) & \
|
|
1764 |
\ (! T4 V4 U4 W4. equal(T4::'a,U4) --> equal(restrct(V4::'a,T4,W4),restrct(V4::'a,U4,W4))) & \
|
|
1765 |
\ (! X4 Z4 A5 Y4. equal(X4::'a,Y4) --> equal(restrct(Z4::'a,A5,X4),restrct(Z4::'a,A5,Y4))) & \
|
|
1766 |
\ (! B5 C5. equal(B5::'a,C5) --> equal(rotate(B5),rotate(C5))) & \
|
|
1767 |
\ (! D5 E5. equal(D5::'a,E5) --> equal(second(D5),second(E5))) & \
|
|
1768 |
\ (! F5 G5. equal(F5::'a,G5) --> equal(singleton(F5),singleton(G5))) & \
|
|
1769 |
\ (! H5 I5. equal(H5::'a,I5) --> equal(successor(H5),successor(I5))) & \
|
|
1770 |
\ (! J5 K5. equal(J5::'a,K5) --> equal(sum_class(J5),sum_class(K5))) & \
|
|
1771 |
\ (! L5 M5 N5. equal(L5::'a,M5) --> equal(union(L5::'a,N5),union(M5::'a,N5))) & \
|
|
1772 |
\ (! O5 Q5 P5. equal(O5::'a,P5) --> equal(union(Q5::'a,O5),union(Q5::'a,P5))) & \
|
|
1773 |
\ (! R5 S5 T5. equal(R5::'a,S5) --> equal(unordered_pair(R5::'a,T5),unordered_pair(S5::'a,T5))) & \
|
|
1774 |
\ (! U5 W5 V5. equal(U5::'a,V5) --> equal(unordered_pair(W5::'a,U5),unordered_pair(W5::'a,V5))) & \
|
|
1775 |
\ (! X5 Y5 Z5 A6. equal(X5::'a,Y5) & compatible(X5::'a,Z5,A6) --> compatible(Y5::'a,Z5,A6)) & \
|
|
1776 |
\ (! B6 D6 C6 E6. equal(B6::'a,C6) & compatible(D6::'a,B6,E6) --> compatible(D6::'a,C6,E6)) & \
|
|
1777 |
\ (! F6 H6 I6 G6. equal(F6::'a,G6) & compatible(H6::'a,I6,F6) --> compatible(H6::'a,I6,G6)) & \
|
|
1778 |
\ (! J6 K6. equal(J6::'a,K6) & function(J6) --> function(K6)) & \
|
|
1779 |
\ (! L6 M6 N6 O6. equal(L6::'a,M6) & homomorphism(L6::'a,N6,O6) --> homomorphism(M6::'a,N6,O6)) & \
|
|
1780 |
\ (! P6 R6 Q6 S6. equal(P6::'a,Q6) & homomorphism(R6::'a,P6,S6) --> homomorphism(R6::'a,Q6,S6)) & \
|
|
1781 |
\ (! T6 V6 W6 U6. equal(T6::'a,U6) & homomorphism(V6::'a,W6,T6) --> homomorphism(V6::'a,W6,U6)) & \
|
|
1782 |
\ (! X6 Y6. equal(X6::'a,Y6) & inductive(X6) --> inductive(Y6)) & \
|
|
1783 |
\ (! Z6 A7 B7. equal(Z6::'a,A7) & member(Z6::'a,B7) --> member(A7::'a,B7)) & \
|
|
1784 |
\ (! C7 E7 D7. equal(C7::'a,D7) & member(E7::'a,C7) --> member(E7::'a,D7)) & \
|
|
1785 |
\ (! F7 G7. equal(F7::'a,G7) & one_to_one(F7) --> one_to_one(G7)) & \
|
|
1786 |
\ (! H7 I7. equal(H7::'a,I7) & operation(H7) --> operation(I7)) & \
|
|
1787 |
\ (! J7 K7. equal(J7::'a,K7) & single_valued_class(J7) --> single_valued_class(K7)) & \
|
|
1788 |
\ (! L7 M7 N7. equal(L7::'a,M7) & subclass(L7::'a,N7) --> subclass(M7::'a,N7)) & \
|
|
1789 |
\ (! O7 Q7 P7. equal(O7::'a,P7) & subclass(Q7::'a,O7) --> subclass(Q7::'a,P7)) & \
|
|
1790 |
\ (! X. subclass(compose_class(X),cross_product(universal_class::'a,universal_class))) & \
|
|
1791 |
\ (! X Y Z. member(ordered_pair(Y::'a,Z),compose_class(X)) --> equal(compos(X::'a,Y),Z)) & \
|
|
1792 |
\ (! Y Z X. member(ordered_pair(Y::'a,Z),cross_product(universal_class::'a,universal_class)) & equal(compos(X::'a,Y),Z) --> member(ordered_pair(Y::'a,Z),compose_class(X))) & \
|
|
1793 |
\ (subclass(composition_function::'a,cross_product(universal_class::'a,cross_product(universal_class::'a,universal_class)))) & \
|
|
1794 |
\ (! X Y Z. member(ordered_pair(X::'a,ordered_pair(Y::'a,Z)),composition_function) --> equal(compos(X::'a,Y),Z)) & \
|
|
1795 |
\ (! X Y. member(ordered_pair(X::'a,Y),cross_product(universal_class::'a,universal_class)) --> member(ordered_pair(X::'a,ordered_pair(Y::'a,compos(X::'a,Y))),composition_function)) & \
|
|
1796 |
\ (subclass(domain_relation::'a,cross_product(universal_class::'a,universal_class))) & \
|
|
1797 |
\ (! X Y. member(ordered_pair(X::'a,Y),domain_relation) --> equal(domain_of(X),Y)) & \
|
|
1798 |
\ (! X. member(X::'a,universal_class) --> member(ordered_pair(X::'a,domain_of(X)),domain_relation)) & \
|
|
1799 |
\ (! X. equal(first(not_subclass_element(compos(X::'a,inverse(X)),identity_relation)),single_valued1(X))) & \
|
|
1800 |
\ (! X. equal(second(not_subclass_element(compos(X::'a,inverse(X)),identity_relation)),single_valued2(X))) & \
|
|
1801 |
\ (! X. equal(domain(X::'a,image_(inverse(X),singleton(single_valued1(X))),single_valued2(X)),single_valued3(X))) & \
|
|
1802 |
\ (equal(intersection(complement(compos(element_relation::'a,complement(identity_relation))),element_relation),singleton_relation)) & \
|
|
1803 |
\ (subclass(application_function::'a,cross_product(universal_class::'a,cross_product(universal_class::'a,universal_class)))) & \
|
|
1804 |
\ (! Z Y X. member(ordered_pair(X::'a,ordered_pair(Y::'a,Z)),application_function) --> member(Y::'a,domain_of(X))) & \
|
|
1805 |
\ (! X Y Z. member(ordered_pair(X::'a,ordered_pair(Y::'a,Z)),application_function) --> equal(apply(X::'a,Y),Z)) & \
|
|
1806 |
\ (! Z X Y. member(ordered_pair(X::'a,ordered_pair(Y::'a,Z)),cross_product(universal_class::'a,cross_product(universal_class::'a,universal_class))) & member(Y::'a,domain_of(X)) --> member(ordered_pair(X::'a,ordered_pair(Y::'a,apply(X::'a,Y))),application_function)) & \
|
|
1807 |
\ (! X Y Xf. maps(Xf::'a,X,Y) --> function(Xf)) & \
|
|
1808 |
\ (! Y Xf X. maps(Xf::'a,X,Y) --> equal(domain_of(Xf),X)) & \
|
|
1809 |
\ (! X Xf Y. maps(Xf::'a,X,Y) --> subclass(range_of(Xf),Y)) & \
|
|
1810 |
\ (! Xf Y. function(Xf) & subclass(range_of(Xf),Y) --> maps(Xf::'a,domain_of(Xf),Y)) & \
|
|
1811 |
\ (! L M. equal(L::'a,M) --> equal(compose_class(L),compose_class(M))) & \
|
|
1812 |
\ (! N2 O2. equal(N2::'a,O2) --> equal(single_valued1(N2),single_valued1(O2))) & \
|
|
1813 |
\ (! P2 Q2. equal(P2::'a,Q2) --> equal(single_valued2(P2),single_valued2(Q2))) & \
|
|
1814 |
\ (! R2 S2. equal(R2::'a,S2) --> equal(single_valued3(R2),single_valued3(S2))) & \
|
|
1815 |
\ (! X2 Y2 Z2 A3. equal(X2::'a,Y2) & maps(X2::'a,Z2,A3) --> maps(Y2::'a,Z2,A3)) & \
|
|
1816 |
\ (! B3 D3 C3 E3. equal(B3::'a,C3) & maps(D3::'a,B3,E3) --> maps(D3::'a,C3,E3)) & \
|
|
1817 |
\ (! F3 H3 I3 G3. equal(F3::'a,G3) & maps(H3::'a,I3,F3) --> maps(H3::'a,I3,G3)) & \
|
|
1818 |
\ (! X. equal(union(X::'a,inverse(X)),symmetrization_of(X))) & \
|
|
1819 |
\ (! X Y. irreflexive(X::'a,Y) --> subclass(restrct(X::'a,Y,Y),complement(identity_relation))) & \
|
|
1820 |
\ (! X Y. subclass(restrct(X::'a,Y,Y),complement(identity_relation)) --> irreflexive(X::'a,Y)) & \
|
|
1821 |
\ (! Y X. connected(X::'a,Y) --> subclass(cross_product(Y::'a,Y),union(identity_relation::'a,symmetrization_of(X)))) & \
|
|
1822 |
\ (! X Y. subclass(cross_product(Y::'a,Y),union(identity_relation::'a,symmetrization_of(X))) --> connected(X::'a,Y)) & \
|
|
1823 |
\ (! Xr Y. transitive(Xr::'a,Y) --> subclass(compos(restrct(Xr::'a,Y,Y),restrct(Xr::'a,Y,Y)),restrct(Xr::'a,Y,Y))) & \
|
|
1824 |
\ (! Xr Y. subclass(compos(restrct(Xr::'a,Y,Y),restrct(Xr::'a,Y,Y)),restrct(Xr::'a,Y,Y)) --> transitive(Xr::'a,Y)) & \
|
|
1825 |
\ (! Xr Y. asymmetric(Xr::'a,Y) --> equal(restrct(intersection(Xr::'a,inverse(Xr)),Y,Y),null_class)) & \
|
|
1826 |
\ (! Xr Y. equal(restrct(intersection(Xr::'a,inverse(Xr)),Y,Y),null_class) --> asymmetric(Xr::'a,Y)) & \
|
|
1827 |
\ (! Xr Y Z. equal(segment(Xr::'a,Y,Z),domain_of(restrct(Xr::'a,Y,singleton(Z))))) & \
|
|
1828 |
\ (! X Y. well_ordering(X::'a,Y) --> connected(X::'a,Y)) & \
|
|
1829 |
\ (! Y Xr U. well_ordering(Xr::'a,Y) & subclass(U::'a,Y) --> equal(U::'a,null_class) | member(least(Xr::'a,U),U)) & \
|
|
1830 |
\ (! Y V Xr U. well_ordering(Xr::'a,Y) & subclass(U::'a,Y) & member(V::'a,U) --> member(least(Xr::'a,U),U)) & \
|
fe75fe482566
restored the MESON examples file HOL/ex/mesontest2.ML
paulson
parents:
|