TRS: {a__f(f(a())) -> c(f(g(f(a())))), mark(f(X)) -> a__f(mark(X)), mark(a()) -> a(), mark(c(X)) -> c(X), mark(g(X)) -> g(mark(X)), a__f(X) -> f(X)} POP* + Boolean Semantic Labelling: Normal positions: pi(mark_sl=1) = [1], pi(mark_sl=0) = [1], pi(a__f_sl=1) = [1] Safe positions: pi(a__f_sl=0) = [1], pi(g_sl=1) = [1], pi(g_sl=0) = [1], pi(f_sl=1) = [1], pi(f_sl=0) = [1], pi(c_sl=1) = [1], pi(c_sl=0) = [1] Precedence: mark_sl=0 > g_sl=0, mark_sl=0 > a__f_sl=0, mark_sl=0 > mark_sl=1, a__f_sl=0 > a_sl=0, a__f_sl=0 > g_sl=0, a__f_sl=0 > f_sl=0, a__f_sl=0 > c_sl=0 empty Interpretation: c^(1): 0 | 0 1 | 0 f^(1): 0 | 0 1 | 0 g^(1): 0 | 0 1 | 0 a^(0): | 0 a__f^(1): 0 | 0 1 | 0 mark^(1): 0 | 0 1 | 0 Labelling: c^(1): 0 | 0 1 | 0 f^(1): 0 | 0 1 | 0 g^(1): 0 | 0 1 | 0 a^(0): | 0 a__f^(1): 0 | 0 1 | 0 mark^(1): 0 | 0 1 | 1 Labelled predicative System: {a__f_sl=0(;f_sl=0(;a_sl=0())) -> c_sl=0(;f_sl=0(;g_sl=0(;f_sl=0(;a_sl=0())))), mark_sl=0(f_sl=0(;X);) -> a__f_sl=0(;mark_sl=0(X;)), mark_sl=0(f_sl=0(;X);) -> a__f_sl=0(;mark_sl=1(X;)), mark_sl=0(a_sl=0();) -> a_sl=0(), mark_sl=0(c_sl=0(;X);) -> c_sl=0(;X), mark_sl=0(c_sl=0(;X);) -> c_sl=0(;X), mark_sl=0(g_sl=0(;X);) -> g_sl=0(;mark_sl=0(X;)), mark_sl=0(g_sl=0(;X);) -> g_sl=0(;mark_sl=1(X;)), a__f_sl=0(;X) -> f_sl=0(;X), a__f_sl=0(;X) -> f_sl=0(;X)} Qed