457 (\<exists>v. C(v) & |
457 (\<exists>v. C(v) & |
458 (\<forall>y. ((C(y) & Q(w,y,y)) & OO(w,g) --> ~P(v,y)) & |
458 (\<forall>y. ((C(y) & Q(w,y,y)) & OO(w,g) --> ~P(v,y)) & |
459 ((C(y) & Q(w,y,y)) & OO(w,b) --> P(v,y) & OO(v,b))))) |
459 ((C(y) & Q(w,y,y)) & OO(w,b) --> P(v,y) & OO(v,b))))) |
460 --> |
460 --> |
461 ~ (\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z))))" |
461 ~ (\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z))))" |
462 by (tactic{*Blast.depth_tac (claset ()) 12 1*}) |
462 by (tactic{*Blast.depth_tac @{claset} 12 1*}) |
463 --{*Needed because the search for depths below 12 is very slow*} |
463 --{*Needed because the search for depths below 12 is very slow*} |
464 |
464 |
465 |
465 |
466 text{*Halting problem II: credited to M. Bruschi by Li Dafa in JAR 18(1), p.105*} |
466 text{*Halting problem II: credited to M. Bruschi by Li Dafa in JAR 18(1), p.105*} |
467 lemma "((\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z)))) --> |
467 lemma "((\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z)))) --> |