YES Problem: f(0()) -> f(0()) 0() -> 1() Proof: DP Processor: DPs: f#(0()) -> f#(0()) TRS: f(0()) -> f(0()) 0() -> 1() EDG Processor: DPs: f#(0()) -> f#(0()) TRS: f(0()) -> f(0()) 0() -> 1() graph: Qed