[Termtools] Re: CPF/CeTA: split for relative termination?

Dear all, to "close" this issue:

can CPF/CeTA do "split" for relative termination?

yes it can - and matchbox is using it now. René explained to me that a design principle in CeTA is (I am paraphrasing) "everything is relative" : a TRS always is a pair (R,S) of sets of (strict and weak) rules, and where this does not make sense, the union R+S is considered. - Johannes.