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