Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0)
          id <07262-0@swan.cl.cam.ac.uk>; Mon, 10 Feb 1992 18:53:36 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA14769;
          Mon, 10 Feb 92 10:34:14 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from Sun.COM by ted.cs.uidaho.edu (16.6/1.34) id AA14760;
          Mon, 10 Feb 92 10:33:50 -0800
Received: from Eng.Sun.COM (zigzag-bb.Corp.Sun.COM) by Sun.COM (4.1/SMI-4.1)
          id AA17997; Mon, 10 Feb 92 10:36:04 PST
Received: from lara.Eng.Sun.COM by Eng.Sun.COM (4.1/SMI-4.1) id AA29222;
          Mon, 10 Feb 92 10:34:43 PST
Received: by lara.Eng.Sun.COM (4.1/SMI-4.1) id AA03493;
          Mon, 10 Feb 92 10:35:51 PST
Date: Mon, 10 Feb 92 10:35:51 PST
From: Paul.Loewenstein@COM.Sun.Eng (Paul Loewenstein)
Message-Id: <9202101835.AA03493@lara.Eng.Sun.COM>
To: chou@edu.ucla.cs, info-hol@edu.uidaho.cs.ted
In-Reply-To: chou@cs.ucla.edu's message of Sat, 08 Feb 92 22:50:04 PST <9202090650.AA17805@maui.cs.ucla.edu>
Subject: Restricted quantification


I have never felt that adding syntactic sugar for:

        !x. P[x] ==> F[x]

was worth the effort.  I have however made a crude unwinding/pruning
conversion to eliminate x when P[x] is of the form:

        x = t

where t does not contain a free occurrence of x.



        Paul.