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: even(0) -> true even(s(x)) -> true even(s(x)) -> odd(x) odd(s(x)) -> true odd(s(x)) -> even(x) even(x) -> x s(x) -> x odd(x) -> x DP Processor: DPs: even#(s(x)) -> odd#(x) odd#(s(x)) -> even#(x) TRS: even(0()) -> true() even(s(x)) -> true() even(s(x)) -> odd(x) odd(s(x)) -> true() odd(s(x)) -> even(x) even(x) -> x s(x) -> x odd(x) -> x TDG Processor: DPs: even#(s(x)) -> odd#(x) odd#(s(x)) -> even#(x) TRS: even(0()) -> true() even(s(x)) -> true() even(s(x)) -> odd(x) odd(s(x)) -> true() odd(s(x)) -> even(x) even(x) -> x s(x) -> x odd(x) -> x graph: odd#(s(x)) -> even#(x) -> even#(s(x)) -> odd#(x) even#(s(x)) -> odd#(x) -> odd#(s(x)) -> even#(x) Subterm Criterion Processor: simple projection: pi(even#) = 0 pi(odd#) = 0 problem: DPs: TRS: even(0()) -> true() even(s(x)) -> true() even(s(x)) -> odd(x) odd(s(x)) -> true() odd(s(x)) -> even(x) even(x) -> x s(x) -> x odd(x) -> x Qed