[Termtools] SRS/Zantema/z090?

[Johannes Waldmann]

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

Aart, thanks for the z090 analysis.

I wonder if there is a very direct way to convince oneself
of the correctness of the proof: since the "semantics" of z090 is known
(see Touzet's paper), it is easy to construct long derivations.


If it was just a proof by interpretation, one could compute
the interpretation for each step and see that it actually decreaes.

What could be done w.r.t. the DP setting? There is a problem
that most of the statements are "if there is an infinite derivation,
then there is some derivation of a special form"
and we cannot fulfil the premise. Still, there must be something?

Oh, and could you provide a TTT2 version that produces XML output
also for self-labelling proofs (even if Rainbow does not understand it
currently -
other programs might want to read your proof output.)

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

iD8DBQFGbXok3ZnXZuOVyMIRAgoWAJ9cB8h+bR23BgSJd5K2iFQPwGWqogCfTxZ3
zoOUdTFv6JDDuNwwV0F2D/8=
=rU+C
-----END PGP SIGNATURE-----