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