TRS:
 {  f(x, y, w, w, a()) -> g1(x, x, y, w),
  f(x, y, w, a(), a()) -> g1(y, x, x, w),
  f(x, y, a(), a(), w) -> g2(x, y, y, w),
    f(x, y, a(), w, w) -> g2(y, y, x, w),
      g1(x, x, y, a()) -> h(x, y),
      g1(y, x, x, a()) -> h(x, y),
      g2(x, y, y, a()) -> h(x, y),
      g2(y, y, x, a()) -> h(x, y),
               h(x, x) -> x}
 POP* + Boolean Semantic Labelling:
  Normal positions:
  pi(h_sl=1) = [1,2], pi(h_sl=0) = [1,2], pi(g2_sl=1) = [1,2,3,4], pi(g2_sl=0) = [1,2,3,4], pi(f_sl=1) = [1,2,3,4,5], pi(f_sl=0) = [1,2,3,4,5], pi(g1_sl=1) = [1,2,3,4], pi(g1_sl=0) = [1,2,3,4]
  
Safe positions:
   
  
Precedence:
   g2_sl=0 > h_sl=0, 
   g1_sl=0 > h_sl=0, 
   f_sl=0 > g2_sl=0, 
   f_sl=0 > g1_sl=0
   empty
  
Interpretation:
   g1^(4):
   0000 | 0
   0001 | 0
   0010 | 0
   0011 | 0
   0100 | 0
   0101 | 0
   0110 | 0
   0111 | 0
   1000 | 0
   1001 | 0
   1010 | 0
   1011 | 0
   1100 | 0
   1101 | 0
   1110 | 1
   1111 | 0
   f^(5):
   00000 | 0
   00001 | 0
   00010 | 0
   00011 | 0
   00100 | 0
   00101 | 0
   00110 | 0
   00111 | 0
   01000 | 0
   01001 | 0
   01010 | 0
   01011 | 0
   01100 | 0
   01101 | 0
   01110 | 0
   01111 | 0
   10000 | 0
   10001 | 0
   10010 | 0
   10011 | 0
   10100 | 0
   10101 | 0
   10110 | 0
   10111 | 0
   11000 | 1
   11001 | 0
   11010 | 0
   11011 | 0
   11100 | 0
   11101 | 0
   11110 | 0
   11111 | 0
   a^(0):
    | 0
   g2^(4):
   0000 | 0
   0001 | 0
   0010 | 0
   0011 | 0
   0100 | 0
   0101 | 0
   0110 | 0
   0111 | 0
   1000 | 0
   1001 | 0
   1010 | 0
   1011 | 0
   1100 | 0
   1101 | 0
   1110 | 1
   1111 | 0
   h^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 1
   
  
Labelling:
   g1^(4):
   0000 | 0
   0001 | 0
   0010 | 0
   0011 | 0
   0100 | 0
   0101 | 0
   0110 | 0
   0111 | 0
   1000 | 0
   1001 | 0
   1010 | 0
   1011 | 0
   1100 | 0
   1101 | 0
   1110 | 0
   1111 | 0
   f^(5):
   00000 | 0
   00001 | 0
   00010 | 0
   00011 | 0
   00100 | 0
   00101 | 0
   00110 | 0
   00111 | 0
   01000 | 0
   01001 | 0
   01010 | 0
   01011 | 0
   01100 | 0
   01101 | 0
   01110 | 0
   01111 | 0
   10000 | 0
   10001 | 0
   10010 | 0
   10011 | 0
   10100 | 0
   10101 | 0
   10110 | 0
   10111 | 0
   11000 | 0
   11001 | 0
   11010 | 0
   11011 | 0
   11100 | 0
   11101 | 0
   11110 | 0
   11111 | 0
   a^(0):
    | 0
   g2^(4):
   0000 | 0
   0001 | 0
   0010 | 0
   0011 | 0
   0100 | 0
   0101 | 0
   0110 | 0
   0111 | 0
   1000 | 0
   1001 | 0
   1010 | 0
   1011 | 0
   1100 | 0
   1101 | 0
   1110 | 0
   1111 | 0
   h^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   
  
