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)))) TDG 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)) -> minus#(minus(minus(f(x)))) f#(minus(x)) -> f#(x) -> f#(minus(x)) -> minus#(minus(f(x))) f#(minus(x)) -> f#(x) -> f#(minus(x)) -> minus#(f(x)) f#(minus(x)) -> f#(x) -> f#(minus(x)) -> f#(x) f#(minus(x)) -> minus#(f(x)) -> minus#(*(x,y)) -> minus#(minus(minus(x))) f#(minus(x)) -> minus#(f(x)) -> minus#(*(x,y)) -> minus#(minus(x)) f#(minus(x)) -> minus#(f(x)) -> minus#(*(x,y)) -> minus#(x) f#(minus(x)) -> minus#(f(x)) -> minus#(*(x,y)) -> minus#(minus(minus(y))) f#(minus(x)) -> minus#(f(x)) -> minus#(*(x,y)) -> minus#(minus(y)) f#(minus(x)) -> minus#(f(x)) -> minus#(*(x,y)) -> minus#(y) f#(minus(x)) -> minus#(f(x)) -> minus#(+(x,y)) -> minus#(minus(minus(x))) f#(minus(x)) -> minus#(f(x)) -> minus#(+(x,y)) -> minus#(minus(x)) f#(minus(x)) -> minus#(f(x)) -> minus#(+(x,y)) -> minus#(x) f#(minus(x)) -> minus#(f(x)) -> minus#(+(x,y)) -> minus#(minus(minus(y))) f#(minus(x)) -> minus#(f(x)) -> minus#(+(x,y)) -> minus#(minus(y)) f#(minus(x)) -> minus#(f(x)) -> minus#(+(x,y)) -> minus#(y) 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#(minus(x)) f#(minus(x)) -> minus#(minus(f(x))) -> minus#(*(x,y)) -> minus#(x) 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#(minus(y)) f#(minus(x)) -> minus#(minus(f(x))) -> minus#(*(x,y)) -> minus#(y) 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#(minus(x)) f#(minus(x)) -> minus#(minus(f(x))) -> minus#(+(x,y)) -> minus#(x) 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#(minus(y)) f#(minus(x)) -> minus#(minus(f(x))) -> minus#(+(x,y)) -> minus#(y) 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#(minus(x)) 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(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#(y) 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#(minus(x)) 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(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#(y) 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#(minus(x)) minus#(*(x,y)) -> minus#(minus(minus(y))) -> minus#(*(x,y)) -> minus#(x) 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#(minus(y)) minus#(*(x,y)) -> minus#(minus(minus(y))) -> minus#(*(x,y)) -> minus#(y) 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#(minus(x)) minus#(*(x,y)) -> minus#(minus(minus(y))) -> minus#(+(x,y)) -> minus#(x) 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#(minus(y)) minus#(*(x,y)) -> minus#(minus(minus(y))) -> minus#(+(x,y)) -> minus#(y) 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#(minus(x)) minus#(*(x,y)) -> minus#(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#(minus(minus(x))) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(minus(minus(x))) -> minus#(*(x,y)) -> minus#(y) 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#(minus(x)) minus#(*(x,y)) -> minus#(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#(minus(minus(x))) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(minus(minus(x))) -> minus#(+(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(y) minus#(*(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(*(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(*(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(y) 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#(minus(x)) minus#(+(x,y)) -> minus#(minus(minus(y))) -> minus#(*(x,y)) -> minus#(x) 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#(minus(y)) minus#(+(x,y)) -> minus#(minus(minus(y))) -> minus#(*(x,y)) -> minus#(y) 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#(minus(x)) minus#(+(x,y)) -> minus#(minus(minus(y))) -> minus#(+(x,y)) -> minus#(x) 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#(minus(y)) minus#(+(x,y)) -> minus#(minus(minus(y))) -> minus#(+(x,y)) -> minus#(y) 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#(minus(x)) minus#(+(x,y)) -> minus#(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#(minus(minus(x))) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(minus(minus(x))) -> minus#(*(x,y)) -> minus#(y) 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#(minus(x)) minus#(+(x,y)) -> minus#(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#(minus(minus(x))) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(minus(minus(x))) -> minus#(+(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(*(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(minus(y)) -> minus#(+(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(*(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(y) minus#(+(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(+(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(minus(y))) minus#(+(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(y)) minus#(+(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(y) 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#(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))) 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)))) Arctic Interpretation Processor: dimension: 1 interpretation: [minus#](x0) = x0, [f](x0) = -8x0 + 0, [*](x0, x1) = x0 + 2x1, [+](x0, x1) = x0 + 2x1, [minus](x0) = x0 orientation: minus#(+(x,y)) = x + 2y >= y = minus#(y) minus#(+(x,y)) = x + 2y >= y = minus#(minus(y)) minus#(+(x,y)) = x + 2y >= y = minus#(minus(minus(y))) minus#(+(x,y)) = x + 2y >= x = minus#(x) minus#(+(x,y)) = x + 2y >= x = minus#(minus(x)) minus#(+(x,y)) = x + 2y >= x = minus#(minus(minus(x))) minus#(*(x,y)) = x + 2y >= y = minus#(y) minus#(*(x,y)) = x + 2y >= y = minus#(minus(y)) minus#(*(x,y)) = x + 2y >= y = minus#(minus(minus(y))) minus#(*(x,y)) = x + 2y >= x = minus#(x) minus#(*(x,y)) = x + 2y >= x = minus#(minus(x)) minus#(*(x,y)) = x + 2y >= x = minus#(minus(minus(x))) minus(minus(x)) = x >= x = x minus(+(x,y)) = x + 2y >= x + 2y = *(minus(minus(minus(x))),minus(minus(minus(y)))) minus(*(x,y)) = x + 2y >= x + 2y = +(minus(minus(minus(x))),minus(minus(minus(y)))) f(minus(x)) = -8x + 0 >= -8x + 0 = minus(minus(minus(f(x)))) problem: DPs: minus#(+(x,y)) -> minus#(x) minus#(+(x,y)) -> minus#(minus(x)) minus#(+(x,y)) -> minus#(minus(minus(x))) minus#(*(x,y)) -> minus#(x) minus#(*(x,y)) -> minus#(minus(x)) minus#(*(x,y)) -> minus#(minus(minus(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)))) Arctic Interpretation Processor: dimension: 1 interpretation: [minus#](x0) = x0, [f](x0) = x0 + 4, [*](x0, x1) = 1x0 + x1 + 1, [+](x0, x1) = 1x0 + x1 + 1, [minus](x0) = x0 orientation: minus#(+(x,y)) = 1x + y + 1 >= x = minus#(x) minus#(+(x,y)) = 1x + y + 1 >= x = minus#(minus(x)) minus#(+(x,y)) = 1x + y + 1 >= x = minus#(minus(minus(x))) minus#(*(x,y)) = 1x + y + 1 >= x = minus#(x) minus#(*(x,y)) = 1x + y + 1 >= x = minus#(minus(x)) minus#(*(x,y)) = 1x + y + 1 >= x = minus#(minus(minus(x))) minus(minus(x)) = x >= x = x minus(+(x,y)) = 1x + y + 1 >= 1x + y + 1 = *(minus(minus(minus(x))),minus(minus(minus(y)))) minus(*(x,y)) = 1x + y + 1 >= 1x + y + 1 = +(minus(minus(minus(x))),minus(minus(minus(y)))) f(minus(x)) = x + 4 >= x + 4 = 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