Dear all,
for proving relative termination SN(R/S), a very crude method is to infer it from SN(R \cup S).
Does the CPF format (the CeTA verifier) have a provision for that?
- Johannes.
NB: crude, but powerful, on current SRS_Relative benchmarks, see our WST contribution ...