MAYBE Problem: and(tt(),X) -> activate(X) plus(N,0()) -> N plus(N,s(M)) -> s(plus(N,M)) x(N,0()) -> 0() x(N,s(M)) -> plus(x(N,M),N) activate(X) -> X Proof: DP Processor: DPs: and#(tt(),X) -> activate#(X) plus#(N,s(M)) -> plus#(N,M) x#(N,s(M)) -> x#(N,M) x#(N,s(M)) -> plus#(x(N,M),N) TRS: and(tt(),X) -> activate(X) plus(N,0()) -> N plus(N,s(M)) -> s(plus(N,M)) x(N,0()) -> 0() x(N,s(M)) -> plus(x(N,M),N) activate(X) -> X ADG Processor: DPs: and#(tt(),X) -> activate#(X) plus#(N,s(M)) -> plus#(N,M) x#(N,s(M)) -> x#(N,M) x#(N,s(M)) -> plus#(x(N,M),N) TRS: and(tt(),X) -> activate(X) plus(N,0()) -> N plus(N,s(M)) -> s(plus(N,M)) x(N,0()) -> 0() x(N,s(M)) -> plus(x(N,M),N) activate(X) -> X graph: x#(N,s(M)) -> x#(N,M) -> x#(N,s(M)) -> x#(N,M) x#(N,s(M)) -> x#(N,M) -> x#(N,s(M)) -> plus#(x(N,M),N) x#(N,s(M)) -> plus#(x(N,M),N) -> plus#(N,s(M)) -> plus#(N,M) plus#(N,s(M)) -> plus#(N,M) -> plus#(N,s(M)) -> plus#(N,M) SCC Processor: #sccs: 2 #rules: 2 #arcs: 4/16 DPs: x#(N,s(M)) -> x#(N,M) TRS: and(tt(),X) -> activate(X) plus(N,0()) -> N plus(N,s(M)) -> s(plus(N,M)) x(N,0()) -> 0() x(N,s(M)) -> plus(x(N,M),N) activate(X) -> X Open DPs: plus#(N,s(M)) -> plus#(N,M) TRS: and(tt(),X) -> activate(X) plus(N,0()) -> N plus(N,s(M)) -> s(plus(N,M)) x(N,0()) -> 0() x(N,s(M)) -> plus(x(N,M),N) activate(X) -> X Open