MAYBE Problem: *(x,*(minus(y),y)) -> *(minus(*(y,y)),x) Proof: DP Processor: DPs: *#(x,*(minus(y),y)) -> *#(y,y) *#(x,*(minus(y),y)) -> *#(minus(*(y,y)),x) TRS: *(x,*(minus(y),y)) -> *(minus(*(y,y)),x) Restore Modifier: DPs: *#(x,*(minus(y),y)) -> *#(y,y) *#(x,*(minus(y),y)) -> *#(minus(*(y,y)),x) TRS: *(x,*(minus(y),y)) -> *(minus(*(y,y)),x) SCC Processor: #sccs: 1 #rules: 2 #arcs: 4/4 DPs: *#(x,*(minus(y),y)) -> *#(y,y) *#(x,*(minus(y),y)) -> *#(minus(*(y,y)),x) TRS: *(x,*(minus(y),y)) -> *(minus(*(y,y)),x) Open