(0) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
a → b
The relative TRS consists of the following S rules:
d → c(a, d)
(1) RelTRSEmissionProof (COMPLETE transformation)
The TRS S admits the following R-emitting loop:
d→c(a, d)
Therefore R/S does not terminate.
(2) NO