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