src/FOL/ex/int.ML
 author clasohm Thu Sep 16 12:20:38 1993 +0200 (1993-09-16) changeset 0 a5a9c433f639 child 232 c28d2fc5dd1c permissions -rw-r--r--
Initial revision
 clasohm@0 1 (* Title: FOL/ex/int clasohm@0 2 ID: \$Id\$ clasohm@0 3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory clasohm@0 4 Copyright 1991 University of Cambridge clasohm@0 5 clasohm@0 6 Intuitionistic First-Order Logic clasohm@0 7 clasohm@0 8 Single-step commands: clasohm@0 9 by (Int.step_tac 1); clasohm@0 10 by (biresolve_tac safe_brls 1); clasohm@0 11 by (biresolve_tac haz_brls 1); clasohm@0 12 by (assume_tac 1); clasohm@0 13 by (Int.safe_tac 1); clasohm@0 14 by (Int.mp_tac 1); clasohm@0 15 by (Int.fast_tac 1); clasohm@0 16 *) clasohm@0 17 clasohm@0 18 writeln"File FOL/ex/int."; clasohm@0 19 clasohm@0 20 (*Note: for PROPOSITIONAL formulae... clasohm@0 21 ~A is classically provable iff it is intuitionistically provable. clasohm@0 22 Therefore A is classically provable iff ~~A is intuitionistically provable. clasohm@0 23 clasohm@0 24 Let Q be the conjuction of the propositions A|~A, one for each atom A in clasohm@0 25 P. If P is provable classically, then clearly P&Q is provable clasohm@0 26 intuitionistically, so ~~(P&Q) is also provable intuitionistically. clasohm@0 27 The latter is intuitionistically equivalent to ~~P&~~Q, hence to ~~P, clasohm@0 28 since ~~Q is intuitionistically provable. Finally, if P is a negation then clasohm@0 29 ~~P is intuitionstically equivalent to P. [Andy Pitts] clasohm@0 30 *) clasohm@0 31 clasohm@0 32 goal IFOL.thy "~~(P&Q) <-> ~~P & ~~Q"; clasohm@0 33 by (Int.fast_tac 1); clasohm@0 34 result(); clasohm@0 35 clasohm@0 36 goal IFOL.thy "~~~P <-> ~P"; clasohm@0 37 by (Int.fast_tac 1); clasohm@0 38 result(); clasohm@0 39 clasohm@0 40 goal IFOL.thy "~~((P --> Q | R) --> (P-->Q) | (P-->R))"; clasohm@0 41 by (Int.fast_tac 1); clasohm@0 42 result(); clasohm@0 43 clasohm@0 44 goal IFOL.thy "(P<->Q) <-> (Q<->P)"; clasohm@0 45 by (Int.fast_tac 1); clasohm@0 46 result(); clasohm@0 47 clasohm@0 48 clasohm@0 49 writeln"Lemmas for the propositional double-negation translation"; clasohm@0 50 clasohm@0 51 goal IFOL.thy "P --> ~~P"; clasohm@0 52 by (Int.fast_tac 1); clasohm@0 53 result(); clasohm@0 54 clasohm@0 55 goal IFOL.thy "~~(~~P --> P)"; clasohm@0 56 by (Int.fast_tac 1); clasohm@0 57 result(); clasohm@0 58 clasohm@0 59 goal IFOL.thy "~~P & ~~(P --> Q) --> ~~Q"; clasohm@0 60 by (Int.fast_tac 1); clasohm@0 61 result(); clasohm@0 62 clasohm@0 63 clasohm@0 64 writeln"The following are classically but not constructively valid."; clasohm@0 65 clasohm@0 66 (*The attempt to prove them terminates quickly!*) clasohm@0 67 goal IFOL.thy "((P-->Q) --> P) --> P"; clasohm@0 68 by (Int.fast_tac 1) handle ERROR => writeln"Failed, as expected"; clasohm@0 69 (*Check that subgoals remain: proof failed.*) clasohm@0 70 getgoal 1; clasohm@0 71 clasohm@0 72 goal IFOL.thy "(P&Q-->R) --> (P-->R) | (Q-->R)"; clasohm@0 73 by (Int.fast_tac 1) handle ERROR => writeln"Failed, as expected"; clasohm@0 74 getgoal 1; clasohm@0 75 clasohm@0 76 clasohm@0 77 writeln"Intuitionistic FOL: propositional problems based on Pelletier."; clasohm@0 78 clasohm@0 79 writeln"Problem ~~1"; clasohm@0 80 goal IFOL.thy "~~((P-->Q) <-> (~Q --> ~P))"; clasohm@0 81 by (Int.fast_tac 1); clasohm@0 82 result(); clasohm@0 83 (*5 secs*) clasohm@0 84 clasohm@0 85 clasohm@0 86 writeln"Problem ~~2"; clasohm@0 87 goal IFOL.thy "~~(~~P <-> P)"; clasohm@0 88 by (Int.fast_tac 1); clasohm@0 89 result(); clasohm@0 90 (*1 secs*) clasohm@0 91 clasohm@0 92 clasohm@0 93 writeln"Problem 3"; clasohm@0 94 goal IFOL.thy "~(P-->Q) --> (Q-->P)"; clasohm@0 95 by (Int.fast_tac 1); clasohm@0 96 result(); clasohm@0 97 clasohm@0 98 writeln"Problem ~~4"; clasohm@0 99 goal IFOL.thy "~~((~P-->Q) <-> (~Q --> P))"; clasohm@0 100 by (Int.fast_tac 1); clasohm@0 101 result(); clasohm@0 102 (*9 secs*) clasohm@0 103 clasohm@0 104 writeln"Problem ~~5"; clasohm@0 105 goal IFOL.thy "~~((P|Q-->P|R) --> P|(Q-->R))"; clasohm@0 106 by (Int.fast_tac 1); clasohm@0 107 result(); clasohm@0 108 (*10 secs*) clasohm@0 109 clasohm@0 110 clasohm@0 111 writeln"Problem ~~6"; clasohm@0 112 goal IFOL.thy "~~(P | ~P)"; clasohm@0 113 by (Int.fast_tac 1); clasohm@0 114 result(); clasohm@0 115 clasohm@0 116 writeln"Problem ~~7"; clasohm@0 117 goal IFOL.thy "~~(P | ~~~P)"; clasohm@0 118 by (Int.fast_tac 1); clasohm@0 119 result(); clasohm@0 120 clasohm@0 121 writeln"Problem ~~8. Peirce's law"; clasohm@0 122 goal IFOL.thy "~~(((P-->Q) --> P) --> P)"; clasohm@0 123 by (Int.fast_tac 1); clasohm@0 124 result(); clasohm@0 125 clasohm@0 126 writeln"Problem 9"; clasohm@0 127 goal IFOL.thy "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"; clasohm@0 128 by (Int.fast_tac 1); clasohm@0 129 result(); clasohm@0 130 (*9 secs*) clasohm@0 131 clasohm@0 132 clasohm@0 133 writeln"Problem 10"; clasohm@0 134 goal IFOL.thy "(Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)"; clasohm@0 135 by (Int.fast_tac 1); clasohm@0 136 result(); clasohm@0 137 clasohm@0 138 writeln"11. Proved in each direction (incorrectly, says Pelletier!!) "; clasohm@0 139 goal IFOL.thy "P<->P"; clasohm@0 140 by (Int.fast_tac 1); clasohm@0 141 clasohm@0 142 writeln"Problem ~~12. Dijkstra's law "; clasohm@0 143 goal IFOL.thy "~~(((P <-> Q) <-> R) <-> (P <-> (Q <-> R)))"; clasohm@0 144 by (Int.fast_tac 1); clasohm@0 145 result(); clasohm@0 146 clasohm@0 147 goal IFOL.thy "((P <-> Q) <-> R) --> ~~(P <-> (Q <-> R))"; clasohm@0 148 by (Int.fast_tac 1); clasohm@0 149 result(); clasohm@0 150 clasohm@0 151 writeln"Problem 13. Distributive law"; clasohm@0 152 goal IFOL.thy "P | (Q & R) <-> (P | Q) & (P | R)"; clasohm@0 153 by (Int.fast_tac 1); clasohm@0 154 result(); clasohm@0 155 clasohm@0 156 writeln"Problem ~~14"; clasohm@0 157 goal IFOL.thy "~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))"; clasohm@0 158 by (Int.fast_tac 1); clasohm@0 159 result(); clasohm@0 160 clasohm@0 161 writeln"Problem ~~15"; clasohm@0 162 goal IFOL.thy "~~((P --> Q) <-> (~P | Q))"; clasohm@0 163 by (Int.fast_tac 1); clasohm@0 164 result(); clasohm@0 165 clasohm@0 166 writeln"Problem ~~16"; clasohm@0 167 goal IFOL.thy "~~((P-->Q) | (Q-->P))"; clasohm@0 168 by (Int.fast_tac 1); clasohm@0 169 result(); clasohm@0 170 clasohm@0 171 writeln"Problem ~~17"; clasohm@0 172 goal IFOL.thy clasohm@0 173 "~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))"; clasohm@0 174 by (Int.fast_tac 1); clasohm@0 175 result(); clasohm@0 176 clasohm@0 177 (*Dijkstra's "Golden Rule"*) clasohm@0 178 goal IFOL.thy "(P&Q) <-> P <-> Q <-> (P|Q)"; clasohm@0 179 by (Int.fast_tac 1); clasohm@0 180 result(); clasohm@0 181 clasohm@0 182 clasohm@0 183 writeln"U****Examples with quantifiers****"; clasohm@0 184 clasohm@0 185 clasohm@0 186 writeln"The converse is classical in the following implications..."; clasohm@0 187 clasohm@0 188 goal IFOL.thy "(EX x.P(x)-->Q) --> (ALL x.P(x)) --> Q"; clasohm@0 189 by (Int.fast_tac 1); clasohm@0 190 result(); clasohm@0 191 clasohm@0 192 goal IFOL.thy "((ALL x.P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)"; clasohm@0 193 by (Int.fast_tac 1); clasohm@0 194 result(); clasohm@0 195 clasohm@0 196 goal IFOL.thy "((ALL x. ~P(x))-->Q) --> ~ (ALL x. ~ (P(x)|Q))"; clasohm@0 197 by (Int.fast_tac 1); clasohm@0 198 result(); clasohm@0 199 clasohm@0 200 goal IFOL.thy "(ALL x.P(x)) | Q --> (ALL x. P(x) | Q)"; clasohm@0 201 by (Int.fast_tac 1); clasohm@0 202 result(); clasohm@0 203 clasohm@0 204 goal IFOL.thy "(EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))"; clasohm@0 205 by (Int.fast_tac 1); clasohm@0 206 result(); clasohm@0 207 clasohm@0 208 clasohm@0 209 clasohm@0 210 clasohm@0 211 writeln"The following are not constructively valid!"; clasohm@0 212 (*The attempt to prove them terminates quickly!*) clasohm@0 213 clasohm@0 214 goal IFOL.thy "((ALL x.P(x))-->Q) --> (EX x.P(x)-->Q)"; clasohm@0 215 by (Int.fast_tac 1) handle ERROR => writeln"Failed, as expected"; clasohm@0 216 getgoal 1; clasohm@0 217 clasohm@0 218 goal IFOL.thy "(P --> (EX x.Q(x))) --> (EX x. P-->Q(x))"; clasohm@0 219 by (Int.fast_tac 1) handle ERROR => writeln"Failed, as expected"; clasohm@0 220 getgoal 1; clasohm@0 221 clasohm@0 222 goal IFOL.thy "(ALL x. P(x) | Q) --> ((ALL x.P(x)) | Q)"; clasohm@0 223 by (Int.fast_tac 1) handle ERROR => writeln"Failed, as expected"; clasohm@0 224 getgoal 1; clasohm@0 225 clasohm@0 226 goal IFOL.thy "(ALL x. ~~P(x)) --> ~~(ALL x. P(x))"; clasohm@0 227 by (Int.fast_tac 1) handle ERROR => writeln"Failed, as expected"; clasohm@0 228 getgoal 1; clasohm@0 229 clasohm@0 230 (*Classically but not intuitionistically valid. Proved by a bug in 1986!*) clasohm@0 231 goal IFOL.thy "EX x. Q(x) --> (ALL x. Q(x))"; clasohm@0 232 by (Int.fast_tac 1) handle ERROR => writeln"Failed, as expected"; clasohm@0 233 getgoal 1; clasohm@0 234 clasohm@0 235 clasohm@0 236 writeln"Hard examples with quantifiers"; clasohm@0 237 clasohm@0 238 (*The ones that have not been proved are not known to be valid! clasohm@0 239 Some will require quantifier duplication -- not currently available*) clasohm@0 240 clasohm@0 241 writeln"Problem ~~18"; clasohm@0 242 goal IFOL.thy "~~(EX y. ALL x. P(y)-->P(x))"; clasohm@0 243 (*NOT PROVED*) clasohm@0 244 clasohm@0 245 writeln"Problem ~~19"; clasohm@0 246 goal IFOL.thy "~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))"; clasohm@0 247 (*NOT PROVED*) clasohm@0 248 clasohm@0 249 writeln"Problem 20"; clasohm@0 250 goal IFOL.thy "(ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w))) \ clasohm@0 251 \ --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"; clasohm@0 252 by (Int.fast_tac 1); clasohm@0 253 result(); clasohm@0 254 clasohm@0 255 writeln"Problem 21"; clasohm@0 256 goal IFOL.thy "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))"; clasohm@0 257 (*NOT PROVED*) clasohm@0 258 clasohm@0 259 writeln"Problem 22"; clasohm@0 260 goal IFOL.thy "(ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))"; clasohm@0 261 by (Int.fast_tac 1); clasohm@0 262 result(); clasohm@0 263 clasohm@0 264 writeln"Problem ~~23"; clasohm@0 265 goal IFOL.thy "~~ ((ALL x. P | Q(x)) <-> (P | (ALL x. Q(x))))"; clasohm@0 266 by (Int.best_tac 1); clasohm@0 267 result(); clasohm@0 268 clasohm@0 269 writeln"Problem 24"; clasohm@0 270 goal IFOL.thy "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & \ clasohm@0 271 \ ~(EX x.P(x)) --> (EX x.Q(x)) & (ALL x. Q(x)|R(x) --> S(x)) \ clasohm@0 272 \ --> (EX x. P(x)&R(x))"; clasohm@0 273 by (Int.fast_tac 1); clasohm@0 274 result(); clasohm@0 275 clasohm@0 276 writeln"Problem 25"; clasohm@0 277 goal IFOL.thy "(EX x. P(x)) & \ clasohm@0 278 \ (ALL x. L(x) --> ~ (M(x) & R(x))) & \ clasohm@0 279 \ (ALL x. P(x) --> (M(x) & L(x))) & \ clasohm@0 280 \ ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x))) \ clasohm@0 281 \ --> (EX x. Q(x)&P(x))"; clasohm@0 282 by (Int.best_tac 1); clasohm@0 283 result(); clasohm@0 284 clasohm@0 285 writeln"Problem ~~26"; clasohm@0 286 goal IFOL.thy "(~~(EX x. p(x)) <-> ~~(EX x. q(x))) & \ clasohm@0 287 \ (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y))) \ clasohm@0 288 \ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))"; clasohm@0 289 (*NOT PROVED*) clasohm@0 290 clasohm@0 291 writeln"Problem 27"; clasohm@0 292 goal IFOL.thy "(EX x. P(x) & ~Q(x)) & \ clasohm@0 293 \ (ALL x. P(x) --> R(x)) & \ clasohm@0 294 \ (ALL x. M(x) & L(x) --> P(x)) & \ clasohm@0 295 \ ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x))) \ clasohm@0 296 \ --> (ALL x. M(x) --> ~L(x))"; clasohm@0 297 by (Int.fast_tac 1); (*44 secs*) clasohm@0 298 result(); clasohm@0 299 clasohm@0 300 writeln"Problem ~~28. AMENDED"; clasohm@0 301 goal IFOL.thy "(ALL x. P(x) --> (ALL x. Q(x))) & \ clasohm@0 302 \ (~~(ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) & \ clasohm@0 303 \ (~~(EX x.S(x)) --> (ALL x. L(x) --> M(x))) \ clasohm@0 304 \ --> (ALL x. P(x) & L(x) --> M(x))"; clasohm@0 305 by (Int.fast_tac 1); (*101 secs*) clasohm@0 306 result(); clasohm@0 307 clasohm@0 308 writeln"Problem 29. Essentially the same as Principia Mathematica *11.71"; clasohm@0 309 goal IFOL.thy "(EX x. P(x)) & (EX y. Q(y)) \ clasohm@0 310 \ --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <-> \ clasohm@0 311 \ (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"; clasohm@0 312 by (Int.fast_tac 1); clasohm@0 313 result(); clasohm@0 314 clasohm@0 315 writeln"Problem ~~30"; clasohm@0 316 goal IFOL.thy "(ALL x. (P(x) | Q(x)) --> ~ R(x)) & \ clasohm@0 317 \ (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) \ clasohm@0 318 \ --> (ALL x. ~~S(x))"; clasohm@0 319 by (Int.fast_tac 1); clasohm@0 320 result(); clasohm@0 321 clasohm@0 322 writeln"Problem 31"; clasohm@0 323 goal IFOL.thy "~(EX x.P(x) & (Q(x) | R(x))) & \ clasohm@0 324 \ (EX x. L(x) & P(x)) & \ clasohm@0 325 \ (ALL x. ~ R(x) --> M(x)) \ clasohm@0 326 \ --> (EX x. L(x) & M(x))"; clasohm@0 327 by (Int.fast_tac 1); clasohm@0 328 result(); clasohm@0 329 clasohm@0 330 writeln"Problem 32"; clasohm@0 331 goal IFOL.thy "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \ clasohm@0 332 \ (ALL x. S(x) & R(x) --> L(x)) & \ clasohm@0 333 \ (ALL x. M(x) --> R(x)) \ clasohm@0 334 \ --> (ALL x. P(x) & M(x) --> L(x))"; clasohm@0 335 by (Int.best_tac 1); clasohm@0 336 result(); clasohm@0 337 clasohm@0 338 writeln"Problem ~~33"; clasohm@0 339 goal IFOL.thy "(ALL x. ~~(P(a) & (P(x)-->P(b))-->P(c))) <-> \ clasohm@0 340 \ (ALL x. ~~((~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c))))"; clasohm@0 341 by (Int.best_tac 1); clasohm@0 342 result(); clasohm@0 343 clasohm@0 344 clasohm@0 345 writeln"Problem 36"; clasohm@0 346 goal IFOL.thy clasohm@0 347 "(ALL x. EX y. J(x,y)) & \ clasohm@0 348 \ (ALL x. EX y. G(x,y)) & \ clasohm@0 349 \ (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z))) \ clasohm@0 350 \ --> (ALL x. EX y. H(x,y))"; clasohm@0 351 by (Int.fast_tac 1); (*35 secs*) clasohm@0 352 result(); clasohm@0 353 clasohm@0 354 writeln"Problem 37"; clasohm@0 355 goal IFOL.thy clasohm@0 356 "(ALL z. EX w. ALL x. EX y. \ clasohm@0 357 \ ~~(P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u.Q(u,w)))) & \ clasohm@0 358 \ (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \ clasohm@0 359 \ (~~(EX x y. Q(x,y)) --> (ALL x. R(x,x))) \ clasohm@0 360 \ --> ~~(ALL x. EX y. R(x,y))"; clasohm@0 361 (*NOT PROVED*) clasohm@0 362 clasohm@0 363 writeln"Problem 39"; clasohm@0 364 goal IFOL.thy "~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"; clasohm@0 365 by (Int.fast_tac 1); clasohm@0 366 result(); clasohm@0 367 clasohm@0 368 writeln"Problem 40. AMENDED"; clasohm@0 369 goal IFOL.thy "(EX y. ALL x. F(x,y) <-> F(x,x)) --> \ clasohm@0 370 \ ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"; clasohm@0 371 by (Int.fast_tac 1); clasohm@0 372 result(); clasohm@0 373 clasohm@0 374 writeln"Problem 44"; clasohm@0 375 goal IFOL.thy "(ALL x. f(x) --> \ clasohm@0 376 \ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \ clasohm@0 377 \ (EX x. j(x) & (ALL y. g(y) --> h(x,y))) \ clasohm@0 378 \ --> (EX x. j(x) & ~f(x))"; clasohm@0 379 by (Int.fast_tac 1); clasohm@0 380 result(); clasohm@0 381 clasohm@0 382 writeln"Problem 48"; clasohm@0 383 goal IFOL.thy "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"; clasohm@0 384 by (Int.fast_tac 1); clasohm@0 385 result(); clasohm@0 386 clasohm@0 387 writeln"Problem 51"; clasohm@0 388 goal IFOL.thy clasohm@0 389 "(EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) --> \ clasohm@0 390 \ (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"; clasohm@0 391 by (Int.best_tac 1); (*60 seconds*) clasohm@0 392 result(); clasohm@0 393 clasohm@0 394 writeln"Problem 52"; clasohm@0 395 (*Almost the same as 51. *) clasohm@0 396 goal IFOL.thy clasohm@0 397 "(EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) --> \ clasohm@0 398 \ (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)"; clasohm@0 399 by (Int.best_tac 1); (*60 seconds*) clasohm@0 400 result(); clasohm@0 401 clasohm@0 402 writeln"Problem 56"; clasohm@0 403 goal IFOL.thy clasohm@0 404 "(ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"; clasohm@0 405 by (Int.fast_tac 1); clasohm@0 406 result(); clasohm@0 407 clasohm@0 408 writeln"Problem 57"; clasohm@0 409 goal IFOL.thy clasohm@0 410 "P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \ clasohm@0 411 \ (ALL x y z. P(x,y) & P(y,z) --> P(x,z)) --> P(f(a,b), f(a,c))"; clasohm@0 412 by (Int.fast_tac 1); clasohm@0 413 result(); clasohm@0 414 clasohm@0 415 writeln"Problem 60"; clasohm@0 416 goal IFOL.thy clasohm@0 417 "ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"; clasohm@0 418 by (Int.fast_tac 1); clasohm@0 419 result(); clasohm@0 420 clasohm@0 421 writeln"Reached end of file.";