[Termtools] Re: buggy proofs

[Johannes Waldmann]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1


>
> Consider MU-TERM for instance. We find the polynomial
> interpretations with rational coefficients that it (quickly)
> generates very interesting.

So do we. -  Salvador, what are the proofs where muterm "needs"
non-integers?
Can you make them available elsewhere, for reference?

> Since the bug is due to narrowing, it is very easy to filter out
> wrong proofs.

That is a possibility that we did not discuss.
You mean, just grep for "narrowing" and remove only those proofs.

I guess it's technically possible, but do we want this? Claude?

Would this open a "can of worms" (i.e. will there be other instances
of such after-the-fact selections?)


Best regards, Johannes.

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.2 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFGbXa83ZnXZuOVyMIRAt1wAJoC6f5ePqVZYOjKoICKBD3wROGjtgCgnygm
8H15CwArxXigRmw3Fig+wcY=
=/bBV
-----END PGP SIGNATURE-----