[opentheory-users] the Unwanted namespace

[Ramana Kumar]

Will your scheme for eliminating Unwanted.id work in terms where it
does not appear fully applied, but can still be eliminated?
Specifically, when Unwanted.id is composed with another function.

On Tue, Dec 6, 2011 at 6:44 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> Thanks for making it quicker :)
>
> Now, the only place where Unwanted.id seems not to be erased is in an
> apparent axiom required by my article.
> Can you confirm that the article is actually trying to define Unwanted.id?
> I generated the article from a HOL4 theory that I don't think should
> be defining anything mapped to Unwanted.id, so I'm a bit confused
> about that at the moment...
>
> On Tue, Dec 6, 2011 at 4:58 AM, Joe Hurd <joe at gilith.com> wrote:
>> Hi Ramana,
>>
>> I fixed a performance bug in the proof rewriting, and your example
>> goes through pretty quickly now (see below). The fix is both pushed
>> and released in the latest version of the opentheory tool.
>>
>> Cheers,
>>
>> Joe
>>
>> ________________________________________________________________
>>
>> dimholt:~/dev/opentheory$ gzcat ~/Desktop/ll.art.gz | time
>> bin/mlton/opentheory info --inference article:-
>> WARNING: 38 objects left on the stack by -
>> WARNING: 473,658 objects left in the dictionary by -
>> Primitive inferences:
>> eqMp ............ 150,377
>> deductAntisym ... 129,584
>> subst ............ 76,065
>> appThm ........... 20,748
>> assume ........... 18,086
>> refl .............. 9,363
>> betaConv .......... 7,461
>> absThm ............ 4,564
>> axiom ............... 193
>> defineConst .......... 25
>> defineTypeOp .......... 1
>> Total ........... 416,467
>>       24.40 real
>>       15.30 user
>>         9.07 sys
>>
>> dimholt:~/dev/opentheory$ time bin/mlton/opentheory info --inference
>> foo.art Primitive inferences:
>> eqMp ............. 68,100
>> subst ............ 56,228
>> deductAntisym .... 51,689
>> appThm ........... 17,378
>> betaConv .......... 6,866
>> refl .............. 6,325
>> absThm ............ 4,267
>> assume ............ 1,608
>> axiom ............... 190
>> defineConst .......... 26
>> defineTypeOp .......... 1
>> Total ........... 212,678
>>
>> real    0m5.289s
>> user    0m5.027s
>> sys     0m0.256s
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list