YES Problem: perfectp(0()) -> false() perfectp(s(x)) -> f(x,s(0()),s(x),s(x)) f(0(),y,0(),u) -> true() f(0(),y,s(z),u) -> false() f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u) f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) Proof: DP Processor: DPs: perfectp#(s(x)) -> f#(x,s(0()),s(x),s(x)) f#(s(x),0(),z,u) -> f#(x,u,minus(z,s(x)),u) f#(s(x),s(y),z,u) -> f#(x,u,z,u) f#(s(x),s(y),z,u) -> f#(s(x),minus(y,x),z,u) TRS: perfectp(0()) -> false() perfectp(s(x)) -> f(x,s(0()),s(x),s(x)) f(0(),y,0(),u) -> true() f(0(),y,s(z),u) -> false() f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u) f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) Usable Rule Processor: DPs: perfectp#(s(x)) -> f#(x,s(0()),s(x),s(x)) f#(s(x),0(),z,u) -> f#(x,u,minus(z,s(x)),u) f#(s(x),s(y),z,u) -> f#(x,u,z,u) f#(s(x),s(y),z,u) -> f#(s(x),minus(y,x),z,u) TRS: LPO Processor: argument filtering: pi(0) = [] pi(s) = [0] pi(minus) = [] pi(perfectp#) = [0] pi(f#) = [0,1,3] usable rules: precedence: perfectp# > s > f# ~ minus ~ 0 problem: DPs: TRS: Qed