[Termtools] TRS/Zantema - z12

[Peter Schneider-Kamp]

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

Johannes Waldmann wrote:
> I am having trouble understanding this proof:
> http://www.lri.fr/%7Emarche/termination-competition/2006/webform.cgi?command=viewres&tool=muterm&prob=TRS.Zantema.z12.trs
> 
> 
> This is an encoding of Zantema's system aabb -> bbbaaa
> So I'd expect it requires RFC match-bounds (Aprove does this)
> or matrices (Jambox does this).
> I don't understand how Muterm can do without either.

My guess is, that this is a bug in the computation
of the dependency graph. The dependency pairs as given
by MU-TERM are:

- -> Dependency pairs:
nF_f(x,a(a(b(b(y))))) -> nF_f(a(a(a(b(b(b(x)))))),y)
nF_f(a(x),y) -> nF_f(x,a(y))
nF_f(b(x),y) -> nF_f(x,b(y))

If we label them by 1 to 3 from top to bottom we
obtain the following dependency graph:

digraph depgraph {
1 [label="nF_f(x,a(a(b(b(y))))) -> nF_f(a(a(a(b(b(b(x)))))),y)"];
2 [label="nF_f(a(x),y) -> nF_f(x,a(y))"];
3 [label="nF_f(b(x),y) -> nF_f(x,b(y))"];
1 -> 1;
1 -> 2;
2 -> 1;
2 -> 2;
2 -> 3;
3 -> 2;
3 -> 3;
}

But MU-TERM seems to loose either 2 -> 3 or
3 -> 2 (or both):

- -> -> Dependency pairs in cycle:
nF_f(x,a(a(b(b(y))))) -> nF_f(a(a(a(b(b(b(x)))))),y)
nF_f(a(x),y) -> nF_f(x,a(y))

Best regards,
Peter
- --
Peter Schneider-Kamp   mailto:psk at informatik.rwth-aachen.de
LuFG Informatik II     http://www-i2.informatik.rwth-aachen.de/~nowonder
RWTH Aachen            phone: ++49 241 80-21211
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.3 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFEkn113VbrCXkKHhwRAugfAJsEO0rNINI7i5M/hpVbgQ9RlUfWdACglJXp
m98+d8BRxrTbbouxjNoKoGU=
=pRDR
-----END PGP SIGNATURE-----

_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools