YES 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 TDG 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)) -> plus#(x(N,M),N) x#(N,s(M)) -> x#(N,M) -> x#(N,s(M)) -> x#(N,M) 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 LPO Processor: argument filtering: pi(tt) = [] pi(and) = [1] pi(activate) = 0 pi(0) = [] pi(plus) = [0,1] pi(s) = [0] pi(x) = [0,1] pi(x#) = 1 precedence: x > plus > x# ~ s ~ 0 ~ activate ~ and ~ tt problem: DPs: 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 Qed 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 LPO Processor: argument filtering: pi(tt) = [] pi(and) = [1] pi(activate) = 0 pi(0) = [] pi(plus) = [0,1] pi(s) = [0] pi(x) = [0,1] pi(plus#) = 1 precedence: x > plus > plus# ~ s ~ 0 ~ activate ~ and ~ tt problem: DPs: 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 Qed