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