[Termtools] TRS/Zantema - z12

[Johannes Waldmann]

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.
-- 
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/ -------

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