Theory Classical

(*  Title:      FOL/ex/Classical.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge
*)

section ‹Classical Predicate Calculus Problems›

theory Classical
imports FOL
begin

lemma ‹(P ⟶ Q ∨ R) ⟶ (P ⟶ Q) ∨ (P ⟶ R)›
  by blast


subsubsection ‹If and only if›

lemma ‹(P ⟷ Q) ⟷ (Q ⟷ P)›
  by blast

lemma ‹¬ (P ⟷ ¬ P)›
  by blast


subsection ‹Pelletier's examples›

text ‹
  Sample problems from

    ▪ F. J. Pelletier,
    Seventy-Five Problems for Testing Automatic Theorem Provers,
    J. Automated Reasoning 2 (1986), 191-216.
    Errata, JAR 4 (1988), 236-236.

  The hardest problems -- judging by experience with several theorem
  provers, including matrix ones -- are 34 and 43.
›

text‹1›
lemma ‹(P ⟶ Q) ⟷ (¬ Q ⟶ ¬ P)›
  by blast

text‹2›
lemma ‹¬ ¬ P ⟷ P›
  by blast

text‹3›
lemma ‹¬ (P ⟶ Q) ⟶ (Q ⟶ P)›
  by blast

text‹4›
lemma ‹(¬ P ⟶ Q) ⟷ (¬ Q ⟶ P)›
  by blast

text‹5›
lemma ‹((P ∨ Q) ⟶ (P ∨ R)) ⟶ (P ∨ (Q ⟶ R))›
  by blast

text‹6›
lemma ‹P ∨ ¬ P›
  by blast

text‹7›
lemma ‹P ∨ ¬ ¬ ¬ P›
  by blast

text‹8. Peirce's law›
lemma ‹((P ⟶ Q) ⟶ P) ⟶ P›
  by blast

text‹9›
lemma ‹((P ∨ Q) ∧ (¬ P ∨ Q) ∧ (P ∨ ¬ Q)) ⟶ ¬ (¬ P ∨ ¬ Q)›
  by blast

text‹10›
lemma ‹(Q ⟶ R) ∧ (R ⟶ P ∧ Q) ∧ (P ⟶ Q ∨ R) ⟶ (P ⟷ Q)›
  by blast

text‹11. Proved in each direction (incorrectly, says Pelletier!!)›
lemma ‹P ⟷ P›
  by blast

text‹12. "Dijkstra's law"›
lemma ‹((P ⟷ Q) ⟷ R) ⟷ (P ⟷ (Q ⟷ R))›
  by blast

text‹13. Distributive law›
lemma ‹P ∨ (Q ∧ R) ⟷ (P ∨ Q) ∧ (P ∨ R)›
  by blast

text‹14›
lemma ‹(P ⟷ Q) ⟷ ((Q ∨ ¬ P) ∧ (¬ Q ∨ P))›
  by blast

text‹15›
lemma ‹(P ⟶ Q) ⟷ (¬ P ∨ Q)›
  by blast

text‹16›
lemma ‹(P ⟶ Q) ∨ (Q ⟶ P)›
  by blast

text‹17›
lemma ‹((P ∧ (Q ⟶ R)) ⟶ S) ⟷ ((¬ P ∨ Q ∨ S) ∧ (¬ P ∨ ¬ R ∨ S))›
  by blast


subsection ‹Classical Logic: examples with quantifiers›

lemma ‹(∀x. P(x) ∧ Q(x)) ⟷ (∀x. P(x)) ∧ (∀x. Q(x))›
  by blast

lemma ‹(∃x. P ⟶ Q(x)) ⟷ (P ⟶ (∃x. Q(x)))›
  by blast

lemma ‹(∃x. P(x) ⟶ Q) ⟷ (∀x. P(x)) ⟶ Q›
  by blast

lemma ‹(∀x. P(x)) ∨ Q ⟷ (∀x. P(x) ∨ Q)›
  by blast

text‹Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux,
  JAR 10 (265-281), 1993.  Proof is trivial!›
lemma ‹¬ ((∃x. ¬ P(x)) ∧ ((∃x. P(x)) ∨ (∃x. P(x) ∧ Q(x))) ∧ ¬ (∃x. P(x)))›
  by blast


subsection ‹Problems requiring quantifier duplication›

