YES Problem: prime(0()) -> false() prime(s(0())) -> false() prime(s(s(x))) -> prime1(s(s(x)),s(x)) prime1(x,0()) -> false() prime1(x,s(0())) -> true() prime1(x,s(s(y))) -> and(not(divp(s(s(y)),x)),prime1(x,s(y))) divp(x,y) -> =(rem(x,y),0()) Proof: DP Processor: DPs: prime#(s(s(x))) -> prime1#(s(s(x)),s(x)) prime1#(x,s(s(y))) -> prime1#(x,s(y)) prime1#(x,s(s(y))) -> divp#(s(s(y)),x) TRS: prime(0()) -> false() prime(s(0())) -> false() prime(s(s(x))) -> prime1(s(s(x)),s(x)) prime1(x,0()) -> false() prime1(x,s(0())) -> true() prime1(x,s(s(y))) -> and(not(divp(s(s(y)),x)),prime1(x,s(y))) divp(x,y) -> =(rem(x,y),0()) TDG Processor: DPs: prime#(s(s(x))) -> prime1#(s(s(x)),s(x)) prime1#(x,s(s(y))) -> prime1#(x,s(y)) prime1#(x,s(s(y))) -> divp#(s(s(y)),x) TRS: prime(0()) -> false() prime(s(0())) -> false() prime(s(s(x))) -> prime1(s(s(x)),s(x)) prime1(x,0()) -> false() prime1(x,s(0())) -> true() prime1(x,s(s(y))) -> and(not(divp(s(s(y)),x)),prime1(x,s(y))) divp(x,y) -> =(rem(x,y),0()) graph: prime1#(x,s(s(y))) -> prime1#(x,s(y)) -> prime1#(x,s(s(y))) -> divp#(s(s(y)),x) prime1#(x,s(s(y))) -> prime1#(x,s(y)) -> prime1#(x,s(s(y))) -> prime1#(x,s(y)) prime#(s(s(x))) -> prime1#(s(s(x)),s(x)) -> prime1#(x,s(s(y))) -> divp#(s(s(y)),x) prime#(s(s(x))) -> prime1#(s(s(x)),s(x)) -> prime1#(x,s(s(y))) -> prime1#(x,s(y)) SCC Processor: #sccs: 1 #rules: 1 #arcs: 4/9 DPs: prime1#(x,s(s(y))) -> prime1#(x,s(y)) TRS: prime(0()) -> false() prime(s(0())) -> false() prime(s(s(x))) -> prime1(s(s(x)),s(x)) prime1(x,0()) -> false() prime1(x,s(0())) -> true() prime1(x,s(s(y))) -> and(not(divp(s(s(y)),x)),prime1(x,s(y))) divp(x,y) -> =(rem(x,y),0()) KBO Processor: argument filtering: pi(0) = [] pi(prime) = [0] pi(false) = [] pi(s) = [0] pi(prime1) = [] pi(true) = [] pi(divp) = 1 pi(not) = [] pi(and) = 1 pi(rem) = 1 pi(=) = 0 pi(prime1#) = [0,1] weight function: w0 = 1 w(prime1#) = w(=) = w(rem) = w(and) = w(not) = w(true) = w(prime1) = w( false) = w(prime) = w(0) = 1 w(divp) = w(s) = 0 precedence: prime1# ~ and ~ not ~ prime1 ~ s ~ prime ~ 0 > = ~ rem ~ divp ~ true ~ false problem: DPs: TRS: prime(0()) -> false() prime(s(0())) -> false() prime(s(s(x))) -> prime1(s(s(x)),s(x)) prime1(x,0()) -> false() prime1(x,s(0())) -> true() prime1(x,s(s(y))) -> and(not(divp(s(s(y)),x)),prime1(x,s(y))) divp(x,y) -> =(rem(x,y),0()) Qed