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 10:47:45 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA03685;
          Tue, 21 Dec 1993 03:37:42 -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 AA03681;
          Tue, 21 Dec 1993 03:37:32 -0700
Received: from infix.cs.ruu.nl by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA16147;
          Tue, 21 Dec 1993 02:35:32 -0800
Received: by relay.cs.ruu.nl id AA08606 (5.67a/IDA-1.5 
          for info-hol@ted.cs.uidaho.edu); Tue, 21 Dec 1993 11:35:28 +0100
From: Wishnu Prasetya <wishnu@cs.ruu.nl>
Message-Id: <199312211035.AA08606@relay.cs.ruu.nl>
Subject: Help with DEPTH_CONV
To: info-hol@cs.uidaho.edu (hol mailing list)
Date: Tue, 21 Dec 1993 11:35:27 +0100 (MET)
X-Mailer: ELM [version 2.4 PL23]
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Length: 451

Hi there,

Can anyone kindly explain why is the following application of
DEPTH_CONV is wrong:

   #DEPTH_CONV CONTRAPOS_CONV "!x:*. P x ==> p" ;;

   Error: Frame stack overflow.
   Fast links are on: do (use-fast-links nil) for debugging
   Error signalled by %AP.
   Backtrace:  > funcall > lambda > %AP
   evaluation failed     lisp error

the number of subterms is surely small enough, and only one of them
in implication form.

Thanks.

-Wishnu-