YES
Time: 0.001488
TRS:
 {        merge(x, nil()) -> x,
          merge(nil(), y) -> y,
  merge(.(x, y), .(u, v)) -> if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v))),
         if(true(), x, y) -> x,
        if(false(), x, y) -> x,
             ++(nil(), y) -> y,
           ++(.(x, y), z) -> .(x, ++(y, z))}
 DP:
  DP:
   {merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v)),
    merge#(.(x, y), .(u, v)) -> merge#(.(x, y), v),
    merge#(.(x, y), .(u, v)) -> if#(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v))),
             ++#(.(x, y), z) -> ++#(y, z)}
  TRS:
  {        merge(x, nil()) -> x,
           merge(nil(), y) -> y,
   merge(.(x, y), .(u, v)) -> if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v))),
          if(true(), x, y) -> x,
         if(false(), x, y) -> x,
              ++(nil(), y) -> y,
            ++(.(x, y), z) -> .(x, ++(y, z))}
  EDG:
   {(++#(.(x, y), z) -> ++#(y, z), ++#(.(x, y), z) -> ++#(y, z))
    (merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v)), merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v)))
    (merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v)), merge#(.(x, y), .(u, v)) -> merge#(.(x, y), v))
    (merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v)), merge#(.(x, y), .(u, v)) -> if#(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v))))
    (merge#(.(x, y), .(u, v)) -> merge#(.(x, y), v), merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v)))
    (merge#(.(x, y), .(u, v)) -> merge#(.(x, y), v), merge#(.(x, y), .(u, v)) -> merge#(.(x, y), v))
    (merge#(.(x, y), .(u, v)) -> merge#(.(x, y), v), merge#(.(x, y), .(u, v)) -> if#(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v))))}
   SCCS (2):
    Scc:
     {++#(.(x, y), z) -> ++#(y, z)}
    Scc:
     {merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v)),
      merge#(.(x, y), .(u, v)) -> merge#(.(x, y), v)}
    SCC (1):
     Strict:
      {++#(.(x, y), z) -> ++#(y, z)}
     Weak:
     {        merge(x, nil()) -> x,
              merge(nil(), y) -> y,
      merge(.(x, y), .(u, v)) -> if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v))),
             if(true(), x, y) -> x,
            if(false(), x, y) -> x,
                 ++(nil(), y) -> y,
               ++(.(x, y), z) -> .(x, ++(y, z))}
     SPSC:
      Simple Projection:
       pi(++#) = 0
      Strict:
       {}
      Qed
    SCC (2):
     Strict:
      {merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v)),
       merge#(.(x, y), .(u, v)) -> merge#(.(x, y), v)}
     Weak:
     {        merge(x, nil()) -> x,
              merge(nil(), y) -> y,
      merge(.(x, y), .(u, v)) -> if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v))),
             if(true(), x, y) -> x,
            if(false(), x, y) -> x,
                 ++(nil(), y) -> y,
               ++(.(x, y), z) -> .(x, ++(y, z))}
     SPSC:
      Simple Projection:
       pi(merge#) = 1
      Strict:
       {merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v))}
      EDG:
       {(merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v)), merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v)))}
       SCCS (1):
        Scc:
         {merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v))}
        SCC (1):
         Strict:
          {merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v))}
         Weak:
         {        merge(x, nil()) -> x,
                  merge(nil(), y) -> y,
          merge(.(x, y), .(u, v)) -> if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v))),
                 if(true(), x, y) -> x,
                if(false(), x, y) -> x,
                     ++(nil(), y) -> y,
                   ++(.(x, y), z) -> .(x, ++(y, z))}
         SPSC:
          Simple Projection:
           pi(merge#) = 0
          Strict:
           {}
          Qed