TRS: {c() -> f(), f() -> g()} POP* + Boolean Semantic Labelling: Normal positions: Safe positions: Precedence: c_sl=0 > f_sl=0, f_sl=0 > g_sl=0 empty Interpretation: f^(0): | 0 c^(0): | 0 g^(0): | 0 Labelling: f^(0): | 0 c^(0): | 0 g^(0): | 0 Labelled predicative System: {c_sl=0() -> f_sl=0(), f_sl=0() -> g_sl=0()} Qed