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)) Restore Modifier: 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)) SCC Processor: #sccs: 1 #rules: 2 #arcs: 4/4 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [*#](x0, x1) = x0 + x1 + 1, [0] = 1, [1] = 0, [*](x0, x1) = x0 + x1 + 1, [i](x0) = 1 orientation: *#(*(x,y),z) = x + y + z + 2 >= y + z + 1 = *#(y,z) *#(*(x,y),z) = x + y + z + 2 >= x + y + z + 2 = *#(x,*(y,z)) *(i(x),x) = x + 2 >= 0 = 1() *(1(),y) = y + 1 >= y = y *(x,0()) = x + 2 >= 1 = 0() *(*(x,y),z) = x + y + z + 2 >= x + y + z + 2 = *(x,*(y,z)) problem: DPs: *#(*(x,y),z) -> *#(x,*(y,z)) TRS: *(i(x),x) -> 1() *(1(),y) -> y *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) Matrix Interpretation Processor: dimension: 1 interpretation: [*#](x0, x1) = x0, [0] = 1, [1] = 0, [*](x0, x1) = x0 + x1 + 1, [i](x0) = 1 orientation: *#(*(x,y),z) = x + y + 1 >= x = *#(x,*(y,z)) *(i(x),x) = x + 2 >= 0 = 1() *(1(),y) = y + 1 >= y = y *(x,0()) = x + 2 >= 1 = 0() *(*(x,y),z) = x + y + z + 2 >= x + y + z + 2 = *(x,*(y,z)) problem: DPs: TRS: *(i(x),x) -> 1() *(1(),y) -> y *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) Qed