Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 25 Aug 1993 11:14:59 +0100
Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA02227;
          Wed, 25 Aug 93 03:09:21 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from iraun1.ira.uka.de by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA02223; Wed, 25 Aug 93 03:09:18 -0700
Received: from ira.uka.de by iraun1.ira.uka.de with SMTP (PP) 
          id <22098-0@iraun1.ira.uka.de>; Wed, 25 Aug 1993 12:09:13 +0200
To: info-hol@dworshak.cs.uidaho.edu
Date: Wed, 25 Aug 93 12:11:31 MET DST
From: schneide@ira.uka.de
Message-Id: <"iraun1.ira.100:25.07.93.10.09.15"@ira.uka.de>


I presented a tactic which eliminated select operators
by quantifiers.

Tom has proven that the tactics which I have presented
are not always adequate, i.e. they may generate subgoals
which are not theorems though the original goal is one.

Now, I have another question: Given any formula Q
with a subterm @x:'a.P x, is there always an equivalent 
formula Q' without a select  operator ?

Klaus