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())} POP* + Boolean Semantic Labelling: Normal positions: pi(divp_sl=1) = [1,2], pi(divp_sl=0) = [1,2], pi(prime1_sl=1) = [1,2], pi(prime1_sl=0) = [1,2], pi(prime_sl=1) = [1], pi(prime_sl=0) = [1] Safe positions: pi(rem_sl=1) = [1,2], pi(rem_sl=0) = [1,2], pi(=_sl=1) = [1,2], pi(=_sl=0) = [1,2], pi(not_sl=1) = [1], pi(not_sl=0) = [1], pi(and_sl=1) = [1,2], pi(and_sl=0) = [1,2], pi(s_sl=1) = [1], pi(s_sl=0) = [1] Precedence: prime_sl=0 > prime1_sl=0, prime_sl=0 > false_sl=0, prime1_sl=0 > divp_sl=0, prime1_sl=0 > not_sl=0, prime1_sl=0 > and_sl=0, prime1_sl=0 > true_sl=0, prime1_sl=0 > false_sl=0, divp_sl=0 > rem_sl=0, divp_sl=0 > =_sl=0, divp_sl=0 > 0_sl=1 empty Interpretation: false^(0): | 0 prime^(1): 0 | 0 1 | 0 0^(0): | 0 s^(1): 0 | 0 1 | 0 prime1^(2): 00 | 0 01 | 0 10 | 0 11 | 0 true^(0): | 0 and^(2): 00 | 0 01 | 0 10 | 0 11 | 0 not^(1): 0 | 0 1 | 0 divp^(2): 00 | 0 01 | 0 10 | 0 11 | 0 =^(2): 00 | 0 01 | 0 10 | 0 11 | 0 rem^(2): 00 | 0 01 | 1 10 | 1 11 | 1 Labelling: false^(0): | 0 prime^(1): 0 | 0 1 | 0 0^(0): | 1 s^(1): 0 | 0 1 | 0 prime1^(2): 00 | 0 01 | 0 10 | 0 11 | 0 true^(0): | 0 and^(2): 00 | 0 01 | 0 10 | 0 11 | 0 not^(1): 0 | 0 1 | 0 divp^(2): 00 | 0 01 | 0 10 | 0 11 | 0 =^(2): 00 | 0 01 | 0 10 | 0 11 | 0 rem^(2): 00 | 0 01 | 0 10 | 0 11 | 0 Labelled predicative System: { prime_sl=0(0_sl=1();) -> false_sl=0(), prime_sl=0(s_sl=0(;0_sl=1());) -> false_sl=0(), prime_sl=0(s_sl=0(;s_sl=0(;x));) -> prime1_sl=0(s_sl=0(;s_sl=0(;x)),s_sl=0(;x);), prime_sl=0(s_sl=0(;s_sl=0(;x));) -> prime1_sl=0(s_sl=0(;s_sl=0(;x)),s_sl=0(;x);), prime1_sl=0(x,0_sl=1();) -> false_sl=0(), prime1_sl=0(x,0_sl=1();) -> false_sl=0(), prime1_sl=0(x,s_sl=0(;0_sl=1());) -> true_sl=0(), prime1_sl=0(x,s_sl=0(;0_sl=1());) -> true_sl=0(), prime1_sl=0(x,s_sl=0(;s_sl=0(;y));) -> and_sl=0(;not_sl=0(;divp_sl=0(s_sl=0(;s_sl=0(;y)),x;)),prime1_sl=0(x,s_sl=0(;y);)), prime1_sl=0(x,s_sl=0(;s_sl=0(;y));) -> and_sl=0(;not_sl=0(;divp_sl=0(s_sl=0(;s_sl=0(;y)),x;)),prime1_sl=0(x,s_sl=0(;y);)), prime1_sl=0(x,s_sl=0(;s_sl=0(;y));) -> and_sl=0(;not_sl=0(;divp_sl=0(s_sl=0(;s_sl=0(;y)),x;)),prime1_sl=0(x,s_sl=0(;y);)), prime1_sl=0(x,s_sl=0(;s_sl=0(;y));) -> and_sl=0(;not_sl=0(;divp_sl=0(s_sl=0(;s_sl=0(;y)),x;)),prime1_sl=0(x,s_sl=0(;y);)), divp_sl=0(x,y;) -> =_sl=0(;rem_sl=0(;x,y),0_sl=1()), divp_sl=0(x,y;) -> =_sl=0(;rem_sl=0(;x,y),0_sl=1()), divp_sl=0(x,y;) -> =_sl=0(;rem_sl=0(;x,y),0_sl=1()), divp_sl=0(x,y;) -> =_sl=0(;rem_sl=0(;x,y),0_sl=1())} Qed