text‹Theorem B of Peter Andrews, Theorem Proving via General Matings,
  JACM 28 (1981).›
lemma ‹(∃x. ∀y. P(x) ⟷ P(y)) ⟶ ((∃x. P(x)) ⟷ (∀y. P(y)))›
  by blast

text‹Needs multiple instantiation of ALL.›
lemma ‹(∀x. P(x) ⟶ P(f(x))) ∧ P(d) ⟶ P(f(f(f(d))))›
  by blast

text‹Needs double instantiation of the quantifier›
lemma ‹∃x. P(x) ⟶ P(a) ∧ P(b)›
  by blast

lemma ‹∃z. P(z) ⟶ (∀x. P(x))›
  by blast

lemma ‹∃x. (∃y. P(y)) ⟶ P(x)›
  by blast

text‹V. Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23. NOT PROVED.›
lemma
  ‹∃x x'. ∀y. ∃z z'.
    (¬ P(y,y) ∨ P(x,x) ∨ ¬ S(z,x)) ∧
    (S(x,y) ∨ ¬ S(y,z) ∨ Q(z',z')) ∧
    (Q(x',y) ∨ ¬ Q(y,z') ∨ S(x',x'))›
  oops


subsection ‹Hard examples with quantifiers›

text‹18›
lemma ‹∃y. ∀x. P(y) ⟶ P(x)›
  by blast

text‹19›
lemma ‹∃x. ∀y z. (P(y) ⟶ Q(z)) ⟶ (P(x) ⟶ Q(x))›
  by blast

text‹20›
lemma ‹(∀x y. ∃z. ∀w. (P(x) ∧ Q(y) ⟶ R(z) ∧ S(w)))
  ⟶ (∃x y. P(x) ∧ Q(y)) ⟶ (∃z. R(z))›
  by blast

text‹21›
lemma ‹(∃x. P ⟶ Q(x)) ∧ (∃x. Q(x) ⟶ P) ⟶ (∃x. P ⟷ Q(x))›
  by blast

text‹22›
lemma ‹(∀x. P ⟷ Q(x)) ⟶ (P ⟷ (∀x. Q(x)))›
  by blast

text‹23›
lemma ‹(∀x. P ∨ Q(x)) ⟷ (P ∨ (∀x. Q(x)))›
  by blast

text‹24›
lemma
  ‹¬ (∃x. S(x) ∧ Q(x)) ∧ (∀x. P(x) ⟶ Q(x) ∨ R(x)) ∧
    (¬ (∃x. P(x)) ⟶ (∃x. Q(x))) ∧ (∀x. Q(x) ∨ R(x) ⟶ S(x))
    ⟶ (∃x. P(x) ∧ R(x))›
  by blast

text‹25›
lemma
  ‹(∃x. P(x)) ∧
    (∀x. L(x) ⟶ ¬ (M(x) ∧ R(x))) ∧
    (∀x. P(x) ⟶ (M(x) ∧ L(x))) ∧
    ((∀x. P(x) ⟶ Q(x)) ∨ (∃x. P(x) ∧ R(x)))
    ⟶ (∃x. Q(x) ∧ P(x))›
  by blast

text‹26›
lemma
  ‹((∃x. p(x)) ⟷ (∃x. q(x))) ∧
    (∀x. ∀y. p(x) ∧ q(y) ⟶ (r(x) ⟷ s(y)))
  ⟶ ((∀x. p(x) ⟶ r(x)) ⟷ (∀x. q(x) ⟶ s(x)))›
  by blast

text‹27›
lemma
  ‹(∃x. P(x) ∧ ¬ Q(x)) ∧
    (∀x. P(x) ⟶ R(x)) ∧
    (∀x. M(x) ∧ L(x) ⟶ P(x)) ∧
    ((∃x. R(x) ∧ ¬ Q(x)) ⟶ (∀x. L(x) ⟶ ¬ R(x)))
  ⟶ (∀x. M(x) ⟶ ¬ L(x))›
  by blast

text‹28. AMENDED›
lemma
  ‹(∀x. P(x) ⟶ (∀x. Q(x))) ∧
    ((∀x. Q(x) ∨ R(x)) ⟶ (∃x. Q(x) ∧ S(x))) ∧
    ((∃x. S(x)) ⟶ (∀x. L(x) ⟶ M(x)))
  ⟶ (∀x. P(x) ∧ L(x) ⟶ M(x))›
  by blast

