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) CDG 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: 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: 1 #rules: 12 #arcs: 144/256 DPs: minus#(*(x,y)) -> minus#(minus(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(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: dim=1 interpretation: [minus#](x0) = 5x0, [f](x0) = 0, [*](x0, x1) = x0 + x1 + 5, [+](x0, x1) = x0 + x1 + 5, [minus](x0) = x0 orientation: minus#(*(x,y)) = 5x + 5y + 25 >= 5y = minus#(minus(minus(y))) minus#(*(x,y)) = 5x + 5y + 25 >= 5x = minus#(minus(minus(x))) minus#(*(x,y)) = 5x + 5y + 25 >= 5x = minus#(minus(x)) minus#(*(x,y)) = 5x + 5y + 25 >= 5x = minus#(x) minus#(*(x,y)) = 5x + 5y + 25 >= 5y = minus#(minus(y)) minus#(*(x,y)) = 5x + 5y + 25 >= 5y = minus#(y) minus#(+(x,y)) = 5x + 5y + 25 >= 5x = minus#(minus(minus(x))) minus#(+(x,y)) = 5x + 5y + 25 >= 5x = minus#(minus(x)) minus#(+(x,y)) = 5x + 5y + 25 >= 5x = minus#(x) minus#(+(x,y)) = 5x + 5y + 25 >= 5y = minus#(minus(minus(y))) minus#(+(x,y)) = 5x + 5y + 25 >= 5y = minus#(minus(y)) minus#(+(x,y)) = 5x + 5y + 25 >= 5y = minus#(y) minus(minus(x)) = x >= x = x minus(+(x,y)) = x + y + 5 >= x + y + 5 = *(minus(minus(minus(x))),minus(minus(minus(y)))) minus(*(x,y)) = x + y + 5 >= x + y + 5 = +(minus(minus(minus(x))),minus(minus(minus(y)))) f(minus(x)) = 0 >= 0 = 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