Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 3 May 1993 18:28:05 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA14213; Mon, 3 May 93 10:18:49 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from Sun.COM by ted.cs.uidaho.edu (16.6/1.34) id AA14208; Mon, 3 May 93 10:18:34 -0700 Received: from Eng.Sun.COM (zigzag-bb.Corp.Sun.COM) by Sun.COM (4.1/SMI-4.1) id AA09793; Mon, 3 May 93 10:18:27 PDT Received: from lara.Eng.Sun.COM by Eng.Sun.COM (4.1/SMI-4.1) id AA15732; Mon, 3 May 93 10:18:17 PDT Received: by lara.Eng.Sun.COM (4.1/SMI-4.1) id AA14476; Mon, 3 May 93 10:21:37 PDT Date: Mon, 3 May 93 10:21:37 PDT From: Paul.Loewenstein@Eng.Sun.COM (Paul Loewenstein) Message-Id: <9305031721.AA14476@lara.Eng.Sun.COM> To: coe@leopard.cs.uidaho.edu, info-hol@ted.cs.uidaho.edu In-Reply-To: Mike Coe's message of Mon, 3 May 93 9:59:12 PDT <9305031659.AA08710@leopard.cs.uidaho.edu> Subject: help Content-Length: 427 No, because it's not a theorem (assuming t is a natural number). ((0 - 1)+1) = 1 ((SUC t - 1) + 1) = SUC t is a theorem, and is simple to prove. Paul Loewenstein Sun Microsystems Inc, Mailstop MPK 3-103, Staff Engineer 2550 Garcia Avenue, Mountain View, CA 94043, USA Formal Verification Tel: 415-688-9664 FAX: 415-688-9565 paul.loewenstein@eng.sun.com