MAYBE Problem: ackin(s(X),s(Y)) -> u21(ackin(s(X),Y),X) u21(ackout(X),Y) -> u22(ackin(Y,X)) Proof: DP Processor: DPs: ackin#(s(X),s(Y)) -> ackin#(s(X),Y) ackin#(s(X),s(Y)) -> u21#(ackin(s(X),Y),X) u21#(ackout(X),Y) -> ackin#(Y,X) TRS: ackin(s(X),s(Y)) -> u21(ackin(s(X),Y),X) u21(ackout(X),Y) -> u22(ackin(Y,X)) ADG Processor: DPs: ackin#(s(X),s(Y)) -> ackin#(s(X),Y) ackin#(s(X),s(Y)) -> u21#(ackin(s(X),Y),X) u21#(ackout(X),Y) -> ackin#(Y,X) TRS: ackin(s(X),s(Y)) -> u21(ackin(s(X),Y),X) u21(ackout(X),Y) -> u22(ackin(Y,X)) graph: u21#(ackout(X),Y) -> ackin#(Y,X) -> ackin#(s(X),s(Y)) -> ackin#(s(X),Y) u21#(ackout(X),Y) -> ackin#(Y,X) -> ackin#(s(X),s(Y)) -> u21#(ackin(s(X),Y),X) ackin#(s(X),s(Y)) -> ackin#(s(X),Y) -> ackin#(s(X),s(Y)) -> ackin#(s(X),Y) ackin#(s(X),s(Y)) -> ackin#(s(X),Y) -> ackin#(s(X),s(Y)) -> u21#(ackin(s(X),Y),X) SCC Processor: #sccs: 1 #rules: 1 #arcs: 4/9 DPs: ackin#(s(X),s(Y)) -> ackin#(s(X),Y) TRS: ackin(s(X),s(Y)) -> u21(ackin(s(X),Y),X) u21(ackout(X),Y) -> u22(ackin(Y,X)) Open