Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <05015-0@swan.cl.cam.ac.uk>; Wed, 29 Jul 1992 10:31:31 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA02778;
          Wed, 29 Jul 92 02:21:46 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA02773;
          Wed, 29 Jul 92 02:21:39 -0700
Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk 
          with SMTP (PP-6.0) to cl id <04761-0@swan.cl.cam.ac.uk>;
          Wed, 29 Jul 1992 10:19:59 +0100
To: gavan@za.ac.uct.mth.UCT_elc (Gavan Tredoux)
Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl
Subject: Re: CHOOSE breaks
In-Reply-To: Your message of Tue, 28 Jul 92 23:36:26. <9207282136.AA03441@UCT_elc.mth.uct.ac.za>
Date: Wed, 29 Jul 92 10:19:52 +0100
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.770:29.06.92.09.20.05"@cl.cam.ac.uk>

Hi Gavan,

It looks to me like you've found a bug, probably in CHOOSE_THEN.
I've managed to reproduce the problem with the following
theory-free simulation of your goal:

"(P0[(e:*)] \/ (?e1:*. ?e2:*. P1 [e1;e2;(e:*)])) /\
 P9[(e:*)] \/
 (?e1 e2. (P2 [e1] \/
    (?e1' e2. (P3 [e1';e2])) /\
    P3 [e1;e2;(e:*)])) ==>
    P4[(e:*)] \/
 (?e1:*. ?e2:*. P5[e1;e2] /\
   (P6[e2] \/
    (?e1 e2'. P7[e1;e2';e2])) /\
   P8[e2;e1])"

I'll look into it when I get a chance.

Tom