YES Proof: This system is confluent. By \cite{ALS94}, Theorem 4.1. This system is of type 3 or smaller. This system is strongly deterministic. All 4 critical pairs are joinable. false = true <= odd(x) = true, odd(x) = false: This critical pair is unfeasible. true = false <= odd(x) = false, odd(x) = true: This critical pair is unfeasible. false = true <= even(x) = true, even(x) = false: This critical pair is unfeasible. true = false <= even(x) = false, even(x) = true: This critical pair is unfeasible. 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)) -> false even(s(x)) -> odd(x) even(s(x)) -> true odd(0) -> false odd(s(x)) -> false odd(s(x)) -> even(x) odd(s(x)) -> true 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)) -> false() even(s(x)) -> odd(x) even(s(x)) -> true() odd(0()) -> false() odd(s(x)) -> false() odd(s(x)) -> even(x) odd(s(x)) -> true() 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)) -> false() even(s(x)) -> odd(x) even(s(x)) -> true() odd(0()) -> false() odd(s(x)) -> false() odd(s(x)) -> even(x) odd(s(x)) -> true() 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)) -> false() even(s(x)) -> odd(x) even(s(x)) -> true() odd(0()) -> false() odd(s(x)) -> false() odd(s(x)) -> even(x) odd(s(x)) -> true() even(x) -> x s(x) -> x odd(x) -> x Qed