YES Problem: not(true()) -> false() not(false()) -> true() evenodd(x,0()) -> not(evenodd(x,s(0()))) evenodd(0(),s(0())) -> false() evenodd(s(x),s(0())) -> evenodd(x,0()) Proof: DP Processor: DPs: evenodd#(x,0()) -> evenodd#(x,s(0())) evenodd#(x,0()) -> not#(evenodd(x,s(0()))) evenodd#(s(x),s(0())) -> evenodd#(x,0()) TRS: not(true()) -> false() not(false()) -> true() evenodd(x,0()) -> not(evenodd(x,s(0()))) evenodd(0(),s(0())) -> false() evenodd(s(x),s(0())) -> evenodd(x,0()) TDG Processor: DPs: evenodd#(x,0()) -> evenodd#(x,s(0())) evenodd#(x,0()) -> not#(evenodd(x,s(0()))) evenodd#(s(x),s(0())) -> evenodd#(x,0()) TRS: not(true()) -> false() not(false()) -> true() evenodd(x,0()) -> not(evenodd(x,s(0()))) evenodd(0(),s(0())) -> false() evenodd(s(x),s(0())) -> evenodd(x,0()) graph: evenodd#(s(x),s(0())) -> evenodd#(x,0()) -> evenodd#(s(x),s(0())) -> evenodd#(x,0()) evenodd#(s(x),s(0())) -> evenodd#(x,0()) -> evenodd#(x,0()) -> not#(evenodd(x,s(0()))) evenodd#(s(x),s(0())) -> evenodd#(x,0()) -> evenodd#(x,0()) -> evenodd#(x,s(0())) evenodd#(x,0()) -> evenodd#(x,s(0())) -> evenodd#(s(x),s(0())) -> evenodd#(x,0()) evenodd#(x,0()) -> evenodd#(x,s(0())) -> evenodd#(x,0()) -> not#(evenodd(x,s(0()))) evenodd#(x,0()) -> evenodd#(x,s(0())) -> evenodd#(x,0()) -> evenodd#(x,s(0())) SCC Processor: #sccs: 1 #rules: 2 #arcs: 6/9 DPs: evenodd#(s(x),s(0())) -> evenodd#(x,0()) evenodd#(x,0()) -> evenodd#(x,s(0())) TRS: not(true()) -> false() not(false()) -> true() evenodd(x,0()) -> not(evenodd(x,s(0()))) evenodd(0(),s(0())) -> false() evenodd(s(x),s(0())) -> evenodd(x,0()) Subterm Criterion Processor: simple projection: pi(evenodd#) = 0 problem: DPs: evenodd#(x,0()) -> evenodd#(x,s(0())) TRS: not(true()) -> false() not(false()) -> true() evenodd(x,0()) -> not(evenodd(x,s(0()))) evenodd(0(),s(0())) -> false() evenodd(s(x),s(0())) -> evenodd(x,0()) EDG Processor: DPs: evenodd#(x,0()) -> evenodd#(x,s(0())) TRS: not(true()) -> false() not(false()) -> true() evenodd(x,0()) -> not(evenodd(x,s(0()))) evenodd(0(),s(0())) -> false() evenodd(s(x),s(0())) -> evenodd(x,0()) graph: Qed