0.00/0.57 YES 0.00/0.57 0.00/0.57 Problem: 0.00/0.57 even(0()) -> true() 0.00/0.57 even(s(x)) -> false() <= odd(x) = false() 0.00/0.57 even(s(x)) -> true() <= odd(x) = true() 0.00/0.57 odd(0()) -> false() 0.00/0.57 odd(s(x)) -> false() <= even(x) = false() 0.00/0.57 odd(s(x)) -> true() <= even(x) = true() 0.00/0.57 0.00/0.57 Proof: 0.00/0.57 This system is confluent. 0.00/0.57 By \cite{GNG13}, Theorem 9. 0.00/0.57 This system is of type 3 or smaller. 0.00/0.57 This system is deterministic. 0.00/0.57 This system is weakly left-linear. 0.00/0.57 System R transformed to optimized U(R). 0.00/0.57 This system is orthogonal. 0.00/0.57 0.00/0.87 EOF