Return-Path: Return-Path: Received: from nsf.ac.uk by swan.cl.cam.ac.uk via JANET with NIFTP to fgate (PP) id <1759-0@swan.cl.cam.ac.uk>; Fri, 21 Jun 1991 21:49:59 +0100 Received: from vax.nsfnet-relay.ac.uk by sun2.nsfnet-relay.ac.uk with SMTP inbound id <20308-110@sun2.nsfnet-relay.ac.uk>; Fri, 21 Jun 1991 20:57:02 +0100 Received: from [129.101.100.20] by vax.NSFnet-Relay.AC.UK via NSFnet with SMTP id aa16265; 21 Jun 91 19:31 BST Received: from relay1.UU.NET by ted.cs.uidaho.edu (15.11/1.34) id AA07243; Fri, 21 Jun 91 10:21:00 pdt Received: from uunet.uu.net (via LOCALHOST.UU.NET) by relay1.UU.NET with SMTP (5.61/UUNET-internet-primary) id AA24414; Fri, 21 Jun 91 13:23:24 -0400 Received: from melasv.UUCP by uunet.uu.net with UUCP/RMAIL (queueing-rmail) id 132211.13342; Fri, 21 Jun 1991 13:22:11 EDT Received: from rdc03. by melasv.uunet.uu.net (3.2/SMI-RD-3.2) id AA20948; Fri, 21 Jun 91 09:54:01 PDT Received: by rdc03. (4.0/SMI-RD-4.0) id AA01582; Fri, 21 Jun 91 09:53:59 PDT Date: Fri, 21 Jun 91 09:53:59 PDT From: melasv!paul@net.UU.uunet ( Paul Loewenstein CAD) Message-Id: <9106211653.AA01582@rdc03.> To: sandy Cc: info-hol@edu.uidaho.cs.ted In-Reply-To: Sandy Murphy's message of Thu, 20 Jun 91 19:58:58 EDT <9106202358.AA25006@TIS.COM> Subject: select Sender: melasv!paul@net.uu.uunet Sandy, Yes, @ is the wrong thing to use. I discovered that dealing with uninitialised state machines. Just make a direct statement about x: "!x. P x ==> Q", or whatever. About the only time I have needed to use @ directly is as part of a witness for existence proofs. Paul.