My code works fine on this article. The problem was my CGI script. It should be fixed now. (It had a call to runhaskell n2b.hs which got confused when called from another directory, so now I've given it an absolute path to n2b.hs.) <div class="gmail_quote">On Thu, Apr 5, 2012 at 11:10 PM, Joe Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> Hi Ramana, <div class="im"> > 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...) </div>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))) <div class="im"> > 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... </div>Your algorithm looks absolutely fine, and should scale up to any size of natural number that a theorem prover could conceivably process. Cheers, Joe _______________________________________________ opentheory-users mailing list <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> <a href="http://www.gilith.com/mailman/listinfo/opentheory-users" target="_blank">http://www.gilith.com/mailman/listinfo/opentheory-users</a> </blockquote></div>