TRS: {f(s(x), y, y) -> f(y, x, s(x))} POP* + Boolean Semantic Labelling: Normal positions: pi(f_sl=1) = [1,2,3], pi(f_sl=0) = [2,3] Safe positions: pi(s_sl=1) = [1], pi(s_sl=0) = [1], pi(f_sl=0) = [1] Precedence: f_sl=1 > f_sl=0 empty Interpretation: f^(3): 000 | 0 001 | 0 010 | 0 011 | 0 100 | 0 101 | 0 110 | 0 111 | 0 s^(1): 0 | 1 1 | 0 Labelling: f^(3): 000 | 1 001 | 0 010 | 0 011 | 1 100 | 1 101 | 0 110 | 0 111 | 1 s^(1): 0 | 0 1 | 0 Labelled predicative System: {f_sl=1(s_sl=0(;x),y,y;) -> f_sl=0(x,s_sl=0(;x);y), f_sl=1(s_sl=0(;x),y,y;) -> f_sl=0(x,s_sl=0(;x);y), f_sl=1(s_sl=0(;x),y,y;) -> f_sl=0(x,s_sl=0(;x);y), f_sl=1(s_sl=0(;x),y,y;) -> f_sl=0(x,s_sl=0(;x);y)} Qed