text‹29. Essentially the same as Principia Mathematica *11.71›
lemma
  ‹(∃x. P(x)) ∧ (∃y. Q(y))
    ⟶ ((∀x. P(x) ⟶ R(x)) ∧ (∀y. Q(y) ⟶ S(y)) ⟷
      (∀x y. P(x) ∧ Q(y) ⟶ R(x) ∧ S(y)))›
  by blast

text‹30›
lemma
  ‹(∀x. P(x) ∨ Q(x) ⟶ ¬ R(x)) ∧
    (∀x. (Q(x) ⟶ ¬ S(x)) ⟶ P(x) ∧ R(x))
    ⟶ (∀x. S(x))›
  by blast

text‹31›
lemma
  ‹¬ (∃x. P(x) ∧ (Q(x) ∨ R(x))) ∧
    (∃x. L(x) ∧ P(x)) ∧
    (∀x. ¬ R(x) ⟶ M(x))
  ⟶ (∃x. L(x) ∧ M(x))›
  by blast

text‹32›
lemma
  ‹(∀x. P(x) ∧ (Q(x) ∨ R(x)) ⟶ S(x)) ∧
    (∀x. S(x) ∧ R(x) ⟶ L(x)) ∧
    (∀x. M(x) ⟶ R(x))
  ⟶ (∀x. P(x) ∧ M(x) ⟶ L(x))›
  by blast

text‹33›
lemma
  ‹(∀x. P(a) ∧ (P(x) ⟶ P(b)) ⟶ P(c)) ⟷
    (∀x. (¬ P(a) ∨ P(x) ∨ P(c)) ∧ (¬ P(a) ∨ ¬ P(b) ∨ P(c)))›
  by blast

text‹34. AMENDED (TWICE!!). Andrews's challenge.›
lemma
  ‹((∃x. ∀y. p(x) ⟷ p(y)) ⟷ ((∃x. q(x)) ⟷ (∀y. p(y)))) ⟷
    ((∃x. ∀y. q(x) ⟷ q(y)) ⟷ ((∃x. p(x)) ⟷ (∀y. q(y))))›
  by blast

text‹35›
lemma ‹∃x y. P(x,y) ⟶ (∀u v. P(u,v))›
  by blast

text‹36›
lemma
  ‹(∀x. ∃y. J(x,y)) ∧
    (∀x. ∃y. G(x,y)) ∧
    (∀x y. J(x,y) ∨ G(x,y) ⟶ (∀z. J(y,z) ∨ G(y,z) ⟶ H(x,z)))
  ⟶ (∀x. ∃y. H(x,y))›
  by blast

text‹37›
lemma
  ‹(∀z. ∃w. ∀x. ∃y.
    (P(x,z) ⟶ P(y,w)) ∧ P(y,z) ∧ (P(y,w) ⟶ (∃u. Q(u,w)))) ∧
    (∀x z. ¬ P(x,z) ⟶ (∃y. Q(y,z))) ∧
    ((∃x y. Q(x,y)) ⟶ (∀x. R(x,x)))
  ⟶ (∀x. ∃y. R(x,y))›
  by blast

text‹38›
lemma
  ‹(∀x. p(a) ∧ (p(x) ⟶ (∃y. p(y) ∧ r(x,y))) ⟶
    (∃z. ∃w. p(z) ∧ r(x,w) ∧ r(w,z)))  ⟷
    (∀x. (¬ p(a) ∨ p(x) ∨ (∃z. ∃w. p(z) ∧ r(x,w) ∧ r(w,z))) ∧
      (¬ p(a) ∨ ¬ (∃y. p(y) ∧ r(x,y)) ∨
      (∃z. ∃w. p(z) ∧ r(x,w) ∧ r(w,z))))›
  by blast

text‹39›
lemma ‹¬ (∃x. ∀y. F(y,x) ⟷ ¬ F(y,y))›
  by blast

text‹40. AMENDED›
lemma
  ‹(∃y. ∀x. F(x,y) ⟷ F(x,x)) ⟶
    ¬ (∀x. ∃y. ∀z. F(z,y) ⟷ ¬ F(z,x))›
  by blast

