Return-Path: <John.Harrison-request@cl.cam.ac.uk>
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:21:27 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA14193;
          Mon, 3 May 93 10:12:43 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA14188;
          Mon, 3 May 93 10:12:32 -0700
Received: from puffin.cl.cam.ac.uk (user btg (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Mon, 3 May 1993 18:12:20 +0100
To: coe@leopard.cs.uidaho.edu (Mike Coe)
Cc: info-hol@ted.cs.uidaho.edu
Subject: Re: help
In-Reply-To: Your message of Mon, 03 May 93 09:59:12 -0700. <9305031659.AA08710@leopard.cs.uidaho.edu>
Date: Mon, 03 May 93 18:12:16 +0100
From: Brian Graham <Brian.Graham@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:103880:930503171223"@cl.cam.ac.uk>

> Is there a way prove the following in HOL:

> ((t-1)+1) = t


er, hopefully not ...

for if:

 |- !t. ((t-1)+1) = t

we would get:

  |- (0-1)+1 = 0
      
  |- 0 + 1 = 0

  |- 1 = 0

  |- F

--brian