Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 21 Dec 1993 11:32:11 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA03815;
          Tue, 21 Dec 1993 04:25:00 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA03811;
          Tue, 21 Dec 1993 04:24:53 -0700
Received: from iraun1.ira.uka.de by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA16220;
          Tue, 21 Dec 1993 03:22:53 -0800
Received: from ira.uka.de by iraun1.ira.uka.de id <25833-0@iraun1.ira.uka.de>;
          Tue, 21 Dec 1993 12:22:25 +0100
Received: from ira.uka.de by i80fs2.ira.uka.de id <01968-0@i80fs2.ira.uka.de>;
          Tue, 21 Dec 1993 12:23:18 +0100
To: wishnu@cs.ruu.nl, info-hol@cs.uidaho.edu
Subject: Re: Help with DEPTH_CONV
In-Reply-To: Mail from 'Wishnu Prasetya <wishnu@cs.ruu.nl>' dated: Tue, 21 Dec 1993 11:35:27 +0100 (MET)
Date: Tue, 21 Dec 1993 12:23:17 +0100
From: schneide <schneide@ira.uka.de>
Message-Id: <"i80fs2.ira.970:21.11.93.11.23.21"@ira.uka.de>

Wishnu Prasetya asks:

|> Can anyone kindly explain why is the following application of
|> DEPTH_CONV is wrong:
|> 
|>   #DEPTH_CONV CONTRAPOS_CONV "!x:*. P x ==> p" ;;


I think this is because CONTRAPOS_CONV can be infinitely applied.
If one tries 
	ONCE_DEPTH_CONV CONTRAPOS_CONV (--`!x:'a. P x ==> p`--);
everything is o.k.

Ciao, Klaus