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:08:21 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA14139;
          Mon, 3 May 93 09:58:44 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from leopard.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) 
          id AA14134; Mon, 3 May 93 09:58:37 -0700
Received: by leopard.cs.uidaho.edu (16.7/1.34) id AA08710;
          Mon, 3 May 93 09:59:12 -0700
From: coe@leopard.cs.uidaho.edu (Mike Coe)
Message-Id: <9305031659.AA08710@leopard.cs.uidaho.edu>
Subject: help
To: info-hol@ted.cs.uidaho.edu
Date: Mon, 3 May 93 9:59:12 PDT
Mailer: Elm [revision: 66.33]



Is there a way prove the following in HOL:



((t-1)+1) = t


I have tried the reduce library with no luck, and I have
tried Phil Windley's normalize tactics with no luck.

Any help is appreciated.



mike
coe@leopard.cs.uidaho.edu