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()) EDG 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#(x,0()) -> evenodd#(x,s(0())) evenodd#(s(x),s(0())) -> evenodd#(x,0()) -> evenodd#(x,0()) -> not#(evenodd(x,s(0()))) evenodd#(x,0()) -> evenodd#(x,s(0())) -> evenodd#(s(x),s(0())) -> evenodd#(x,0()) SCC Processor: #sccs: 1 #rules: 2 #arcs: 3/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()) Matrix Interpretation Processor: dimension: 1 interpretation: [evenodd#](x0, x1) = x1, [s](x0) = 0, [evenodd](x0, x1) = 1, [0] = 1, [false] = 1, [not](x0) = x0, [true] = 1 orientation: evenodd#(x,0()) = 1 >= 0 = evenodd#(x,s(0())) not(true()) = 1 >= 1 = false() not(false()) = 1 >= 1 = true() evenodd(x,0()) = 1 >= 1 = not(evenodd(x,s(0()))) evenodd(0(),s(0())) = 1 >= 1 = false() evenodd(s(x),s(0())) = 1 >= 1 = evenodd(x,0()) problem: DPs: 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()) Qed