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