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