MAYBE 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))) Restore Modifier: 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)))) 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)))) Open