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