[Termtools] polytool proof output

[Johannes Waldmann]

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

ManhThang Nguyen wrote:
>
>
> Do you think that I should provide a version which gives
> information about the proof? However, then somebody has to run the
> test again.
The requirements are that the first line is YES or NO,
and the following lines provide some explanation
that conveys the essence of the termination proof to a human.

I suggest you quickly provide an executable that adds proof output,
and Claude runs it when computer time will become available.

If the status (YES/NO/MAYBE) of the new output
differs from the previous output (that is now in the table),
we will consider it as MAYBE
(but I see no reason why this should happen).

Formally, this procedure is a suggestion that still has to be approved
by the competition committee (consisting of Claude, Hans and me).
Also, if any of the competitors sees any problems, then please speak up.

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

iD8DBQFGZIhC3ZnXZuOVyMIRAkXSAKC2ZusU8vIPfejcJnG/CMG5PXnc0QCgttLg
uZiDwk6ytN3/TgFquhSGAcU=
=y+qg
-----END PGP SIGNATURE-----