[Termtools] [Cime-club] problem with Coccinelle's RPO?

[Frederic Blanqui]

Pierre Courtieu a écrit :
> Hello to both of you. First thank you for using coccinelle!
> 
> There is no problem with symbol equivalence in rpo definition of
> coccinelle. Actually afs and symbol equivalence are just instances of
> well foundedness proofs by "inverse image" theorem. This works very
> well in Cime certificates.
> 
> If you want to apply an afs, you need to apply a function (doing
> projection or removing arguments) to your terms before applying your
> ordering. It is well known that you obtain a well founded ordering if
> the initial ordering was.
> 
> If moreover you need to consider symbol f equivalent to g, then it is
> enough to modify the afs function in such a way that it replaces all
> occurrence of f by g.

Does the CPF format allow this?