# HG changeset patch
# User paulson
# Date 826549410 -3600
# Node ID 9d001e5f43d81a2cc7b196cca01e28504145edc7
# Parent  9ba0906aa60d4b0dff8876a092ac5ca52ad818ed
Added formulation of Halting Problem

diff -r 9ba0906aa60d -r 9d001e5f43d8 src/FOL/ex/cla.ML
--- a/src/FOL/ex/cla.ML	Mon Mar 11 11:49:05 1996 +0100
+++ b/src/FOL/ex/cla.ML	Mon Mar 11 14:03:30 1996 +0100
@@ -496,6 +496,27 @@
 by (fast_tac FOL_cs 1);
 result();
 
+(*Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.)
+	author U. Egly*)
+goal FOL.thy
+"((EX X. a(X) & (ALL Y. c(Y) --> (ALL Z. d(X, Y, Z)))) -->  \
+\  (EX W. c(W) & (ALL Y. c(Y) --> (ALL Z. d(W, Y, Z)))))     \
+\ &                                                          \
+\ (ALL W. c(W) & (ALL U. c(U) --> (ALL V. d(W, U, V))) -->       \
+\       (ALL Y Z.                                               \
+\           (c(Y) & h2(Y, Z) --> h3(W, Y, Z) & o(W, g)) &       \
+\           (c(Y) & ~h2(Y, Z) --> h3(W, Y, Z) & o(W, b))))  \
+\ &                    \
+\ (ALL W. c(W) &       \
+\   (ALL Y Z.          \
+\       (c(Y) & h2(Y, Z) --> h3(W, Y, Z) & o(W, g)) &       \
+\       (c(Y) & ~h2(Y, Z) --> h3(W, Y, Z) & o(W, b))) -->       \
+\   (EX V. c(V) &       \
+\         (ALL Y. ((c(Y) & h3(W, Y, Y)) & o(W, g) --> ~h2(V, Y)) &       \
+\                 ((c(Y) & h3(W, Y, Y)) & o(W, b) --> h2(V, Y) & o(V, b))))) \
+\  -->                  \
+\  ~ (EX X. a(X) & (ALL Y. c(Y) --> (ALL Z. d(X, Y, Z))))";
+
 
 writeln"Reached end of file.";