Re: [isabelle] size_change raises DUP

Hi Andreas,

Thanks for the report. It seems that the graph decomposition cannot cope with the same recursive call occurring twice... (But the issue only occurs when graph decomposition actually happens since the plain scnp method does not succeed). Here is a more minimal example:

function f :: "nat => nat"
where "f x = f x + f x"
by auto
termination apply size_change

I'll look for a fix...


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.