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...

Alex




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