Dear Johannes,

yes, this is already supported according to CPF:

there is the sIsEmpty-proof which takes a termination proof for a single TRS (R union S) as argument.

doku: state that the R/S is relative terminating by termination of R since S has no rules. (or more generally: prove termination of R union S.)

Best, René

Am 09.08.2023 um 09:33 schrieb Johannes Waldmann johannes.waldmann@htwk-leipzig.de:

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 ... _______________________________________________ Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de