MAYBE Problem: plus(plus(X,Y),Z) -> plus(X,plus(Y,Z)) times(X,s(Y)) -> plus(X,times(Y,X)) Proof: DP Processor: DPs: plus#(plus(X,Y),Z) -> plus#(Y,Z) plus#(plus(X,Y),Z) -> plus#(X,plus(Y,Z)) times#(X,s(Y)) -> times#(Y,X) times#(X,s(Y)) -> plus#(X,times(Y,X)) TRS: plus(plus(X,Y),Z) -> plus(X,plus(Y,Z)) times(X,s(Y)) -> plus(X,times(Y,X)) ADG Processor: DPs: plus#(plus(X,Y),Z) -> plus#(Y,Z) plus#(plus(X,Y),Z) -> plus#(X,plus(Y,Z)) times#(X,s(Y)) -> times#(Y,X) times#(X,s(Y)) -> plus#(X,times(Y,X)) TRS: plus(plus(X,Y),Z) -> plus(X,plus(Y,Z)) times(X,s(Y)) -> plus(X,times(Y,X)) graph: times#(X,s(Y)) -> times#(Y,X) -> times#(X,s(Y)) -> times#(Y,X) times#(X,s(Y)) -> times#(Y,X) -> times#(X,s(Y)) -> plus#(X,times(Y,X)) times#(X,s(Y)) -> plus#(X,times(Y,X)) -> plus#(plus(X,Y),Z) -> plus#(Y,Z) times#(X,s(Y)) -> plus#(X,times(Y,X)) -> plus#(plus(X,Y),Z) -> plus#(X,plus(Y,Z)) plus#(plus(X,Y),Z) -> plus#(Y,Z) -> plus#(plus(X,Y),Z) -> plus#(Y,Z) plus#(plus(X,Y),Z) -> plus#(Y,Z) -> plus#(plus(X,Y),Z) -> plus#(X,plus(Y,Z)) plus#(plus(X,Y),Z) -> plus#(X,plus(Y,Z)) -> plus#(plus(X,Y),Z) -> plus#(Y,Z) plus#(plus(X,Y),Z) -> plus#(X,plus(Y,Z)) -> plus#(plus(X,Y),Z) -> plus#(X,plus(Y,Z)) Restore Modifier: DPs: plus#(plus(X,Y),Z) -> plus#(Y,Z) plus#(plus(X,Y),Z) -> plus#(X,plus(Y,Z)) times#(X,s(Y)) -> times#(Y,X) times#(X,s(Y)) -> plus#(X,times(Y,X)) TRS: plus(plus(X,Y),Z) -> plus(X,plus(Y,Z)) times(X,s(Y)) -> plus(X,times(Y,X)) SCC Processor: #sccs: 2 #rules: 3 #arcs: 8/16 DPs: times#(X,s(Y)) -> times#(Y,X) TRS: plus(plus(X,Y),Z) -> plus(X,plus(Y,Z)) times(X,s(Y)) -> plus(X,times(Y,X)) Open DPs: plus#(plus(X,Y),Z) -> plus#(X,plus(Y,Z)) plus#(plus(X,Y),Z) -> plus#(Y,Z) TRS: plus(plus(X,Y),Z) -> plus(X,plus(Y,Z)) times(X,s(Y)) -> plus(X,times(Y,X)) Open