[Termtools] TRS/Zantema - z12

[Salvador Lucas]

Dear Johannes,

I think that the proof reported by AProVE is
clear. We use polynomial interpretations to
remove one of the two cycles and Hirokawa and
Middeldorp's subterm criterion for the other.

Do you see any concrete problem?

Best,

Salvador.

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.


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