TRS: {f(x, x) -> f(g(x), x), g(x) -> s(x)} POP* + Boolean Semantic Labelling: Normal positions: pi(g_sl=0) = [1], pi(f_sl=1) = [1,2] Safe positions: pi(s_sl=1) = [1], pi(s_sl=0) = [1], pi(g_sl=1) = [1], pi(f_sl=0) = [1,2] Precedence: g_sl=1 > s_sl=1, g_sl=0 > s_sl=1, f_sl=1 > g_sl=1, f_sl=1 > g_sl=0, f_sl=1 > f_sl=0 empty Interpretation: f^(2): 00 | 1 01 | 0 10 | 1 11 | 0 g^(1): 0 | 1 1 | 0 s^(1): 0 | 1 1 | 0 Labelling: f^(2): 00 | 1 01 | 0 10 | 0 11 | 1 g^(1): 0 | 1 1 | 0 s^(1): 0 | 1 1 | 1 Labelled predicative System: {f_sl=1(x,x;) -> f_sl=0(;g_sl=1(;x),x), f_sl=1(x,x;) -> f_sl=0(;g_sl=0(x;),x), g_sl=1(;x) -> s_sl=1(;x), g_sl=0(x;) -> s_sl=1(;x)} Qed