Hi Clemens, > I'm not familiar with the termination argument for abbreviations, but certainly we can say that abbreviations define a reduction system (in fact a rewrite system), and I would assume that there are no cycles and infinite paths. Now my patch will clone part of this system, introducing additional nodes and transitions, but I don't see how it would introduce cycles if there were no cycles without it. It could introduce infinite chains, but only for infinite chains of interpretations. The latter are not allowed by the roundup algorithm. Am I missing something?
Well, I am not so sure about the cycles:
As a starting point, take A --> B --> C.
Let the interpretation morphism map these as follows:
A |-> D
B |-> E
C |-> D
Then under the morphism we have D --> E --> D.
But maybe this is forbidden by the properties of a morphism itself.
I did not work to contrieve a meaningful counterexample yet.
Cheers,
Florian
>
> Clemens
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