text‹41›
lemma
  ‹(∀z. ∃y. ∀x. f(x,y) ⟷ f(x,z) ∧ ¬ f(x,x))
    ⟶ ¬ (∃z. ∀x. f(x,z))›
  by blast

text‹42›
lemma ‹¬ (∃y. ∀x. p(x,y) ⟷ ¬ (∃z. p(x,z) ∧ p(z,x)))›
  by blast

text‹43›
lemma
  ‹(∀x. ∀y. q(x,y) ⟷ (∀z. p(z,x) ⟷ p(z,y)))
    ⟶ (∀x. ∀y. q(x,y) ⟷ q(y,x))›
  by blast

text ‹
  Other proofs: Can use ‹auto›, which cheats by using rewriting!
  ‹Deepen_tac› alone requires 253 secs.  Or
  ‹by (mini_tac 1 THEN Deepen_tac 5 1)›.
›

text‹44›
lemma
  ‹(∀x. f(x) ⟶ (∃y. g(y) ∧ h(x,y) ∧ (∃y. g(y) ∧ ¬ h(x,y)))) ∧
    (∃x. j(x) ∧ (∀y. g(y) ⟶ h(x,y)))
  ⟶ (∃x. j(x) ∧ ¬ f(x))›
  by blast

text‹45›
lemma
  ‹(∀x. f(x) ∧ (∀y. g(y) ∧ h(x,y) ⟶ j(x,y))
      ⟶ (∀y. g(y) ∧ h(x,y) ⟶ k(y))) ∧
      ¬ (∃y. l(y) ∧ k(y)) ∧
      (∃x. f(x) ∧ (∀y. h(x,y) ⟶ l(y)) ∧ (∀y. g(y) ∧ h(x,y) ⟶ j(x,y)))
      ⟶ (∃x. f(x) ∧ ¬ (∃y. g(y) ∧ h(x,y)))›
  by blast


text‹46›
lemma
  ‹(∀x. f(x) ∧ (∀y. f(y) ∧ h(y,x) ⟶ g(y)) ⟶ g(x)) ∧
      ((∃x. f(x) ∧ ¬ g(x)) ⟶
       (∃x. f(x) ∧ ¬ g(x) ∧ (∀y. f(y) ∧ ¬ g(y) ⟶ j(x,y)))) ∧
      (∀x y. f(x) ∧ f(y) ∧ h(x,y) ⟶ ¬ j(y,x))
      ⟶ (∀x. f(x) ⟶ g(x))›
  by blast


subsection ‹Problems (mainly) involving equality or functions›

text‹48›
lemma ‹(a = b ∨ c = d) ∧ (a = c ∨ b = d) ⟶ a = d ∨ b = c›
  by blast

text‹49. NOT PROVED AUTOMATICALLY. Hard because it involves substitution for
  Vars; the type constraint ensures that x,y,z have the same type as a,b,u.›
lemma
  ‹(∃x y::'a. ∀z. z = x ∨ z = y) ∧ P(a) ∧ P(b) ∧ a ≠ b ⟶ (∀u::'a. P(u))›
  apply safe
  apply (rule_tac x = ‹a› in allE, assumption)
  apply (rule_tac x = ‹b› in allE, assumption)
  apply fast  ― ‹blast's treatment of equality can't do it›
  done

text‹50. (What has this to do with equality?)›
lemma ‹(∀x. P(a,x) ∨ (∀y. P(x,y))) ⟶ (∃x. ∀y. P(x,y))›
  by blast

text‹51›
lemma
  ‹(∃z w. ∀x y. P(x,y) ⟷ (x = z ∧ y = w)) ⟶
    (∃z. ∀x. ∃w. (∀y. P(x,y) ⟷ y=w) ⟷ x = z)›
  by blast

text‹52›
text‹Almost the same as 51.›
lemma
  ‹(∃z w. ∀x y. P(x,y) ⟷ (x = z ∧ y = w)) ⟶
    (∃w. ∀y. ∃z. (∀x. P(x,y) ⟷ x = z) ⟷ y = w)›
  by blast

text‹55›
text‹Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
  fast DISCOVERS who killed Agatha.›
