[opentheory-users] a standalone tactic translating numeral encodings

[Joe Hurd]

Hi Ramana,

> My guess is that you're generating an article with HOLLight.BIT2 rather than
> Number.Natural.bit2, but I haven't actually run your attempt.
> If that's not the problem it would be helpful if you could send me the
> article that gets passed to the web tactic (or maybe I should have some
> infrastructure for saving it...)

I've attached the article encoding the goal: FYI the opentheory
summary for it is:

$ opentheory info n2b-goal.art
3 input type operators: -> bool Number.Natural.natural
5 input constants: F Function.K Number.Natural.bit1 Number.Natural.bit2
  Number.Natural.zero
1 assumption:
  |- Function.K F
       (Number.Natural.bit2 (Number.Natural.bit1 (Number.Natural.bit2 0)))
1 theorem:
  |- Function.K F
       (Number.Natural.bit2 (Number.Natural.bit1 (Number.Natural.bit2 0)))

> The function n2b near the top of the file is the algorithm.
> It's been a while, so let's see if I can figure out the algorithm just by
> reading that code...

Your algorithm looks absolutely fine, and should scale up to any size
of natural number that a theorem prover could conceivably process.

Cheers,

Joe
-------------- next part --------------
A non-text attachment was scrubbed...
Name: n2b-goal.art
Type: application/octet-stream
Size: 899 bytes
Desc: not available
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20120405/76552d0a/attachment.obj>