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