TRS:
 {        merge(nil(), y) -> y,
          merge(x, nil()) -> x,
  merge(.(x, y), .(u, v)) -> if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v))),
             ++(nil(), y) -> y,
           ++(.(x, y), z) -> .(x, ++(y, z)),
         if(true(), x, y) -> x,
        if(false(), x, y) -> x}
 LMPO:
  Quasi-Precedence:
  merge > if
  empty
  
Normal:
   pi(++) = [1,2], pi(merge) = [1,2]
  
Safe:
   pi(if) = [1,2,3]
  
Predicative System:
   {        merge(nil(),y;) -> y,
            merge(x,nil();) -> x,
    merge(.(x,y;),.(u,v;);) -> if(;<(x,u;),.(x,merge(y,.(u,v;););),.(u,merge(.(x,y;),v;);)),
               ++(nil(),y;) -> y,
             ++(.(x,y;),z;) -> .(x,++(y,z;);),
            if(;true(),x,y) -> x,
           if(;false(),x,y) -> x}
  

   
  

  Qed