Labelled predicative System:
   {       f_sl=0(x,y,w,w,a_sl=0();) -> g1_sl=0(x,x,y,w;),
           f_sl=0(x,y,w,w,a_sl=0();) -> g1_sl=0(x,x,y,w;),
           f_sl=0(x,y,w,w,a_sl=0();) -> g1_sl=0(x,x,y,w;),
           f_sl=0(x,y,w,w,a_sl=0();) -> g1_sl=0(x,x,y,w;),
           f_sl=0(x,y,w,w,a_sl=0();) -> g1_sl=0(x,x,y,w;),
           f_sl=0(x,y,w,w,a_sl=0();) -> g1_sl=0(x,x,y,w;),
           f_sl=0(x,y,w,w,a_sl=0();) -> g1_sl=0(x,x,y,w;),
           f_sl=0(x,y,w,w,a_sl=0();) -> g1_sl=0(x,x,y,w;),
    f_sl=0(x,y,w,a_sl=0(),a_sl=0();) -> g1_sl=0(y,x,x,w;),
    f_sl=0(x,y,w,a_sl=0(),a_sl=0();) -> g1_sl=0(y,x,x,w;),
    f_sl=0(x,y,w,a_sl=0(),a_sl=0();) -> g1_sl=0(y,x,x,w;),
    f_sl=0(x,y,w,a_sl=0(),a_sl=0();) -> g1_sl=0(y,x,x,w;),
    f_sl=0(x,y,w,a_sl=0(),a_sl=0();) -> g1_sl=0(y,x,x,w;),
    f_sl=0(x,y,w,a_sl=0(),a_sl=0();) -> g1_sl=0(y,x,x,w;),
    f_sl=0(x,y,w,a_sl=0(),a_sl=0();) -> g1_sl=0(y,x,x,w;),
    f_sl=0(x,y,w,a_sl=0(),a_sl=0();) -> g1_sl=0(y,x,x,w;),
    f_sl=0(x,y,a_sl=0(),a_sl=0(),w;) -> g2_sl=0(x,y,y,w;),
    f_sl=0(x,y,a_sl=0(),a_sl=0(),w;) -> g2_sl=0(x,y,y,w;),
    f_sl=0(x,y,a_sl=0(),a_sl=0(),w;) -> g2_sl=0(x,y,y,w;),
    f_sl=0(x,y,a_sl=0(),a_sl=0(),w;) -> g2_sl=0(x,y,y,w;),
    f_sl=0(x,y,a_sl=0(),a_sl=0(),w;) -> g2_sl=0(x,y,y,w;),
    f_sl=0(x,y,a_sl=0(),a_sl=0(),w;) -> g2_sl=0(x,y,y,w;),
    f_sl=0(x,y,a_sl=0(),a_sl=0(),w;) -> g2_sl=0(x,y,y,w;),
    f_sl=0(x,y,a_sl=0(),a_sl=0(),w;) -> g2_sl=0(x,y,y,w;),
           f_sl=0(x,y,a_sl=0(),w,w;) -> g2_sl=0(y,y,x,w;),
           f_sl=0(x,y,a_sl=0(),w,w;) -> g2_sl=0(y,y,x,w;),
           f_sl=0(x,y,a_sl=0(),w,w;) -> g2_sl=0(y,y,x,w;),
           f_sl=0(x,y,a_sl=0(),w,w;) -> g2_sl=0(y,y,x,w;),
           f_sl=0(x,y,a_sl=0(),w,w;) -> g2_sl=0(y,y,x,w;),
           f_sl=0(x,y,a_sl=0(),w,w;) -> g2_sl=0(y,y,x,w;),
           f_sl=0(x,y,a_sl=0(),w,w;) -> g2_sl=0(y,y,x,w;),
           f_sl=0(x,y,a_sl=0(),w,w;) -> g2_sl=0(y,y,x,w;),
            g1_sl=0(x,x,y,a_sl=0();) -> h_sl=0(x,y;),
            g1_sl=0(x,x,y,a_sl=0();) -> h_sl=0(x,y;),
            g1_sl=0(x,x,y,a_sl=0();) -> h_sl=0(x,y;),
            g1_sl=0(x,x,y,a_sl=0();) -> h_sl=0(x,y;),
            g1_sl=0(y,x,x,a_sl=0();) -> h_sl=0(x,y;),
            g1_sl=0(y,x,x,a_sl=0();) -> h_sl=0(x,y;),
            g1_sl=0(y,x,x,a_sl=0();) -> h_sl=0(x,y;),
            g1_sl=0(y,x,x,a_sl=0();) -> h_sl=0(x,y;),
            g2_sl=0(x,y,y,a_sl=0();) -> h_sl=0(x,y;),
            g2_sl=0(x,y,y,a_sl=0();) -> h_sl=0(x,y;),
            g2_sl=0(x,y,y,a_sl=0();) -> h_sl=0(x,y;),
            g2_sl=0(x,y,y,a_sl=0();) -> h_sl=0(x,y;),
            g2_sl=0(y,y,x,a_sl=0();) -> h_sl=0(x,y;),
            g2_sl=0(y,y,x,a_sl=0();) -> h_sl=0(x,y;),
            g2_sl=0(y,y,x,a_sl=0();) -> h_sl=0(x,y;),
            g2_sl=0(y,y,x,a_sl=0();) -> h_sl=0(x,y;),
                        h_sl=0(x,x;) -> x,
                        h_sl=0(x,x;) -> x}
  

  Qed