[Termtools] Re: SRS/Zantema/z090

[Johannes Waldmann]

Christian, thanks for the acknowledgment.

Here is some empirical evidence: I am running TTT2
on randomly generated looping SRSs
(so far, 7 * 12 CPU hours @ 3 GHz, on some idle machines)
and it did not claim any of them terminating...

Still, this is no substitute for
(1) formally describing the transformation
and at least (2) indicating a correctness proof.
I'd appreciate if you'd do (1) before the weekend (i.e. now).
(If you don't have it in LaTeX, we can also read ML ...)
I do not understand why you need (or want?) that additional letter.

Hans - is it true that z090 then would be the first
non-prim-rec SRS with an automatic termination proof?

But then I wonder why TTT2 cannot also do jw3, which is rather similar
http://www.lri.fr/%7Emarche/termination-competition/2007/webform.cgi?command=viewpb&file=srs-standard.db&id=SRS.Waldmann.jw3.srs

Best regards, Johannes.