On 7/26/22 13:25, YAMADA, Akihisa wrote:
.. conflict ... NaTT...
that's in TRS-Relative. This makes me a bit skeptical about SRS-relative "new results" (NB: I like this, and other options for navigation that you implemented) where NaTT claims to solve Zantema_06_relative/rel{11,12}
But maybe (certainly) I don't understand your paper (JAR 2017) well enough.
rel11 is "obviously" terminating but the argument seems to require arithmetics. I think Hans crafted these to show exactly that. Was there an accompanying paper? (*)
I once found a proof (matrices of dimension 5) for rel12, but never for rel11.
Best regards, Johannes.
(*) some of these problems had annotations when submitted - but these were lost in XMLification?
tpdb-4.0/SRS/Zantema06/rel11.srs:
(RULES b p b -> b a p b , p ->= a p a , a p a a ->= p ) (COMMENT: invariant after first rule: left from p more a's than right from p )