TRS:
 {ackin(s(X), s(Y)) -> u21(ackin(s(X), Y), X),
  u21(ackout(X), Y) -> u22(ackin(Y, X))}
 POP* + Boolean Semantic Labelling:
  Normal positions:
  pi(ackin_sl=1) = [1,2], pi(ackin_sl=0) = [1,2], pi(u21_sl=1) = [1,2], pi(u21_sl=0) = [2]
  
Safe positions:
   pi(ackout_sl=1) = [1], pi(ackout_sl=0) = [1], pi(u22_sl=1) = [1], pi(u22_sl=0) = [1], pi(s_sl=1) = [1], pi(s_sl=0) = [1], pi(u21_sl=0) = [1]
  
Precedence:
   u21_sl=1 > ackin_sl=0, 
   u21_sl=1 > ackin_sl=1, 
   u21_sl=1 > u22_sl=0, 
   ackin_sl=0 > ackin_sl=1, 
   ackin_sl=0 > u21_sl=0
   empty
  
Interpretation:
   u21^(2):
   00 | 0
   01 | 0
   10 | 1
   11 | 1
   ackin^(2):
   00 | 1
   01 | 1
   10 | 0
   11 | 0
   s^(1):
   0 | 0
   1 | 0
   u22^(1):
   0 | 0
   1 | 0
   ackout^(1):
   0 | 0
   1 | 0
   
  
Labelling:
   u21^(2):
   00 | 1
   01 | 1
   10 | 0
   11 | 0
   ackin^(2):
   00 | 0
   01 | 1
   10 | 0
   11 | 0
   s^(1):
   0 | 0
   1 | 0
   u22^(1):
   0 | 0
   1 | 0
   ackout^(1):
   0 | 0
   1 | 0
   
  
Labelled predicative System:
   {ackin_sl=0(s_sl=0(;X),s_sl=0(;Y);) -> u21_sl=0(X;ackin_sl=0(s_sl=0(;X),Y;)),
    ackin_sl=0(s_sl=0(;X),s_sl=0(;Y);) -> u21_sl=0(X;ackin_sl=1(s_sl=0(;X),Y;)),
    ackin_sl=0(s_sl=0(;X),s_sl=0(;Y);) -> u21_sl=0(X;ackin_sl=0(s_sl=0(;X),Y;)),
    ackin_sl=0(s_sl=0(;X),s_sl=0(;Y);) -> u21_sl=0(X;ackin_sl=1(s_sl=0(;X),Y;)),
          u21_sl=1(ackout_sl=0(;X),Y;) -> u22_sl=0(;ackin_sl=0(Y,X;)),
          u21_sl=1(ackout_sl=0(;X),Y;) -> u22_sl=0(;ackin_sl=0(Y,X;)),
          u21_sl=1(ackout_sl=0(;X),Y;) -> u22_sl=0(;ackin_sl=1(Y,X;)),
          u21_sl=1(ackout_sl=0(;X),Y;) -> u22_sl=0(;ackin_sl=0(Y,X;))}
  

  Qed