TRS: { f(x, 0()) -> s(0()), f(s(x), s(y)) -> s(f(x, y)), g(0(), x) -> g(f(x, x), x)} POP* + Boolean Semantic Labelling: Normal positions: pi(g_sl=1) = [1,2], pi(g_sl=0) = [1], pi(f_sl=1) = [1,2], pi(f_sl=0) = [1,2] Safe positions: pi(g_sl=0) = [2], pi(s_sl=1) = [1], pi(s_sl=0) = [1] Precedence: f_sl=1 > s_sl=0, f_sl=1 > 0_sl=0, f_sl=1 > f_sl=0, g_sl=1 > f_sl=1, g_sl=1 > g_sl=0 empty Interpretation: s^(1): 0 | 0 1 | 0 0^(0): | 1 f^(2): 00 | 0 01 | 0 10 | 0 11 | 0 g^(2): 00 | 0 01 | 0 10 | 0 11 | 0 Labelling: s^(1): 0 | 0 1 | 0 0^(0): | 0 f^(2): 00 | 1 01 | 1 10 | 0 11 | 1 g^(2): 00 | 0 01 | 0 10 | 1 11 | 1 Labelled predicative System: { f_sl=1(x,0_sl=0();) -> s_sl=0(;0_sl=0()), f_sl=1(x,0_sl=0();) -> s_sl=0(;0_sl=0()), f_sl=1(s_sl=0(;x),s_sl=0(;y);) -> s_sl=0(;f_sl=1(x,y;)), f_sl=1(s_sl=0(;x),s_sl=0(;y);) -> s_sl=0(;f_sl=1(x,y;)), f_sl=1(s_sl=0(;x),s_sl=0(;y);) -> s_sl=0(;f_sl=0(x,y;)), f_sl=1(s_sl=0(;x),s_sl=0(;y);) -> s_sl=0(;f_sl=1(x,y;)), g_sl=1(0_sl=0(),x;) -> g_sl=0(f_sl=1(x,x;);x), g_sl=1(0_sl=0(),x;) -> g_sl=0(f_sl=1(x,x;);x)} Qed