YES Problem: minus(minus(x)) -> x minus(+(x,y)) -> *(minus(minus(minus(x))),minus(minus(minus(y)))) minus(*(x,y)) -> +(minus(minus(minus(x))),minus(minus(minus(y)))) f(minus(x)) -> minus(minus(minus(f(x)))) Proof: DP Processor: DPs: minus#(+(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(minus(minus(x))) f#(minus(x)) -> f#(x) f#(minus(x)) -> minus#(f(x)) f#(minus(x)) -> minus#(minus(f(x))) f#(minus(x)) -> minus#(minus(minus(f(x)))) TRS: minus(minus(x)) -> x minus(+(x,y)) -> *(minus(minus(minus(x))),minus(minus(minus(y)))) minus(*(x,y)) -> +(minus(minus(minus(x))),minus(minus(minus(y)))) f(minus(x)) -> minus(minus(minus(f(x)))) EDG Processor: DPs: minus#(+(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(minus(minus(x))) f#(minus(x)) -> f#(x) f#(minus(x)) -> minus#(f(x)) f#(minus(x)) -> minus#(minus(f(x))) f#(minus(x)) -> minus#(minus(minus(f(x)))) TRS: minus(minus(x)) -> x minus(+(x,y)) -> *(minus(minus(minus(x))),minus(minus(minus(y)))) minus(*(x,y)) -> +(minus(minus(minus(x))),minus(minus(minus(y)))) f(minus(x)) -> minus(minus(minus(f(x)))) graph: f#(minus(x)) -> f#(x) -> f#(minus(x)) -> f#(x) f#(minus(x)) -> f#(x) -> f#(minus(x)) -> minus#(f(x)) f#(minus(x)) -> f#(x) -> f#(minus(x)) -> minus#(minus(f(x))) f#(minus(x)) -> f#(x) -> f#(minus(x)) -> minus#(minus(minus(f(x)))) f#(minus(x)) -> minus#(f(x)) -> minus#(+(x,y)) -> minus#(y) f#(minus(x)) -> minus#(f(x)) -> minus#(+(x,y)) -> minus#(minus(y)) f#(minus(x)) -> minus#(f(x)) -> minus#(+(x,y)) -> minus#(minus(minus(y))) f#(minus(x)) -> minus#(f(x)) -> minus#(+(x,y)) -> minus#(x) f#(minus(x)) -> minus#(f(x)) -> minus#(+(x,y)) -> minus#(minus(x)) f#(minus(x)) -> minus#(f(x)) -> minus#(+(x,y)) -> minus#(minus(minus(x))) f#(minus(x)) -> minus#(f(x)) -> minus#(*(x,y)) -> minus#(y) f#(minus(x)) -> minus#(f(x)) -> minus#(*(x,y)) -> minus#(minus(y)) f#(minus(x)) -> minus#(f(x)) -> minus#(*(x,y)) -> minus#(minus(minus(y))) f#(minus(x)) -> minus#(f(x)) -> minus#(*(x,y)) -> minus#(x) f#(minus(x)) -> minus#(f(x)) -> minus#(*(x,y)) -> minus#(minus(x)) f#(minus(x)) -> minus#(f(x)) -> minus#(*(x,y)) -> minus#(minus(minus(x))) f#(minus(x)) -> minus#(minus(f(x))) -> minus#(+(x,y)) -> minus#(y) f#(minus(x)) -> minus#(minus(f(x))) -> minus#(+(x,y)) -> minus#(minus(y)) f#(minus(x)) -> minus#(minus(f(x))) -> minus#(+(x,y)) -> minus#(minus(minus(y))) f#(minus(x)) -> minus#(minus(f(x))) -> minus#(+(x,y)) -> minus#(x) f#(minus(x)) -> minus#(minus(f(x))) -> minus#(+(x,y)) -> minus#(minus(x)) f#(minus(x)) -> minus#(minus(f(x))) -> minus#(+(x,y)) -> minus#(minus(minus(x))) f#(minus(x)) -> minus#(minus(f(x))) -> minus#(*(x,y)) -> minus#(y) f#(minus(x)) -> minus#(minus(f(x))) -> minus#(*(x,y)) -> minus#(minus(y)) f#(minus(x)) -> minus#(minus(f(x))) -> minus#(*(x,y)) -> minus#(minus(minus(y))) f#(minus(x)) -> minus#(minus(f(x))) -> minus#(*(x,y)) -> minus#(x) f#(minus(x)) -> minus#(minus(f(x))) -> minus#(*(x,y)) -> minus#(minus(x)) f#(minus(x)) -> minus#(minus(f(x))) -> minus#(*(x,y)) -> minus#(minus(minus(x))) f#(minus(x)) -> minus#(minus(minus(f(x)))) -> minus#(+(x,y)) -> minus#(y) f#(minus(x)) -> minus#(minus(minus(f(x)))) -> minus#(+(x,y)) -> minus#(minus(y)) f#(minus(x)) -> minus#(minus(minus(f(x)))) -> minus#(+(x,y)) -> minus#(minus(minus(y))) f#(minus(x)) -> minus#(minus(minus(f(x)))) -> minus#(+(x,y)) -> minus#(x) f#(minus(x)) -> minus#(minus(minus(f(x)))) -> minus#(+(x,y)) -> minus#(minus(x)) f#(minus(x)) -> minus#(minus(minus(f(x)))) -> minus#(+(x,y)) -> minus#(minus(minus(x))) f#(minus(x)) -> minus#(minus(minus(f(x)))) -> minus#(*(x,y)) -> minus#(y) f#(minus(x)) -> minus#(minus(minus(f(x)))) -> minus#(*(x,y)) -> minus#(minus(y)) f#(minus(x)) -> minus#(minus(minus(f(x)))) -> minus#(*(x,y)) -> minus#(minus(minus(y))) f#(minus(x)) -> minus#(minus(minus(f(x)))) -> minus#(*(x,y)) -> minus#(x) f#(minus(x)) -> minus#(minus(minus(f(x)))) -> minus#(*(x,y)) -> minus#(minus(x)) f#(minus(x)) -> minus#(minus(minus(f(x)))) -> minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(minus(minus(y))) -> minus#(+(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(minus(minus(y))) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(minus(minus(y))) -> minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(minus(minus(y))) -> minus#(+(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(minus(minus(y))) -> minus#(+(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(minus(minus(y))) -> minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(minus(minus(y))) -> minus#(*(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(minus(minus(y))) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(minus(minus(y))) -> minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(minus(minus(y))) -> minus#(*(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(minus(minus(y))) -> minus#(*(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(minus(minus(y))) -> minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(minus(minus(x))) -> minus#(+(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(minus(minus(x))) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(minus(minus(x))) -> minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(minus(minus(x))) -> minus#(+(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(minus(minus(x))) -> minus#(+(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(minus(minus(x))) -> minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(minus(minus(x))) -> minus#(*(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(minus(minus(x))) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(minus(minus(x))) -> minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(minus(minus(x))) -> minus#(*(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(minus(minus(x))) -> minus#(*(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(minus(minus(x))) -> minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(minus(minus(y))) -> minus#(+(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(minus(minus(y))) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(minus(minus(y))) -> minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(minus(minus(y))) -> minus#(+(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(minus(minus(y))) -> minus#(+(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(minus(minus(y))) -> minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(minus(minus(y))) -> minus#(*(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(minus(minus(y))) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(minus(minus(y))) -> minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(minus(minus(y))) -> minus#(*(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(minus(minus(y))) -> minus#(*(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(minus(minus(y))) -> minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(minus(minus(x))) -> minus#(+(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(minus(minus(x))) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(minus(minus(x))) -> minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(minus(minus(x))) -> minus#(+(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(minus(minus(x))) -> minus#(+(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(minus(minus(x))) -> minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(minus(minus(x))) -> minus#(*(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(minus(minus(x))) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(minus(minus(x))) -> minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(minus(minus(x))) -> minus#(*(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(minus(minus(x))) -> minus#(*(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(minus(minus(x))) -> minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(minus(x))) SCC Processor: #sccs: 2 #rules: 13 #arcs: 184/256 DPs: f#(minus(x)) -> f#(x) TRS: minus(minus(x)) -> x minus(+(x,y)) -> *(minus(minus(minus(x))),minus(minus(minus(y)))) minus(*(x,y)) -> +(minus(minus(minus(x))),minus(minus(minus(y)))) f(minus(x)) -> minus(minus(minus(f(x)))) Subterm Criterion Processor: simple projection: pi(f#) = 0 problem: DPs: TRS: minus(minus(x)) -> x minus(+(x,y)) -> *(minus(minus(minus(x))),minus(minus(minus(y)))) minus(*(x,y)) -> +(minus(minus(minus(x))),minus(minus(minus(y)))) f(minus(x)) -> minus(minus(minus(f(x)))) Qed DPs: minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(y) TRS: minus(minus(x)) -> x minus(+(x,y)) -> *(minus(minus(minus(x))),minus(minus(minus(y)))) minus(*(x,y)) -> +(minus(minus(minus(x))),minus(minus(minus(y)))) f(minus(x)) -> minus(minus(minus(f(x)))) Matrix Interpretation Processor: dimension: 1 interpretation: [minus#](x0) = x0, [f](x0) = 1, [*](x0, x1) = x0 + x1 + 1, [+](x0, x1) = x0 + x1 + 1, [minus](x0) = x0 orientation: minus#(*(x,y)) = x + y + 1 >= x = minus#(minus(minus(x))) minus#(*(x,y)) = x + y + 1 >= x = minus#(minus(x)) minus#(*(x,y)) = x + y + 1 >= x = minus#(x) minus#(*(x,y)) = x + y + 1 >= y = minus#(minus(minus(y))) minus#(*(x,y)) = x + y + 1 >= y = minus#(minus(y)) minus#(*(x,y)) = x + y + 1 >= y = minus#(y) minus#(+(x,y)) = x + y + 1 >= x = minus#(minus(minus(x))) minus#(+(x,y)) = x + y + 1 >= x = minus#(minus(x)) minus#(+(x,y)) = x + y + 1 >= x = minus#(x) minus#(+(x,y)) = x + y + 1 >= y = minus#(minus(minus(y))) minus#(+(x,y)) = x + y + 1 >= y = minus#(minus(y)) minus#(+(x,y)) = x + y + 1 >= y = minus#(y) minus(minus(x)) = x >= x = x minus(+(x,y)) = x + y + 1 >= x + y + 1 = *(minus(minus(minus(x))),minus(minus(minus(y)))) minus(*(x,y)) = x + y + 1 >= x + y + 1 = +(minus(minus(minus(x))),minus(minus(minus(y)))) f(minus(x)) = 1 >= 1 = minus(minus(minus(f(x)))) problem: DPs: TRS: minus(minus(x)) -> x minus(+(x,y)) -> *(minus(minus(minus(x))),minus(minus(minus(y)))) minus(*(x,y)) -> +(minus(minus(minus(x))),minus(minus(minus(y)))) f(minus(x)) -> minus(minus(minus(f(x)))) Qed