YES Problem: and(tt(),X) -> activate(X) plus(N,0()) -> N plus(N,s(M)) -> s(plus(N,M)) activate(X) -> X Proof: DP Processor: DPs: and#(tt(),X) -> activate#(X) 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)) activate(X) -> X TDG Processor: DPs: and#(tt(),X) -> activate#(X) 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)) activate(X) -> X graph: plus#(N,s(M)) -> plus#(N,M) -> plus#(N,s(M)) -> plus#(N,M) SCC Processor: #sccs: 1 #rules: 1 #arcs: 1/4 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)) activate(X) -> X Subterm Criterion Processor: simple projection: pi(plus#) = 1 problem: DPs: TRS: and(tt(),X) -> activate(X) plus(N,0()) -> N plus(N,s(M)) -> s(plus(N,M)) activate(X) -> X Qed