YES Problem: U11(tt(),M,N) -> U12(tt(),activate(M),activate(N)) U12(tt(),M,N) -> s(plus(activate(N),activate(M))) U21(tt(),M,N) -> U22(tt(),activate(M),activate(N)) U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N)) plus(N,0()) -> N plus(N,s(M)) -> U11(tt(),M,N) x(N,0()) -> 0() x(N,s(M)) -> U21(tt(),M,N) activate(X) -> X Proof: DP Processor: DPs: U11#(tt(),M,N) -> activate#(N) U11#(tt(),M,N) -> activate#(M) U11#(tt(),M,N) -> U12#(tt(),activate(M),activate(N)) U12#(tt(),M,N) -> activate#(M) U12#(tt(),M,N) -> activate#(N) U12#(tt(),M,N) -> plus#(activate(N),activate(M)) U21#(tt(),M,N) -> activate#(N) U21#(tt(),M,N) -> activate#(M) U21#(tt(),M,N) -> U22#(tt(),activate(M),activate(N)) U22#(tt(),M,N) -> activate#(M) U22#(tt(),M,N) -> activate#(N) U22#(tt(),M,N) -> x#(activate(N),activate(M)) U22#(tt(),M,N) -> plus#(x(activate(N),activate(M)),activate(N)) plus#(N,s(M)) -> U11#(tt(),M,N) x#(N,s(M)) -> U21#(tt(),M,N) TRS: U11(tt(),M,N) -> U12(tt(),activate(M),activate(N)) U12(tt(),M,N) -> s(plus(activate(N),activate(M))) U21(tt(),M,N) -> U22(tt(),activate(M),activate(N)) U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N)) plus(N,0()) -> N plus(N,s(M)) -> U11(tt(),M,N) x(N,0()) -> 0() x(N,s(M)) -> U21(tt(),M,N) activate(X) -> X TDG Processor: DPs: U11#(tt(),M,N) -> activate#(N) U11#(tt(),M,N) -> activate#(M) U11#(tt(),M,N) -> U12#(tt(),activate(M),activate(N)) U12#(tt(),M,N) -> activate#(M) U12#(tt(),M,N) -> activate#(N) U12#(tt(),M,N) -> plus#(activate(N),activate(M)) U21#(tt(),M,N) -> activate#(N) U21#(tt(),M,N) -> activate#(M) U21#(tt(),M,N) -> U22#(tt(),activate(M),activate(N)) U22#(tt(),M,N) -> activate#(M) U22#(tt(),M,N) -> activate#(N) U22#(tt(),M,N) -> x#(activate(N),activate(M)) U22#(tt(),M,N) -> plus#(x(activate(N),activate(M)),activate(N)) plus#(N,s(M)) -> U11#(tt(),M,N) x#(N,s(M)) -> U21#(tt(),M,N) TRS: U11(tt(),M,N) -> U12(tt(),activate(M),activate(N)) U12(tt(),M,N) -> s(plus(activate(N),activate(M))) U21(tt(),M,N) -> U22(tt(),activate(M),activate(N)) U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N)) plus(N,0()) -> N plus(N,s(M)) -> U11(tt(),M,N) x(N,0()) -> 0() x(N,s(M)) -> U21(tt(),M,N) activate(X) -> X graph: x#(N,s(M)) -> U21#(tt(),M,N) -> U21#(tt(),M,N) -> U22#(tt(),activate(M),activate(N)) x#(N,s(M)) -> U21#(tt(),M,N) -> U21#(tt(),M,N) -> activate#(M) x#(N,s(M)) -> U21#(tt(),M,N) -> U21#(tt(),M,N) -> activate#(N) U22#(tt(),M,N) -> x#(activate(N),activate(M)) -> x#(N,s(M)) -> U21#(tt(),M,N) U22#(tt(),M,N) -> plus#(x(activate(N),activate(M)),activate(N)) -> plus#(N,s(M)) -> U11#(tt(),M,N) U21#(tt(),M,N) -> U22#(tt(),activate(M),activate(N)) -> U22#(tt(),M,N) -> plus#(x(activate(N),activate(M)),activate(N)) U21#(tt(),M,N) -> U22#(tt(),activate(M),activate(N)) -> U22#(tt(),M,N) -> x#(activate(N),activate(M)) U21#(tt(),M,N) -> U22#(tt(),activate(M),activate(N)) -> U22#(tt(),M,N) -> activate#(N) U21#(tt(),M,N) -> U22#(tt(),activate(M),activate(N)) -> U22#(tt(),M,N) -> activate#(M) plus#(N,s(M)) -> U11#(tt(),M,N) -> U11#(tt(),M,N) -> U12#(tt(),activate(M),activate(N)) plus#(N,s(M)) -> U11#(tt(),M,N) -> U11#(tt(),M,N) -> activate#(M) plus#(N,s(M)) -> U11#(tt(),M,N) -> U11#(tt(),M,N) -> activate#(N) U12#(tt(),M,N) -> plus#(activate(N),activate(M)) -> plus#(N,s(M)) -> U11#(tt(),M,N) U11#(tt(),M,N) -> U12#(tt(),activate(M),activate(N)) -> U12#(tt(),M,N) -> plus#(activate(N),activate(M)) U11#(tt(),M,N) -> U12#(tt(),activate(M),activate(N)) -> U12#(tt(),M,N) -> activate#(N) U11#(tt(),M,N) -> U12#(tt(),activate(M),activate(N)) -> U12#(tt(),M,N) -> activate#(M) SCC Processor: #sccs: 2 #rules: 6 #arcs: 16/225 DPs: x#(N,s(M)) -> U21#(tt(),M,N) U21#(tt(),M,N) -> U22#(tt(),activate(M),activate(N)) U22#(tt(),M,N) -> x#(activate(N),activate(M)) TRS: U11(tt(),M,N) -> U12(tt(),activate(M),activate(N)) U12(tt(),M,N) -> s(plus(activate(N),activate(M))) U21(tt(),M,N) -> U22(tt(),activate(M),activate(N)) U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N)) plus(N,0()) -> N plus(N,s(M)) -> U11(tt(),M,N) x(N,0()) -> 0() x(N,s(M)) -> U21(tt(),M,N) activate(X) -> X Usable Rule Processor: DPs: x#(N,s(M)) -> U21#(tt(),M,N) U21#(tt(),M,N) -> U22#(tt(),activate(M),activate(N)) U22#(tt(),M,N) -> x#(activate(N),activate(M)) TRS: activate(X) -> X Semantic Labeling Processor: dimension: 2 usable rules: activate(X) -> X interpretation: [0] [s](x0) = [0], [0 1] [1] [activate](x0) = [0 0]x0 + [1], [0] [tt] = [1] labeled: usable (for model): argument filtering: pi(tt) = [] pi(activate) = [0] pi(s) = [0] pi(U21#) = [1] pi(U22#) = [1] pi(x#) = 1 precedence: s > U21# > U22# > x# ~ activate ~ tt problem: DPs: TRS: activate(X) -> X Qed DPs: plus#(N,s(M)) -> U11#(tt(),M,N) U11#(tt(),M,N) -> U12#(tt(),activate(M),activate(N)) U12#(tt(),M,N) -> plus#(activate(N),activate(M)) TRS: U11(tt(),M,N) -> U12(tt(),activate(M),activate(N)) U12(tt(),M,N) -> s(plus(activate(N),activate(M))) U21(tt(),M,N) -> U22(tt(),activate(M),activate(N)) U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N)) plus(N,0()) -> N plus(N,s(M)) -> U11(tt(),M,N) x(N,0()) -> 0() x(N,s(M)) -> U21(tt(),M,N) activate(X) -> X Usable Rule Processor: DPs: plus#(N,s(M)) -> U11#(tt(),M,N) U11#(tt(),M,N) -> U12#(tt(),activate(M),activate(N)) U12#(tt(),M,N) -> plus#(activate(N),activate(M)) TRS: activate(X) -> X Semantic Labeling Processor: dimension: 2 usable rules: activate(X) -> X interpretation: [0] [s](x0) = [0], [0 1] [1] [activate](x0) = [0 0]x0 + [1], [0] [tt] = [1] labeled: usable (for model): argument filtering: pi(tt) = [] pi(activate) = [0] pi(s) = [0] pi(U11#) = [1] pi(U12#) = [1] pi(plus#) = 1 precedence: s > U11# > U12# > plus# ~ activate ~ tt problem: DPs: TRS: activate(X) -> X Qed