schematic_goal
  ‹lives(agatha) ∧ lives(butler) ∧ lives(charles) ∧
   (killed(agatha,agatha) ∨ killed(butler,agatha) ∨ killed(charles,agatha)) ∧
   (∀x y. killed(x,y) ⟶ hates(x,y) ∧ ¬ richer(x,y)) ∧
   (∀x. hates(agatha,x) ⟶ ¬ hates(charles,x)) ∧
   (hates(agatha,agatha) ∧ hates(agatha,charles)) ∧
   (∀x. lives(x) ∧ ¬ richer(x,agatha) ⟶ hates(butler,x)) ∧
   (∀x. hates(agatha,x) ⟶ hates(butler,x)) ∧
   (∀x. ¬ hates(x,agatha) ∨ ¬ hates(x,butler) ∨ ¬ hates(x,charles)) ⟶
    killed(?who,agatha)›
  by fast  ― ‹MUCH faster than blast›


text‹56›
lemma ‹(∀x. (∃y. P(y) ∧ x = f(y)) ⟶ P(x)) ⟷ (∀x. P(x) ⟶ P(f(x)))›
  by blast

text‹57›
lemma
  ‹P(f(a,b), f(b,c)) ∧ P(f(b,c), f(a,c)) ∧
    (∀x y z. P(x,y) ∧ P(y,z) ⟶ P(x,z)) ⟶ P(f(a,b), f(a,c))›
  by blast

text‹58  NOT PROVED AUTOMATICALLY›
lemma ‹(∀x y. f(x) = g(y)) ⟶ (∀x y. f(f(x)) = f(g(y)))›
  by (slow elim: subst_context)


text‹59›
lemma ‹(∀x. P(x) ⟷ ¬ P(f(x))) ⟶ (∃x. P(x) ∧ ¬ P(f(x)))›
  by blast

text‹60›
lemma ‹∀x. P(x,f(x)) ⟷ (∃y. (∀z. P(z,y) ⟶ P(z,f(x))) ∧ P(x,y))›
  by blast

text‹62 as corrected in JAR 18 (1997), page 135›
lemma
  ‹(∀x. p(a) ∧ (p(x) ⟶ p(f(x))) ⟶ p(f(f(x)))) ⟷
    (∀x. (¬ p(a) ∨ p(x) ∨ p(f(f(x)))) ∧
      (¬ p(a) ∨ ¬ p(f(x)) ∨ p(f(f(x)))))›
  by blast

text ‹From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
  fast indeed copes!›
lemma
  ‹(∀x. F(x) ∧ ¬ G(x) ⟶ (∃y. H(x,y) ∧ J(y))) ∧
    (∃x. K(x) ∧ F(x) ∧ (∀y. H(x,y) ⟶ K(y))) ∧
    (∀x. K(x) ⟶ ¬ G(x)) ⟶ (∃x. K(x) ∧ J(x))›
  by fast

text ‹From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.
  It does seem obvious!›
lemma
  ‹(∀x. F(x) ∧ ¬ G(x) ⟶ (∃y. H(x,y) ∧ J(y))) ∧
    (∃x. K(x) ∧ F(x) ∧ (∀y. H(x,y) ⟶ K(y))) ∧
    (∀x. K(x) ⟶ ¬ G(x)) ⟶ (∃x. K(x) ⟶ ¬ G(x))›
  by fast

text ‹Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.)
  author U. Egly.›
lemma
  ‹((∃x. A(x) ∧ (∀y. C(y) ⟶ (∀z. D(x,y,z)))) ⟶
     (∃w. C(w) ∧ (∀y. C(y) ⟶ (∀z. D(w,y,z)))))
    ∧
    (∀w. C(w) ∧ (∀u. C(u) ⟶ (∀v. D(w,u,v))) ⟶
          (∀y z.
              (C(y) ∧ P(y,z) ⟶ Q(w,y,z) ∧ OO(w,g)) ∧
              (C(y) ∧ ¬ P(y,z) ⟶ Q(w,y,z) ∧ OO(w,b))))
    ∧
    (∀w. C(w) ∧
      (∀y z.
          (C(y) ∧ P(y,z) ⟶ Q(w,y,z) ∧ OO(w,g)) ∧
          (C(y) ∧ ¬ P(y,z) ⟶ Q(w,y,z) ∧ OO(w,b))) ⟶
      (∃v. C(v) ∧
            (∀y. ((C(y) ∧ Q(w,y,y)) ∧ OO(w,g) ⟶ ¬ P(v,y)) ∧
                    ((C(y) ∧ Q(w,y,y)) ∧ OO(w,b) ⟶ P(v,y) ∧ OO(v,b)))))
     ⟶ ¬ (∃x. A(x) ∧ (∀y. C(y) ⟶ (∀z. D(x,y,z))))›
  by (blast 12)
    ― ‹Needed because the search for depths below 12 is very slow.›


