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