YES Problem: *(i(x),x) -> 1() *(1(),y) -> y *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) Proof: DP Processor: DPs: *#(*(x,y),z) -> *#(y,z) *#(*(x,y),z) -> *#(x,*(y,z)) TRS: *(i(x),x) -> 1() *(1(),y) -> y *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) KBO Processor: argument filtering: pi(i) = 0 pi(*) = [0,1] pi(1) = [] pi(0) = [] pi(*#) = [0,1] usable rules: *(i(x),x) -> 1() *(1(),y) -> y *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) weight function: w0 = 1 w(*#) = w(0) = w(1) = w(i) = 1 w(*) = 0 precedence: *# ~ 0 ~ 1 ~ * ~ i problem: DPs: TRS: *(i(x),x) -> 1() *(1(),y) -> y *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) Qed