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