YES Time: 0.011051 TRS: {f X -> g()} DP: DP: {} TRS: {f X -> g()} Qed