Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <03730-0@swan.cl.cam.ac.uk>; Wed, 15 Apr 1992 18:33:29 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06743; Wed, 15 Apr 92 10:22:38 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from eros.uknet.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA06739; Wed, 15 Apr 92 10:22:31 -0700 Received: from eccles.dsbc.icl.co.uk by eros.uknet.ac.uk with UUCP id <3461-0@eros.uknet.ac.uk>; Wed, 15 Apr 1992 17:18:12 +0100 Received: on eccles.dsbc.icl.co.uk over UUCP id AA16852; Wed, 15 Apr 92 16:20:19 BST Received: from wilfrid by iclbra.oasis.icl.co.uk (4.14/) id AA06187; Wed, 15 Apr 92 16:22:16 bst From: Rob Arthan Date: Wed, 15 Apr 92 16:15:52 BST Message-Id: <9204151515.4173.20@win.icl.co.uk> To: joyce@ca.ubc.cs Subject: Arithmetic Challenge Cc: info-hol@edu.uidaho.cs.ted There appears to be an error in the bracketing of Jeff's example of a theorem which is a bore to prove in HOL. The sub-term: (B DIV ((2 EXP i) MOD 2)) should, I think, actually read: ((B DIV (2 EXP i)) MOD 2) otherwise the division will be by zero for any i > 0. With this modification, I believe that an informal proof along the lines Jeff sketches works out ok. This is the sort of thing we have done some work towards making easier in ICL HOL, but I haven't worked up the courage or found the time to dive in yet. Rob Arthan. STOP PRESS: I see that Tom Melham found a counter-example using HOL, and indeed the counter-example sets i = 0.