text ‹
  Halting problem II: credited to M. Bruschi by Li Dafa in JAR 18(1),
  p. 105.
›
lemma
  ‹((∃x. A(x) ∧ (∀y. C(y) ⟶ (∀z. D(x,y,z)))) ⟶
     (∃w. C(w) ∧ (∀y. C(y) ⟶ (∀z. D(w,y,z)))))
    ∧
    (∀w. C(w) ∧ (∀u. C(u) ⟶ (∀v. D(w,u,v))) ⟶
          (∀y z.
              (C(y) ∧ P(y,z) ⟶ Q(w,y,z) ∧ OO(w,g)) ∧
              (C(y) ∧ ¬ P(y,z) ⟶ Q(w,y,z) ∧ OO(w,b))))
    ∧
    ((∃w. C(w) ∧ (∀y. (C(y) ∧ P(y,y) ⟶ Q(w,y,y) ∧ OO(w,g)) ∧
                           (C(y) ∧ ¬ P(y,y) ⟶ Q(w,y,y) ∧ OO(w,b))))
     ⟶
     (∃v. C(v) ∧ (∀y. (C(y) ∧ P(y,y) ⟶ P(v,y) ∧ OO(v,g)) ∧
                           (C(y) ∧ ¬ P(y,y) ⟶ P(v,y) ∧ OO(v,b)))))
    ⟶
    ((∃v. C(v) ∧ (∀y. (C(y) ∧ P(y,y) ⟶ P(v,y) ∧ OO(v,g)) ∧
                           (C(y) ∧ ¬ P(y,y) ⟶ P(v,y) ∧ OO(v,b))))
     ⟶
     (∃u. C(u) ∧ (∀y. (C(y) ∧ P(y,y) ⟶ ¬ P(u,y)) ∧
                           (C(y) ∧ ¬ P(y,y) ⟶ P(u,y) ∧ OO(u,b)))))
     ⟶ ¬ (∃x. A(x) ∧ (∀y. C(y) ⟶ (∀z. D(x,y,z))))›
  by blast

text ‹Challenge found on info-hol.›
lemma ‹∀x. ∃v w. ∀y z. P(x) ∧ Q(y) ⟶ (P(v) ∨ R(w)) ∧ (R(z) ⟶ Q(v))›
  by blast

text ‹
  Attributed to Lewis Carroll by S. G. Pulman. The first or last assumption
  can be deleted.›
lemma
  ‹(∀x. honest(x) ∧ industrious(x) ⟶ healthy(x)) ∧
    ¬ (∃x. grocer(x) ∧ healthy(x)) ∧
    (∀x. industrious(x) ∧ grocer(x) ⟶ honest(x)) ∧
    (∀x. cyclist(x) ⟶ industrious(x)) ∧
    (∀x. ¬ healthy(x) ∧ cyclist(x) ⟶ ¬ honest(x))
    ⟶ (∀x. grocer(x) ⟶ ¬ cyclist(x))›
  by blast


(*Runtimes for old versions of this file:
Thu Jul 23 1992: loaded in 467s using iffE [on SPARC2]
Mon Nov 14 1994: loaded in 144s [on SPARC10, with deepen_tac]
Wed Nov 16 1994: loaded in 138s [after addition of norm_term_skip]
Mon Nov 21 1994: loaded in 131s [DEPTH_FIRST suppressing repetitions]

Further runtimes on a Sun-4
Tue Mar  4 1997: loaded in 93s (version 94-7)
Tue Mar  4 1997: loaded in 89s
Thu Apr  3 1997: loaded in 44s--using mostly Blast_tac
Thu Apr  3 1997: loaded in 96s--addition of two Halting Probs
Thu Apr  3 1997: loaded in 98s--using lim-1 for all haz rules
Tue Dec  2 1997: loaded in 107s--added 46; new equalSubst
Fri Dec 12 1997: loaded in 91s--faster proof reconstruction
Thu Dec 18 1997: loaded in 94s--two new "obvious theorems" (??)
*)

end