[Termtools] Re: buggy proofs

[Salvador Lucas]

Johannes Waldmann wrote:

>So do we. -  Salvador, what are the proofs where muterm "needs"
>non-integers?
>
In the meantime, I can say that our preliminary (local) benchmarks tell 
us that we
need to use rational coefficients in around 10% of our proofs of 
termination of
rewriting. Here 'need' means that we could *not* obtain a proof using 
natural
coefficientes in {0,1} or {0,1,2}. Then, we switch to rationals.

Best,

Salvador.