YES Proof: This system is quasi-decreasing. By \cite{A14}, Theorem 11.5.9. This system is of type 3 or smaller. This system is deterministic. System R transformed to V(R) + Emb. Call external tool: ttt2 - trs 30 Input: add(x, 0) -> x add(x, s(y)) -> s(add(x, y)) add(x, s(y)) -> add(x, y) s(x) -> x add(x, y) -> x add(x, y) -> y DP Processor: DPs: add#(x,s(y)) -> add#(x,y) add#(x,s(y)) -> s#(add(x,y)) TRS: add(x,0()) -> x add(x,s(y)) -> s(add(x,y)) add(x,s(y)) -> add(x,y) s(x) -> x add(x,y) -> x add(x,y) -> y TDG Processor: DPs: add#(x,s(y)) -> add#(x,y) add#(x,s(y)) -> s#(add(x,y)) TRS: add(x,0()) -> x add(x,s(y)) -> s(add(x,y)) add(x,s(y)) -> add(x,y) s(x) -> x add(x,y) -> x add(x,y) -> y graph: add#(x,s(y)) -> add#(x,y) -> add#(x,s(y)) -> s#(add(x,y)) add#(x,s(y)) -> add#(x,y) -> add#(x,s(y)) -> add#(x,y) SCC Processor: #sccs: 1 #rules: 1 #arcs: 2/4 DPs: add#(x,s(y)) -> add#(x,y) TRS: add(x,0()) -> x add(x,s(y)) -> s(add(x,y)) add(x,s(y)) -> add(x,y) s(x) -> x add(x,y) -> x add(x,y) -> y Subterm Criterion Processor: simple projection: pi(add#) = 1 problem: DPs: TRS: add(x,0()) -> x add(x,s(y)) -> s(add(x,y)) add(x,s(y)) -> add(x,y) s(x) -> x add(x,y) -> x add(x,y) -> y Qed