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)))) 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)))) Open 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)))) Open