# HG changeset patch
# User lcp
# Date 771868062 -7200
# Node ID 49cc52442678cbf31101df4b348118773a5526d2
# Parent  4ce2ce940fafb9c57a7e5cae6869ba7620153297
problem 38 is provable

diff -r 4ce2ce940faf -r 49cc52442678 src/FOL/ex/cla.ML
--- a/src/FOL/ex/cla.ML	Fri Jun 17 16:51:37 1994 +0200
+++ b/src/FOL/ex/cla.ML	Fri Jun 17 17:47:42 1994 +0200
@@ -184,9 +184,6 @@
 goal FOL.thy "(ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
 \   --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
 by (fast_tac FOL_cs 1); 
-goal FOL.thy "(ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
-\   --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
-by (fast_tac FOL_cs 1); 
 result();
 
 writeln"Problem 21";
@@ -317,13 +314,14 @@
 (*slow...Poly/ML: 9.7 secs*)
 result();
 
-writeln"Problem 38. NOT PROVED";
+writeln"Problem 38";
 goal FOL.thy
     "(ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) -->	\
 \            (EX z. EX w. p(z) & r(x,w) & r(w,z)))  <->		\
 \    (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) &	\
 \            (~p(a) | ~(EX y. p(y) & r(x,y)) |				\
 \             (EX z. EX w. p(z) & r(x,w) & r(w,z))))";
+by (fast_tac FOL_cs 1);
 
 writeln"Problem 39";
 goal FOL.thy "~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
@@ -342,14 +340,15 @@
 by (best_tac FOL_cs 1);
 result();
 
-writeln"Problem 42  NOT PROVED";
+writeln"Problem 42";
 goal FOL.thy "~ (EX y. ALL x. p(x,y) <-> ~ (EX z. p(x,z) & p(z,x)))";
+by (best_tac FOL_dup_cs 1);
+result();
 
 writeln"Problem 43  NOT PROVED AUTOMATICALLY";
 goal FOL.thy "(ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y)))	\
 \         --> (ALL x. (ALL y. q(x,y) <-> q(y,x)))";
 
-
 writeln"Problem 44";
 goal FOL.thy "(ALL x. f(x) -->						\
 \             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &   	\