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 )