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