Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: 15 Apr 92 19:42 +0100
From: Jeffrey Joyce <joyce@ca.ubc.cs>
To: info-hol <info-hol@edu.uidaho.cs.ted>
Message-Id: <4584*joyce@cs.ubc.ca>
Subject: arithmetic challenge

Indeed there was a typo in the "maybe-theorem" I proposed yesterday.
Several people have the spotted the typo:

    ... the sub-term (B DIV ((2 EXP i) MOD 2)) should have been
    ((B DIV (2 EXP i)) MOD 2).

I had the brackets right (I think) when I described the context, eg.,

    S := (S DIV 2) + (((B DIV (2 EXP I)) MOD 2) * A * (2 EXP (N-1)));

... but unfortunately, they wandered out of place when hand-generating
the verification condition.

Thus, the "corrected" version of the maybe-theorem is:

"!A B C n i.
  i < n ==>
  (((((2 EXP (n - i)) * (A * (B MOD (2 EXP i)))) + (C DIV (2 EXP i))) DIV
    2) +
   (((B DIV (2 EXP i)) MOD 2) * (A * (2 EXP (n - 1)))) =
   ((2 EXP (n - (i + 1))) * (A * (B MOD (2 EXP (i + 1))))) +
   (C DIV (2 EXP (i + 1))))"

I still regard this as a "maybe-theorem" .... I haven't had a
chance to check it very carefully to see if there are any further
typo's ... and indeed, it might still be a non-theorem beyond from
simple typo's.

If anyone generates a HOL proof for this maybe-theorem, it would
interesting to know how many new (== non-built-in) lemmas were developed
as part of the effort (and indeed the time spent discovering/proving these
lemmas should be counted as part of the overall effort).

My thanks to those who spotted the typo and provided counter-examples.