TRS: { first(0(), X) -> nil(), first(s(X), cons(Y)) -> cons(Y), from(X) -> cons(X)} POP* + Boolean Semantic Labelling: Normal positions: pi(from_sl=1) = [1], pi(from_sl=0) = [1], pi(first_sl=1) = [1,2], pi(first_sl=0) = [1,2] Safe positions: pi(s_sl=1) = [1], pi(s_sl=0) = [1], pi(cons_sl=1) = [1], pi(cons_sl=0) = [1] Precedence: first_sl=0 > nil_sl=0, from_sl=0 > cons_sl=0 empty Interpretation: nil^(0): | 0 first^(2): 00 | 0 01 | 0 10 | 0 11 | 0 0^(0): | 0 cons^(1): 0 | 0 1 | 0 s^(1): 0 | 0 1 | 0 from^(1): 0 | 0 1 | 0 Labelling: nil^(0): | 0 first^(2): 00 | 0 01 | 0 10 | 0 11 | 0 0^(0): | 0 cons^(1): 0 | 0 1 | 0 s^(1): 0 | 0 1 | 0 from^(1): 0 | 0 1 | 0 Labelled predicative System: { first_sl=0(0_sl=0(),X;) -> nil_sl=0(), first_sl=0(0_sl=0(),X;) -> nil_sl=0(), first_sl=0(s_sl=0(;X),cons_sl=0(;Y);) -> cons_sl=0(;Y), first_sl=0(s_sl=0(;X),cons_sl=0(;Y);) -> cons_sl=0(;Y), first_sl=0(s_sl=0(;X),cons_sl=0(;Y);) -> cons_sl=0(;Y), first_sl=0(s_sl=0(;X),cons_sl=0(;Y);) -> cons_sl=0(;Y), from_sl=0(X;) -> cons_sl=0(;X), from_sl=0(X;) -> cons_sl=0(;X)} Qed