[opentheory-users] the Unwanted namespace

[Ramana Kumar]

>> Currently the tool is failing to process an article because at
>> some point an extra Unwanted.id means two terms that should be
>> alpha-convertible aren't. (But I don't think it's the first occurrence
>> of Unwanted.id in the article.)
>
> Is there any way of reducing your problem to a simple case that I could look at?
>

Maybe - any suggestions? In the meantime the complete (gzipped)
article is available here http://cam.xrchz.net/llist.art.gz. Maybe
running opentheory with some extra debugging code to see whatever it
does to Unwanted.id tags during reading this article will be
helpful...

FYI the error I get is

...
in ObjectProv.mkEqMp:
in Thm.eqMp:
terms not alpha-equivalent:
     Number.Natural.+ (Number.Numeral.bit2 Number.Numeral.zero)
       (Number.Numeral.bit1 Number.Numeral.zero) =
     Number.Natural.+ (Number.Numeral.bit2 Number.Numeral.zero)
       (Number.Numeral.bit1 Number.Numeral.zero)
  vs Number.Natural.+ (Number.Numeral.bit2 Number.Numeral.zero)
       (Number.Numeral.bit1 Number.Numeral.zero) =
     Unwanted.id
       (Number.Natural.+ (Number.Numeral.bit2 Number.Numeral.zero)
          (Number.Numeral.bit1 Number.Numeral.zero))
different term structure at path 10 subterms:
     Number.Natural.+ (Number.Numeral.bit2 Number.Numeral.zero)
  vs Unwanted.id