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}
 LMPO:
  Quasi-Precedence:
  g2 > h, 
  g1 > h, 
  f > g2, 
  f > g1
  empty
  
Normal:
   pi(g2) = [1,2,3,4], pi(f) = [1,2,3,4,5], pi(g1) = [1,2,3,4]
  
Safe:
   pi(h) = [1,2]
  
Predicative System:
   {  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}
  

   
  

  Qed