Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Thu, 25 Feb 1993 08:29:08 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA20643;
          Thu, 25 Feb 93 00:15:21 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA20636;
          Thu, 25 Feb 93 00:15:04 -0800
Received: from scoter.cl.cam.ac.uk (user jvt (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Thu, 25 Feb 1993 08:14:14 +0000
Received: by scoter.cl.cam.ac.uk (4.1/SMI-3.0DEV3) id AA20145;
          Thu, 25 Feb 93 08:14:08 GMT
Date: Thu, 25 Feb 93 08:14:08 GMT
From: John.Van-Tassel@uk.ac.cam.cl
Message-Id: <9302250814.AA20145@scoter.cl.cam.ac.uk>
To: info-hol@edu.uidaho.cs.ted, toal@edu.ucla.cs
Subject: Re: Arithmetic

Hi,

Try the library "arith":

JVT

   albatross> hol


   ===========================================================================
	    HOL88 Version 2.01 (SUN4/AKCL), built on 4/12/92
   ===========================================================================

   #load_library `arith`;;
   Loading library arith ...
   Loading library reduce ...
   Extending help search path.
   Loading boolean conversions........
   Loading arithmetic conversions..................
   Loading general conversions, rule and tactic.....
   Library reduce loaded.
   .Updating help search path
   .......................................................................................................................................................................................................................................................................................
   Library arith loaded.
   () : void

   #timer true;;
   false : bool
   Run time: 0.0s

   #"k =  k1 + ((k1' + (1 + 1)) + 1)";;
   "k = k1 + ((k1' + (1 + 1)) + 1)" : term
   Run time: 0.0s

   #let tm1 = "k =  k1 + ((k1' + (1 + 1)) + 1)"
   #and tm2 = "k1 < k"
   #and tm3 = "k1' < k";;
   tm1 = "k = k1 + ((k1' + (1 + 1)) + 1)" : term
   tm2 = "k1 < k" : term
   tm3 = "k1' < k" : term
   Run time: 0.0s

   #"^tm1 ==> ^tm2";;
   "(k = k1 + ((k1' + (1 + 1)) + 1)) ==> k1 < k" : term
   Run time: 0.0s

   #ARITH_CONV it;;
   |- (k = k1 + ((k1' + (1 + 1)) + 1)) ==> k1 < k = T
   Run time: 0.5s
   Intermediate theorems generated: 213

   #"^tm1 ==> ^tm3";;
   "(k = k1 + ((k1' + (1 + 1)) + 1)) ==> k1' < k" : term
   Run time: 0.0s

   #ARITH_CONV it;;
   |- (k = k1 + ((k1' + (1 + 1)) + 1)) ==> k1' < k = T
   Run time: 0.5s
   Intermediate theorems generated: 208