Re: [isabelle] size_change raises DUP
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"
termination apply size_change
I'll look for a fix...
This archive was generated by a fusion of
Pipermail (Mailman edition) and