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