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